Added refresh version of normal implementations

framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v

+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

framework/DRAM/Implementations/TS/TDMREF/TDMREF.v

+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