diff --git a/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v b/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v
new file mode 100644
index 0000000000000000000000000000000000000000..2e3ff2426c73b5340569a9ef9f1981172daba391
--- /dev/null
+++ b/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v
@@ -0,0 +1,173 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+Set Printing Coercions.
+
+From mathcomp Require Import ssrnat fintype div ssrZ zify ring.
+From CoqDRAM Require Export ImplementationInterface.
+From Coq Require Import Program.
+From Coq Require Import NArith.
+
+Section FIFO.
+
+ Context {SYS_CFG : System_configuration}.
+
+ Instance REQESTOR_CFG : Requestor_configuration := {
+ Requestor_t := unit_eqType
+ }.
+
+ Definition ACT_date := T_RP.-1.
+ Definition CAS_date := ACT_date + T_RCD.
+
+ Definition PREA_date := (T_REFI - T_RP).
+ Definition REF_date := T_RP.-1.
+ Definition END_REF_date := REF_date + T_RFC.
+ (* Just an alias for PRE_date *)
+ (* Definition WAIT_REF := PREA_date. *)
+
+ (* axiom should be here *)
+ Class FIFO_configuration :=
+ {
+ (* The slot length *)
+ WAIT : nat;
+ (* Axioms for hardware compatibility *)
+ WAIT_PW_2 : Nat.pow 2 (Nat.log2 WAIT) = WAIT;
+ WAIT_PW_2_N : N.pow 2 (N.of_nat (Nat.log2 WAIT)) = N.of_nat WAIT;
+
+ (* Basic constraints *)
+ T_RP_GT_ONE : 1 < T_RP;
+ T_RCD_GT_ONE : 1 < T_RCD;
+ T_RTP_GT_ONE : 1 < T_RTP;
+ WAIT_gt_one : 1 < WAIT;
+ WAIT_pos : 0 < WAIT;
+ WAIT_ACT : ACT_date < WAIT;
+ WAIT_CAS : CAS_date < WAIT;
+
+ (* Length of the minimum slot (write request): T_RP + T_RCD + T_WL + T_BURST + T_WR *)
+ WAIT_END_WRITE : CAS_date + T_WR + T_WL + T_BURST < WAIT;
+
+ (* Length of the minimum slot (read request): T_RP + T_RCD + T_RTP *)
+ WAIT_END_READ : CAS_date + T_RTP < WAIT;
+
+ (* WAIT constraints for fitting the slot *)
+ RC_WAIT : T_RC < WAIT;
+ CCD_WAIT : T_CCD_l < WAIT;
+ RRD_WAIT : T_RRD_l < WAIT;
+ RTW_WAIT : T_RTW < WAIT;
+ RAS_WAIT : T_RP + T_RAS < WAIT;
+ WTP_WAIT : T_WR + T_WL + T_BURST < WAIT;
+ WTR_WAIT : T_WTR_l + T_WL + T_BURST < WAIT;
+ FAW_WAIT : T_FAW < WAIT + WAIT + WAIT;
+
+ (* WAIT_REF is the next power of two greather than T_REFI - T_RP *)
+ (* Not optimal but necessary for hardware compatibility *)
+ (* WAIT_REF : nat; *)
+ (* WAIT_REF_val : WAIT_REF = PREA_date; *)
+ PREA_date_pos : 0 < PREA_date ;
+ PREA_date_REF_date : REF_date < PREA_date ;
+ PREA_date_ENDREF_date : END_REF_date < PREA_date ;
+ (* PREA_date_TRP_TRFC : T_RP.-1 + T_RFC < PREA_date ; *)
+
+ (* Hardware compatibility : Workaround *)
+ PREA_date_PW_2 : Nat.pow 2 (Nat.log2 PREA_date) = PREA_date;
+ PREA_date_PW_2_N : N.pow 2 (N.of_nat (Nat.log2 PREA_date)) = N.of_nat PREA_date
+ }.
+
+ Context {FIFO_CFG : FIFO_configuration}.
+ Context {AF : HW_Arrival_function_t}.
+
+ Definition Counter_t := ordinal WAIT.
+ Definition Counter_ref_t := ordinal PREA_date.
+
+ Inductive FIFO_state_t :=
+ | IDLE : Counter_t -> Counter_ref_t -> Requests_t -> FIFO_state_t
+ | RUNNING : Counter_t -> Counter_ref_t -> Requests_t -> Request_t -> FIFO_state_t
+ | REFRESHING : Counter_ref_t -> Requests_t -> FIFO_state_t.
+
+ Instance ARBITER_CFG : Arbiter_configuration := {
+ State_t := FIFO_state_t;
+ }.
+
+ Definition OCycle0 := Ordinal WAIT_pos.
+ Definition OACT_date := Ordinal WAIT_ACT.
+ Definition OCAS_date := Ordinal WAIT_CAS.
+
+ (* Increment counter for cycle ofset (with wrap-arround). *)
+ Definition Next_cycle (c : Counter_t) : Counter_t :=
+ let nextc := c.+1 < WAIT in
+ (if nextc as X return (nextc = X -> Counter_t) then
+ fun (P : nextc = true) => Ordinal (P : nextc)
+ else
+ fun _ => OCycle0) Logic.eq_refl.
+
+ Definition OCycle0REF := Ordinal PREA_date_pos.
+
+ (* Lemma REF_Ord :
+ REF_date < PREA_date.
+ Proof.
+ unfold REF_date, PREA_date.
+ specialize WAIT_REF_TRP_TRFC as H.
+ unfold REF_date, WAIT_REF in *.
+ apply ltn_trans with (n := T_RP.-1 + T_RFC); [ | done].
+ apply nat_ltn_add; by rewrite T_RFC_pos.
+ Qed. *)
+
+ (* Lemma ENDREF_Ord :
+ END_REF_date < WAIT_REF.
+ Proof.
+ unfold END_REF_date,WAIT_REF,REF_date.
+ exact WAIT_REF_TRP_TRFC.
+ Qed. *)
+
+ Definition OREF_date := Ordinal PREA_date_REF_date.
+ Definition OENDREF_date := Ordinal PREA_date_ENDREF_date.
+
+ Definition Next_cycle_ref (c : Counter_ref_t) : Counter_ref_t :=
+ let nextcref := c.+1 < PREA_date in
+ (if nextcref as X return (nextcref = X -> Counter_ref_t) then
+ (fun (P : nextcref = true) => Ordinal (P : nextcref))
+ else (fun _ => OCycle0REF)) Logic.eq_refl.
+
+ Definition Enqueue (R : Request_t) (P : Requests_t) := P ++ [:: R].
+ Definition Dequeue r (P : Requests_t) := rem r P.
+ (* Definition Init_state R := IDLE OCycle0 0 (Enqueue R [::]). *)
+ Definition Init_state R := IDLE OCycle0 OCycle0REF [:: R].
+ Definition nullreq := mkReq tt 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ (* check if there's enough time to proc another req *)
+ Definition Next_state (R : Request_t) (AS : FIFO_state_t)
+ : (FIFO_state_t * (Command_kind_t * Request_t)) :=
+ match AS return FIFO_state_t * (Command_kind_t * Request_t) with
+ | IDLE c cref P =>
+ let P' := Enqueue R P in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ if (nat_of_ord cref == (PREA_date - 1)) then (REFRESHING OCycle0REF P',(PREA,nullreq))
+ else if (cref + WAIT < PREA_date) then
+ match P with
+ | [::] => (IDLE c' cref' P', (NOP,nullreq))
+ | r :: PP => (RUNNING OCycle0 cref' (Enqueue R (Dequeue r P)) r, (PRE,r))
+ end
+ else (IDLE c' cref' P', (NOP,nullreq))
+ | RUNNING c cref P r =>
+ let P' := Enqueue R P in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ if nat_of_ord c == OACT_date then (RUNNING c' cref' P' r, (ACT,r))
+ else if nat_of_ord c == OCAS_date then (RUNNING c' cref' P' r, ((Kind_of_req r), r))
+ else if nat_of_ord c == WAIT.-1 then (IDLE OCycle0 cref' P', (NOP,nullreq))
+ else (RUNNING c' cref' P' r, (NOP,r))
+ | REFRESHING cref P =>
+ let P' := Enqueue R P in
+ let cref' := Next_cycle_ref cref in
+ if (nat_of_ord cref == OREF_date) then (REFRESHING cref' P', (REF,nullreq))
+ else if (cref == OENDREF_date) then (IDLE OCycle0 OCycle0REF P', (NOP, nullreq))
+ else (REFRESHING cref' P', (NOP,nullreq))
+ end.
+
+ (* Global Instance FIFO_implementation : Implementation_t :=
+ mkImplementation Init_state Next_state. *)
+
+ Global Instance FIFO_implementation : HWImplementation_t :=
+ mkHWImplementation Init_state Next_state.
+
+End FIFO.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/TS/TDMREF/TDMREF.v b/framework/DRAM/Implementations/TS/TDMREF/TDMREF.v
new file mode 100644
index 0000000000000000000000000000000000000000..f0daab6ee0dc7d58a4b7c9ddbf00980cc64349c7
--- /dev/null
+++ b/framework/DRAM/Implementations/TS/TDMREF/TDMREF.v
@@ -0,0 +1,244 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+From CoqDRAM Require Export ImplementationInterface.
+From mathcomp Require Export fintype div.
+Require Import Program.
+
+Section TDM.
+
+ Context {SYS_CFG : System_configuration}.
+
+ Definition ACT_date := T_RP.
+ Definition CAS_date := ACT_date + T_RCD.
+
+ Definition PREA_date := (T_REFI - T_RP).
+ Definition REF_date := T_RP.-1.
+ Definition END_REF_date := REF_date + T_RFC.
+
+ Class TDM_configuration :=
+ {
+ SL : nat;
+ SN : nat;
+
+ SL_pos : 0 < SL;
+ SL_one : 1 < SL;
+ SL_ACT : ACT_date < SL;
+ SL_ACTS : ACT_date.+1 < SL;
+ SL_CAS : CAS_date < SL;
+ SL_CASS : CAS_date.+1 < SL;
+
+ SN_pos : 0 < SN;
+ SN_one : 1 < SN;
+
+ T_RP_GT_ONE : 1 < T_RP;
+ T_REFI_T_RP : T_RP < T_REFI;
+
+ T_RTP_SN_SL : T_RTP < SN * SL - CAS_date;
+ T_WTP_SN_SL : (T_WR + T_WL + T_BURST) < SN * SL - CAS_date;
+
+ T_RAS_SL : T_RP + T_RAS < SL;
+ T_RC_SL : T_RC < SL;
+ T_RRD_SL : T_RRD_l < SL;
+ T_RTW_SL : T_RTW < SL;
+ T_CCD_SL : T_CCD_l < SL;
+ WTR_SL : T_WTR_l + T_WL + T_BURST < SL;
+ T_FAW_3SL : T_FAW < SL + SL + SL;
+
+ PREA_date_pos : 0 < PREA_date ;
+ PREA_date_REF_date : REF_date < PREA_date ;
+ PREA_date_ENDREF_date : END_REF_date < PREA_date ;
+ }.
+
+ Context {TDM_CFG : TDM_configuration}.
+
+ (* SL counter *)
+ Definition Counter_t := ordinal SL.
+ Lemma Last_cycle:
+ SL.-1 < SL.
+ Proof.
+ rewrite ltn_predL; apply SL_pos.
+ Qed.
+ Definition OZCycle := Ordinal SL_pos.
+ Definition OACT_date := Ordinal SL_ACT.
+ Definition OCAS_date := Ordinal SL_CAS.
+ Definition OLastCycle := Ordinal Last_cycle.
+
+ (* SN counter *)
+ Definition Slot_t := ordinal_eqType SN.
+ Definition OZSlot := Ordinal SN_pos.
+
+ Instance REQESTOR_CFG : Requestor_configuration := {
+ Requestor_t := Slot_t
+ }.
+
+ (* REF counter *)
+ Definition Counter_ref_t := ordinal PREA_date.
+ Definition OCycle0REF := Ordinal PREA_date_pos.
+ Definition OREF_date := Ordinal PREA_date_REF_date.
+ Definition OENDREF_date := Ordinal PREA_date_ENDREF_date.
+
+ Definition Next_cycle_ref (c : Counter_ref_t) : Counter_ref_t :=
+ let nextcref := c.+1 < PREA_date in
+ (if nextcref as X return (nextcref = X -> Counter_ref_t) then
+ (fun (P : nextcref = true) => Ordinal (P : nextcref))
+ else (fun _ => OCycle0REF)) Logic.eq_refl.
+
+ Context {HAF : HW_Arrival_function_t}.
+
+ Definition Same_Slot (a b : Command_t) :=
+ a.(Request).(Requestor) == b.(Request).(Requestor).
+
+ Inductive TDM_state_t :=
+ | IDLE : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> TDM_state_t
+ | RUNNING : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> Request_t-> TDM_state_t
+ | REFRESHING : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> TDM_state_t.
+
+ Definition TDM_state_eqdef (a b : TDM_state_t) :=
+ match a, b with
+ | IDLE sa ca crefa Pa, IDLE sb cb crefb Pb
+ => (sa == sb) && (ca == cb) && (crefa == crefb) && (Pa == Pb)
+ | RUNNING sa ca crefa Pa ra, RUNNING sb cb crefb Pb rb
+ => (sa == sb) && (ca == cb) && (crefa == crefb) && (Pa == Pb) && (ra == rb)
+ | REFRESHING sa ca crefa Pa, REFRESHING sb cb crefb Pb
+ => (sa == sb) && (ca == cb) && (crefa == crefb) && (Pa == Pb)
+ | _, _ => false
+ end.
+
+ Lemma TDM_state_eqn : Equality.axiom TDM_state_eqdef.
+ Proof.
+ Admitted.
+
+ Canonical TDM_state_eqMixin := EqMixin TDM_state_eqn.
+ Canonical TDM_state_eqType := Eval hnf in EqType TDM_state_t TDM_state_eqMixin.
+
+ Global Instance ARBITER_CFG : Arbiter_configuration := {
+ State_t := TDM_state_t;
+ }.
+
+ (*************************************************************************************************)
+ (** ARBITER IMPLEMENTATION ***********************************************************************)
+ (*************************************************************************************************)
+
+ (* Increment counter for cycle offset (with wrap-arround). *)
+ Definition Next_cycle (c : Counter_t) :=
+ let nextc := c.+1 < SL in
+ (if nextc as X return (nextc = X -> Counter_t) then
+ fun (P : nextc = true) => Ordinal (P : nextc)
+ else
+ fun _ => OZCycle) Logic.eq_refl.
+
+ (* Increment the slot counter (with wrap-arround) *)
+ Definition Next_slot (s : Slot_t) (c : Counter_t) : Slot_t :=
+ if (c.+1 < SL) then
+ s
+ else
+ let nexts := s.+1 < SN in
+ (if nexts as X return (nexts = X -> Slot_t) then
+ fun (P : nexts = true) => Ordinal (P : nexts)
+ else
+ fun _ => OZSlot) Logic.eq_refl.
+
+ Definition Enqueue (R : Request_t) (P : Requests_t) := P ++ [:: R].
+ Definition Dequeue r (P : Requests_t) := rem r P.
+
+ (* The set of pending requests of a slot *)
+ Definition Pending_of s (P : Requests_t) :=
+ [seq r <- P | r.(Requestor) == s].
+
+ Definition Init_state R :=
+ IDLE OZSlot OZCycle OCycle0REF (Enqueue R [::]).
+
+ Hint Unfold PRE_of_req : core.
+ Hint Unfold ACT_of_req : core.
+ Hint Unfold CAS_of_req : core.
+
+ Definition nullreq :=
+ mkReq OZSlot 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ (* The next-state function of the arbiter *)
+ Definition Next_state (R : Request_t) (AS : TDM_state_t)
+ : (TDM_state_t * (Command_kind_t * Request_t)) :=
+ match AS return (TDM_state_t * (Command_kind_t * Request_t)) with
+ | IDLE s c cref P => (* Currently no request is processed *)
+ let P' := Enqueue R P in (* enqueue newly arriving requests *)
+ let s' := Next_slot s c in (* advance slot counter (if needed) *)
+ let c' := Next_cycle c in (* advance slot counter (if needed) *)
+ let cref' := Next_cycle_ref cref in
+ if (cref + SN * SL < PREA_date) then (* there is enough time to start another TDM period *)
+ if (c == OZCycle) then
+ match Pending_of s P with (* Check if a request is pending *)
+ | [::] => (* No? Continue with IDLE *)
+ (IDLE s' c' cref' P', (NOP, nullreq))
+ | r::_ => (* Yes? Emit PRE, dequeue request, and continue with RUNNING *)
+ (RUNNING s' c' cref' (Enqueue R (Dequeue r P)) r, (PRE,r))
+ end
+ else (IDLE s' c' cref' P', (NOP, nullreq))
+ else if (nat_of_ord cref == PREA_date) then (REFRESHING s' c' OCycle0REF P', (PREA,nullreq))
+ else (IDLE s' c' cref' P', (NOP,nullreq))
+ | RUNNING s c cref P r => (* Currently a request is processed *)
+ let P' := Enqueue R P in (* enqueue newly arriving requests *)
+ let s' := Next_slot s c in (* advance slot counter (if needed) *)
+ let c' := Next_cycle c in (* advance slot counter (if needed) *)
+ let cref' := Next_cycle_ref cref in
+ if c == OACT_date then (* need to emit the ACT command *)
+ (RUNNING s' c' cref' P' r, (ACT, r))
+ else if c == OCAS_date then (* need to emit the CAS command *)
+ (RUNNING s' c' cref' P' r, (Kind_of_req r, r))
+ else if c == OLastCycle then (* return to IDLE state *)
+ (IDLE s' c' cref' P', (NOP, nullreq))
+ else (RUNNING s' c' cref' P' r, (NOP, r))
+ | REFRESHING s c cref P =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in (* advance slot counter (if needed) *)
+ let c' := Next_cycle c in (* advance slot counter (if needed) *)
+ let cref' := Next_cycle_ref cref in
+ if (nat_of_ord cref == REF_date) then (REFRESHING s' c' cref' P', (REF,nullreq))
+ else if (nat_of_ord cref == END_REF_date) then (IDLE s' c' OCycle0REF P', (NOP, nullreq))
+ else (REFRESHING s' c' cref' P', (NOP,nullreq))
+ end.
+
+ Global Instance TDM_implementation : HWImplementation_t :=
+ mkHWImplementation Init_state Next_state.
+
+ (* Global Instance TDM_implementation : Implementation_t :=
+ mkImplementation Init_state Next_state. *)
+
+ Definition TDM_counter (AS : State_t) : Counter_t :=
+ match AS with
+ | IDLE _ c _ _ => c
+ | RUNNING _ c _ _ _ => c
+ | REFRESHING _ c _ _ => c
+ end.
+
+ Definition TDM_slot (AS : State_t) :=
+ match AS with
+ | IDLE s _ _ _ => s
+ | RUNNING s _ _ _ _ => s
+ | REFRESHING s _ _ _ => s
+ end.
+
+ Hypothesis Private_Mapping :
+ forall a b, Same_Bank a b ->
+ nat_of_ord (TDM_slot (HW_Default_arbitrate b.(CDate)).(Implementation_State)) =
+ nat_of_ord (TDM_slot (HW_Default_arbitrate a.(CDate)).(Implementation_State)).
+
+ (*
+ Definition TDM_pending (AS : State_t) :=
+ match AS with
+ | IDLE _ _ P => P
+ | RUNNING _ _ P _ => P
+ end.
+
+ Definition TDM_request (AS : State_t) :=
+ match AS with
+ | IDLE _ _ _ => None
+ | RUNNING _ _ _ r => Some r
+ end.
+
+ Definition isRUNNING (AS : State_t) :=
+ match AS with
+ | IDLE _ _ _ => false
+ | RUNNING _ _ _ _ => true
+ end. *)
+
+End TDM.
\ No newline at end of file