diff --git a/framework/DRAM/FIFO_proofs.v b/framework/DRAM/FIFO_proofs.v
index 4cfa6d5bedf3d00922a2cd9f69496456c6925165..58a7a73653fc545bb02fe5b0cf11df1af70cd9a9 100644
--- a/framework/DRAM/FIFO_proofs.v
+++ b/framework/DRAM/FIFO_proofs.v
@@ -4,6 +4,7 @@ Set Printing Projections.
From mathcomp Require Export fintype div.
Require Import Program.
From DRAM Require Export FIFO.
+From mathcomp Require Import ssrZ zify.
Section FIFOPROOFS.
@@ -15,6 +16,10 @@ Section FIFOPROOFS.
Existing Instance ARBITER_CFG.
Existing Instance FIFO_implementation.
+
+ (* ------------------------------------------------------------------ *)
+ (* --------------------- USEFUL DEFINITIONS ------------------------- *)
+ (* ------------------------------------------------------------------ *)
Definition FIFO_counter (AS : State_t) :=
match AS with
@@ -58,6 +63,10 @@ Section FIFOPROOFS.
| RUNNING _ _ r => Some r
end.
+ (* ------------------------------------------------------------------ *)
+ (* --------------------- BASIC LEMMAS ------------------------------- *)
+ (* ------------------------------------------------------------------ *)
+
Ltac isCommand :=
unfold isPRE, isACT, isCAS, PRE_of_req, ACT_of_req, CAS_of_req, Kind_of_req;
match goal with
@@ -2473,6 +2482,50 @@ Section FIFOPROOFS.
apply leq_subr. }
exact Hreq_b.
Qed.
+
+ Theorem Cmds_initial t b:
+ b \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS b ->
+ exists a, (a \in (Default_arbitrate t).(Arbiter_Commands)) && (isACT a) && (Same_Row a b) && (Before a b).
+ Proof.
+ intros Hb iCb.
+ apply FIFO_CAS_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
+ 2: done.
+ destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb.
+ 1: by simpl in Hrun_b.
+ rewrite -Hsb in Hreq_b.
+ apply Request_ACT_bounded in Hreq_b.
+ 2: by rewrite -Hsb in Hrun_b.
+ rewrite /Slot_start Hsb in Hreq_b.
+ exists (ACT_of_req b.(Request) (b.(CDate) - c + Next_cycle OACT_date)).
+ rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
+
+ apply /andP; split.
+ 2: {
+ rewrite /FIFO_counter in Hcb; rewrite Hcb FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS.
+ rewrite -Hsb in Hrun_b.
+ rewrite -subnA.
+ 3: {
+ apply Date_gt_counter in Hrun_b as H; rewrite Hsb /FIFO_counter Hcb FIFO_next_cycle_cas_eq_casS in H.
+ apply ltn_trans with (m := CAS_date) in H. exact H. done. }
+ 2: rewrite /CAS_date /ACT_date -addnS; by apply nat_ltn_add.
+ rewrite ltn_subrL.
+ apply FIFO_date_gt_0 in Hb; rewrite subn_gt0 Hb andbT -addn1 -[CAS_date.+1]addn1 leq_add2r.
+ rewrite /CAS_date /ACT_date; apply nat_ltn_add; by rewrite lt0n T_RCD_pos.
+ }
+
+ apply FIFO_in_the_past with (t := b.(CDate)).
+ { by apply Cmd_in_trace. }
+ apply FIFO_in_the_past with (t := b.(CDate) - c + Next_cycle OACT_date).
+ { rewrite -subnA.
+ 3: { rewrite -Hsb in Hrun_b; apply Date_gt_counter in Hrun_b.
+ rewrite /FIFO_counter Hsb in Hrun_b; by rewrite leq_eqVlt Hrun_b orbT. }
+ 2: { rewrite /FIFO_counter in Hcb; rewrite Hcb;
+ rewrite FIFO_next_cycle_cas_eq_casS FIFO_nextcycle_act_eq_actS;
+ rewrite /CAS_date -addnS; by apply nat_ltn_add. }
+ apply leq_subr. }
+ exact Hreq_b.
+ Qed.
+
(* ------------------------------------------------------------------ *)
(* --------------------- INSTANCES ---------------------------------- *)
@@ -2518,7 +2571,7 @@ Section FIFOPROOFS.
Qed.
(* nat -> Trace *)
- Definition FIFO_arbitrate t :=
+ Program Definition FIFO_arbitrate t :=
mkTrace
(Default_arbitrate t).(Arbiter_Commands)
(Default_arbitrate t).(Arbiter_Time)
@@ -2535,12 +2588,17 @@ Section FIFOPROOFS.
(Cmds_T_WtoR_DBG_ok t)
(Cmds_T_CCD_SBG_ok t)
(Cmds_T_CCD_DBG_ok t)
+ _
+ _
(Cmds_T_FAW_ok t)
(Cmds_T_RRD_SBG_ok t)
(Cmds_T_RRD_DBG_ok t)
(Cmds_ACT_ok t)
- (Cmds_row_ok t).
-
+ (Cmds_row_ok t)
+ (Cmds_initial t)
+ _.
+ Admit Obligations.
+
Global Instance FIFO_arbiter : Arbiter_t :=
mkArbiter AF FIFO_arbitrate Requests_handled Default_arbitrate_time_match.
diff --git a/framework/DRAM/System.v b/framework/DRAM/System.v
index fec7f72f21d86f52a4ab0305822c5c03165d3773..0f74c25af6783eec0261a14da252505a62314efe 100644
--- a/framework/DRAM/System.v
+++ b/framework/DRAM/System.v
@@ -26,6 +26,16 @@ Class System_configuration :=
T_CCD_s : nat; (* RD/WR to RD/WR delay intra- + inter-bank : different bank groups *)
T_CCD_l : nat; (* RD/WR to RD/WR delay intra- + inter-bank : same bank groups *)
+ (* Refresh related properties *)
+ (* Assuming 1X refresh mode *)
+
+ T_REFI : nat;
+ (* All banks must be pre-charged and idle for a minimum time tRP before the REF command can be applied *)
+ (* Address bits should be don't care during a refresh command *)
+ T_RFC : nat; (* Depends on memory density *)
+ (* Delay to be respected between REF and the next valid command (except DES) *)
+ (* Maximum 8/16/32 REF can be postponed -> 1X/2X/4X refresh mode *)
+
(* POs *)
BANKGROUPS_pos : BANKGROUPS != 0;
BANKS_pos : BANKS != 0;
@@ -43,7 +53,12 @@ Class System_configuration :=
T_WTR_s_pos : T_WTR_s != 0;
T_WTR_l_pos : T_WTR_l != 0;
T_CCD_s_pos : T_CCD_s != 0;
- T_CCD_l_pos : T_CCD_l != 0
+ T_CCD_l_pos : T_CCD_l != 0;
+ T_RFC_pos : T_RFC > 0;
+
+ T_RRD_bgs : T_RRD_s < T_RRD_l;
+ T_WTR_bgs : T_WTR_s < T_WTR_l;
+ T_CCD_bgs : T_CCD_s < T_CCD_l;
}.
End System.
\ No newline at end of file
diff --git a/framework/DRAM/TDMds.v b/framework/DRAM/TDMds.v
new file mode 100644
index 0000000000000000000000000000000000000000..64914f43e0b20f5803432d60b7f6bd554e23de82
--- /dev/null
+++ b/framework/DRAM/TDMds.v
@@ -0,0 +1,340 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+
+From DRAM Require Export ImplementationInterface.
+From mathcomp Require Import fintype div ssrZ zify.
+From mathcomp Require Import ssreflect seq.
+
+From Coq Require Import Program FMapList OrderedTypeEx.
+
+(* FMapList.Make expects an instance of the OrderedType module, which we define as Nat_as_OT *)
+Module Import NatMap := FMapList.Make(Nat_as_OT).
+
+Section TDMds.
+
+ Context {SYS_CFG : System_configuration}.
+
+ #[local] Axiom DDR3: BANKGROUPS = 1.
+
+ Definition ACT_date := T_RP.+1.
+ Definition CAS_date := ACT_date + T_RCD.+1.
+
+ Class TDMds_configuration :=
+ {
+ SL : nat; (* still exists *)
+ SN : nat; (* number of critical tasks / TDM slots *)
+
+ SN_one : 1 < SN;
+
+ SL_pos : 0 < SL;
+ SL_ACT : ACT_date < SL;
+ SL_CASS : CAS_date.+1 < SL;
+ }.
+
+ Context {TDMds_CFG : TDMds_configuration}.
+
+ Lemma SN_pos : 0 < SN.
+ specialize SN_one; lia.
+ Qed.
+
+ Lemma SL_CAS: CAS_date < SL.
+ specialize SL_CASS as H; lia.
+ Qed.
+
+ Lemma Last_cycle: SL.-1 < SL.
+ specialize SL_pos; lia.
+ Qed.
+
+ (* Have to introduce the concept of criticality as well *)
+ Record Requestor_t_def := mkRequestorSlack
+ {
+ nb : nat; (* the id of the requestor : no longer bounded by slot number *)
+ crit : bool; (* criticality *)
+
+ (* critical requests are bounded by the number of slots *)
+ crit_req : crit == true -> nb < SN;
+ }.
+
+ Definition Same_Requestor (a b : Requestor_t_def) :=
+ a.(nb) == b.(nb).
+
+ Definition Requestor_t_def_eqdef (a b : Requestor_t_def) :=
+ (a.(nb) == b.(nb)) && (a.(crit) == b.(crit)).
+
+ Lemma Requestor_t_def_eqn : Equality.axiom Requestor_t_def_eqdef.
+ Admitted.
+
+ Canonical Requestor_t_def_eqMixin := EqMixin Requestor_t_def_eqn.
+ Canonical Requestor_t_def_eqType := Eval hnf in EqType Requestor_t_def Requestor_t_def_eqMixin.
+
+ Instance REQUESTOR_CFG : Requestor_configuration :=
+ {
+ Requestor_t := Requestor_t_def_eqType
+ }.
+
+ Context {AF : Arrival_function_t}.
+
+ Definition Slot_t := ordinal_eqType SN.
+ Definition Counter_t := ordinal SL.
+
+ (* Weak maps : maps with no ordering on the key type nor the data type, WSfun and WS *)
+ (* Sfun and S: the key type is ordered *)
+ Check NatMap.t.
+
+ (* Slack is an ordered map from nat (requestor id) to nat (slack amount) *)
+ Definition Slack_t := NatMap.t nat.
+
+ (* Track whether a request is processed (RUNNING) or not (IDLE), the owner of
+ the current slot, the cycle offset within the slot, as well as the set of
+ pending requests. *)
+ Inductive TDM_state_t :=
+ | IDLE : Slot_t -> Slack_t -> Counter_t -> Requests_t -> TDM_state_t
+ | RUNNING : Slot_t -> Slack_t -> Counter_t -> Requests_t -> Request_t-> TDM_state_t.
+
+ Global Instance ARBITER_CFG : Arbiter_configuration :=
+ {
+ State_t := TDM_state_t;
+ }.
+
+ Definition OZCycle := Ordinal SL_pos.
+ Definition OACT_date := Ordinal SL_ACT.
+ Definition OCAS_date := Ordinal SL_CAS.
+ Definition OLastCycle := Ordinal Last_cycle.
+ Definition OZSlot := Ordinal SN_pos.
+
+ (*************************************************************************************************)
+ (** ARBITER IMPLEMENTATION ***********************************************************************)
+ (*************************************************************************************************)
+
+ Definition p_transform (x cs : nat) : nat :=
+ match (cs > 0) as X return nat with
+ | true => if (x < cs) then (cs - 1) - x else (SN - 1 + cs) - x
+ | _ => (SN - 1) - x
+ end.
+
+ Definition egt (cs a b : nat) :=
+ gtn (p_transform a cs) (p_transform b cs).
+
+ Definition lp (cs : Slot_t) := if (nat_of_ord cs == 0) then (SN.-1) else cs.-1.
+
+ Definition dist (max a b : nat) : nat :=
+ if (b < a) then (a - b) else (if (b == a) then 0 else (max - (b - a))).
+
+ (* Definition elt (cs a b : nat) : bool :=
+ if (a == cs) then true
+ else if (b == cs) then false
+ else if (((a > cs) && (b < cs)) || (a < cs) && (b > cs)) then (ltn a b) else ~~ (ltn a b).
+
+ Definition elt_ (cs a b : nat) : bool :=
+ if (b == cs) then true
+ else if (a == cs) then false
+ else if (((a > cs) && (b < cs)) || (a < cs) && (b > cs)) then (ltn a b) else ~~ (ltn a b).
+
+ Definition less_priority cs := (cs + (SN - 1)) %% SN. *)
+
+ (* 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 P : Requests_t) := P ++ R.
+ Definition Dequeue r (P : Requests_t) := rem r P.
+
+ Program Definition nullreq := mkReq
+ (mkRequestorSlack 0 true _) 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+ Next Obligation.
+ exact SN_pos.
+ Qed.
+
+ (* Returns a triple: the selected requestor's id, the current slot, and the request *)
+ Program Definition edf (cs : Slot_t) := foldr (fun r_it r_saved =>
+ let s := r_it.(Requestor).(nb) in
+ let min := r_saved.(Requestor).(nb) in
+ let cs_nat := nat_of_ord cs in
+ if egt cs_nat s min then r_it else r_saved)
+ (mkReq (mkRequestorSlack (nat_of_ord cs) true _) 1 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0).
+
+ Program Definition edf_slack (cs : Slot_t) (smap : Slack_t) := foldr (fun req r_saved =>
+ let min := r_saved.(Requestor).(nb) in
+ let req_id := req.(Requestor).(nb) in
+ let slack := find req.(Requestor).(nb) smap in
+ let cs_nat := nat_of_ord cs in
+ let cond := egt cs_nat req_id min in
+ (* Testing with SN = 4 and SL = 8 *)
+ match slack with
+ | None => if cond then req else r_saved
+ | Some sl => let t := ((cs_nat + 1) * 8) - (req.(Date) %% 32) in
+ if (sl > t) then r_saved
+ (* if there is enough slack, then the
+ associated request is not priority, don't update variables *)
+ else if cond then req else r_saved
+ end) (mkReq (mkRequestorSlack (nat_of_ord cs) true _) 1 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0).
+
+ Program Definition edf_slack_crit (cs : Slot_t) (smap : Slack_t) := foldr (fun r_it r_saved =>
+ let cs_nat := nat_of_ord cs in
+ let r_it_crit := r_it.(Requestor).(crit) in
+ let r_it_id := r_it.(Requestor).(nb) in
+ let r_saved_crit := r_saved.(Requestor).(crit) in
+ let r_saved_id := r_saved.(Requestor).(nb) in
+ if ~~ (r_it_crit) then
+ (* safe to choose the non-critical request when the saved
+ request is not the upcoming one, which has the most priority *)
+ (if (r_saved_id != cs_nat) then r_it else r_saved)
+ else (
+ (* choose the request if:
+ a) r_it[i] > r_saved[i] , i.e., r_it has more priority than r_saved
+ b) r_it[i] is the due for the upcoming slot (most priority), this condition
+ is useful to overwrite previously selected non-critical requests *)
+ let cond := (egt cs_nat r_it_id r_saved_id) || (r_it_id == cs_nat) || (r_saved.(Date) == 0) in
+ let slack := find r_it.(Requestor).(nb) smap in
+ match slack with
+ | None => if cond then r_it else r_saved
+ | Some sl =>
+ let t := (r_it.(Date) %% (SL * SN)) in
+ if (sl > t) then r_saved else
+ (* if there is enough slack, then the
+ associated request is not priority, don't update variables *)
+ (if cond then r_it else r_saved)
+ end(* how to make sure that the initial request will never be picked ? *)
+ )) (mkReq (mkRequestorSlack (lp cs) true _) 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0).
+ Next Obligation.
+ unfold lp; clear H.
+ destruct (nat_of_ord cs == 0); [ rewrite ltn_predL; exact SN_pos | ].
+ destruct cs; simpl; lia.
+ Qed.
+
+ Definition empty_nat_map := NatMap.empty nat.
+
+ Definition Next_state (R : Requests_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 slmap c P =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ if (c == OZCycle) then (
+ match P with
+ | [::] => (IDLE s' slmap c' P', (NOP,nullreq))
+ | _ => let req := edf_slack_crit s slmap P in
+ (RUNNING s' slmap c' (Enqueue R (Dequeue req P)) req, (PRE, req))
+ end)
+ else (IDLE s' slmap c' P', (NOP,nullreq))
+ | RUNNING s slmap c P r =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ if c == OACT_date then
+ (RUNNING s' slmap c' P' r, (ACT, r))
+ else if c == OCAS_date then
+ (RUNNING s' slmap c' P' r, (Kind_of_req r, r))
+ else if c == OLastCycle then
+ let req_id := r.(Requestor).(nb) in
+ let slack' := (dist SN (nat_of_ord s) req_id) * SL in
+ (* replaces existing slack -- won't accumulate *)
+ let slmap' := NatMap.add req_id slack' slmap in
+ (IDLE s' slmap' c' P', (NOP, nullreq))
+ else
+ (RUNNING s' slmap c' P' r, (NOP, nullreq))
+ end.
+
+ Definition Init_state R :=
+ IDLE OZSlot empty_nat_map OZCycle (Enqueue R [::]).
+
+ Instance TDMds_implementation : Implementation_t :=
+ mkImplementation Init_state Next_state.
+
+ Program Definition TDMds_arbitrate t :=
+ mkTrace
+ (Default_arbitrate t).(Arbiter_Commands)
+ (Default_arbitrate t).(Arbiter_Time)
+ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _.
+ Admit Obligations.
+
+ Program Instance TDMds_arbiter : Arbiter_t :=
+ mkArbiter AF TDMds_arbitrate _ _.
+ Admit Obligations.
+
+End TDMds.
+
+Section TDMds_sim.
+
+ Program Instance SYS_CFG : System_configuration :=
+ {
+ BANKGROUPS := 1;
+ BANKS := 8;
+
+ T_BURST := 1;
+ T_WL := 1;
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+ T_FAW := 20;
+ T_RC := 3;
+ T_RP := 1;
+ T_RCD := 1;
+ T_RAS := 4;
+ T_RTP := 4;
+ T_WR := 1;
+ T_RTW := 10;
+ T_WTR_s := 1;
+ T_WTR_l := 10;
+ T_CCD_s := 1;
+ T_CCD_l := 12;
+
+ T_REFI := 10;
+ T_RFC := 10;
+ }.
+
+ Program Instance TDMds_CFG : TDMds_configuration :=
+ {
+ SN := 2;
+ SL := 8;
+ }.
+
+ Existing Instance REQUESTOR_CFG.
+ Existing Instance TDMds_implementation.
+ Existing Instance TDMds_arbiter.
+
+ Program Definition ReqA0 := mkReq
+ (mkRequestorSlack 0 true _) 2 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 5.
+
+ Program Definition ReqB0 := mkReq (* 3 instead of 14 *)
+ (mkRequestorSlack 1 true _) 14 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 10.
+
+ Program Definition ReqC0 := mkReq
+ (mkRequestorSlack 2 false _) 26 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqB1 := mkReq
+ (mkRequestorSlack 1 true _) 28 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqA1 := mkReq
+ (mkRequestorSlack 0 true _) 40 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqC1 := mkReq
+ (mkRequestorSlack 2 false _) 46 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqB2 := mkReq
+ (mkRequestorSlack 1 true _) 50 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqA2 := mkReq
+ (mkRequestorSlack 0 true _) 72 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Definition test_req_seq := [:: ReqA0;ReqB0;ReqC0;ReqB1;ReqA1;ReqC1;ReqB2;ReqA2].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t test_req_seq.
+
+ Compute (Arbitrate 80).(Commands).
+
+End TDMds_sim.
\ No newline at end of file
diff --git a/framework/DRAM/TDMes.v b/framework/DRAM/TDMes.v
new file mode 100644
index 0000000000000000000000000000000000000000..f78c960da7a90f201d69b8344e350bffdf925de0
--- /dev/null
+++ b/framework/DRAM/TDMes.v
@@ -0,0 +1,337 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+
+From DRAM Require Export ImplementationInterface.
+From mathcomp Require Import fintype div ssrZ zify.
+From mathcomp Require Import ssreflect seq.
+
+From Coq Require Import Program FMapList OrderedTypeEx.
+
+(* FMapList.Make expects an instance of the OrderedType module, which we define as Nat_as_OT *)
+Module Import NatMap := FMapList.Make(Nat_as_OT).
+
+Section TDMes.
+
+ Context {SYS_CFG : System_configuration}.
+
+ #[local] Axiom DDR3: BANKGROUPS = 1.
+
+ Definition ACT_date := T_RP.+1.
+ Definition CAS_date := ACT_date + T_RCD.+1.
+
+ Class TDMds_configuration :=
+ {
+ SL : nat; (* still exists *)
+ SN : nat; (* number of critical tasks / TDM slots *)
+
+ SN_one : 1 < SN;
+
+ SL_pos : 0 < SL;
+ SL_ACT : ACT_date < SL;
+ SL_CASS : CAS_date.+1 < SL;
+ }.
+
+ Context {TDMds_CFG : TDMds_configuration}.
+
+ Lemma SN_pos : 0 < SN.
+ specialize SN_one; lia.
+ Qed.
+
+ Lemma SL_CAS: CAS_date < SL.
+ specialize SL_CASS as H; lia.
+ Qed.
+
+ Lemma Last_cycle: SL.-1 < SL.
+ specialize SL_pos; lia.
+ Qed.
+
+ (* Have to introduce the concept of criticality as well *)
+ Record Requestor_t_def := mkRequestorSlack
+ {
+ nb : nat; (* the id of the requestor : no longer bounded by slot number *)
+ crit : bool; (* criticality *)
+
+ (* critical requests are bounded by the number of slots *)
+ crit_req : crit == true -> nb < SN;
+ }.
+
+ Definition Same_Requestor (a b : Requestor_t_def) :=
+ a.(nb) == b.(nb).
+
+ Definition Requestor_t_def_eqdef (a b : Requestor_t_def) :=
+ (a.(nb) == b.(nb)) && (a.(crit) == b.(crit)).
+
+ Lemma Requestor_t_def_eqn : Equality.axiom Requestor_t_def_eqdef.
+ Admitted.
+
+ Canonical Requestor_t_def_eqMixin := EqMixin Requestor_t_def_eqn.
+ Canonical Requestor_t_def_eqType := Eval hnf in EqType Requestor_t_def Requestor_t_def_eqMixin.
+
+ Instance REQUESTOR_CFG : Requestor_configuration :=
+ {
+ Requestor_t := Requestor_t_def_eqType
+ }.
+
+ Context {AF : Arrival_function_t}.
+
+ Definition Slot_t := ordinal_eqType SN.
+ Definition Counter_t := ordinal SL.
+
+ (* Weak maps : maps with no ordering on the key type nor the data type, WSfun and WS *)
+ (* Sfun and S: the key type is ordered *)
+ (* Check NatMap.t. *)
+
+ (* Slack is an ordered map from nat (requestor id) to nat (slack amount) *)
+ Definition Slack_t := NatMap.t nat.
+
+ (* Track whether a request is processed (RUNNING) or not (IDLE), the owner of
+ the current slot, the cycle offset within the slot, as well as the set of
+ pending requests. *)
+ Inductive TDM_state_t :=
+ | IDLE : Slot_t -> Slack_t -> Counter_t -> Requests_t -> TDM_state_t
+ | RUNNING : Slot_t -> Slack_t -> Counter_t -> Counter_t -> Requests_t -> Request_t-> TDM_state_t.
+
+ Global Instance ARBITER_CFG : Arbiter_configuration :=
+ {
+ State_t := TDM_state_t;
+ }.
+
+ Definition OZCycle := Ordinal SL_pos.
+
+ Lemma SL_one : 1 < SL.
+ specialize SL_ACT; specialize T_RP_pos; unfold ACT_date; lia.
+ Qed.
+ Definition OSlot1 := Ordinal SL_one.
+
+ Definition OACT_date := Ordinal SL_ACT.
+ Definition OCAS_date := Ordinal SL_CAS.
+ Definition OLastCycle := Ordinal Last_cycle.
+ Definition OZSlot := Ordinal SN_pos.
+
+ (*************************************************************************************************)
+ (** ARBITER IMPLEMENTATION ***********************************************************************)
+ (*************************************************************************************************)
+
+ Definition p_transform (x cs : nat) : nat :=
+ match (cs > 0) as X with
+ | true => if (x < cs) then (cs - 1) - x else (SN - 1 + cs) - x
+ | _ => (SN - 1) - x
+ end.
+
+ Definition egt (cs a b : nat) :=
+ gtn (p_transform a cs) (p_transform b cs).
+
+ Definition lp (cs : Slot_t) := if (nat_of_ord cs == 0) then (SN.-1) else cs.-1.
+
+ Definition dist (max a b : nat) : nat :=
+ if (b < a) then (a - b) else (if (b == a) then 0 else (max - (b - a))).
+
+ (* 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 P : Requests_t) := P ++ R.
+ Definition Dequeue r (P : Requests_t) := rem r P.
+
+ Program Definition nullreq := mkReq
+ (mkRequestorSlack 0 true _) 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+ Next Obligation.
+ exact SN_pos.
+ Qed.
+
+ Program Definition edf_slack_crit (cs : Slot_t) (smap : Slack_t) := foldr (fun r_it r_saved =>
+ let cs_nat := nat_of_ord cs in
+ let r_it_crit := r_it.(Requestor).(crit) in
+ let r_it_id := r_it.(Requestor).(nb) in
+ let r_saved_crit := r_saved.(Requestor).(crit) in
+ let r_saved_id := r_saved.(Requestor).(nb) in
+ if ~~ (r_it_crit) then
+ (* safe to choose the non-critical request when the saved
+ request is not the upcoming one, which has the most priority *)
+ (if (r_saved_id != cs_nat) then r_it else r_saved)
+ else (
+ (* choose the request if:
+ a) r_it[i] > r_saved[i] , i.e., r_it has more priority than r_saved
+ b) r_it[i] is the due for the upcoming slot (most priority), this condition
+ is useful to overwrite previously selected non-critical requests
+ c) overwrite the default request, which has special date 0 *)
+ let cond := (egt cs_nat r_it_id r_saved_id) || (r_it_id == cs_nat) || (r_saved.(Date) == 0) in
+ let slack := find r_it.(Requestor).(nb) smap in
+ match slack with
+ | None => if cond then r_it else r_saved
+ | Some sl =>
+ let t := (r_it.(Date) %% (SL * SN)) in
+ if (sl > t) then r_saved else
+ (* if there is enough slack, then the
+ associated request is not priority, don't update variables *)
+ (if cond then r_it else r_saved)
+ end(* how to make sure that the initial request will never be picked ? *)
+ )) (mkReq (mkRequestorSlack (lp cs) true _) 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0).
+ Next Obligation.
+ unfold lp; clear H.
+ destruct (nat_of_ord cs == 0); [ rewrite ltn_predL; exact SN_pos | ].
+ destruct cs; simpl; lia.
+ Qed.
+
+ Definition empty_nat_map := NatMap.empty nat.
+
+ Definition early_start cs cnt smap req :=
+ let ncs := nat_of_ord (Next_slot cs OLastCycle) in
+ if (ncs == req.(Requestor).(nb)) then true
+ else (let slack := find ncs smap in
+ match slack with
+ | None => false
+ | Some sl => SL.-1 - cnt < sl
+ end
+ ).
+
+ Definition Next_state (R : Requests_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 slmap c P =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ match P with
+ | [::] => (IDLE s' slmap c' P', (NOP,nullreq))
+ | _ =>
+ (* normal start at beginning of slot *)
+ if (c == OZCycle) then (
+ let req := edf_slack_crit s slmap P in
+ (RUNNING s' slmap c' OSlot1 (Enqueue R (Dequeue req P)) req, (PRE, req)))
+ (* early-start optimisation *)
+ else (
+ (* if arbitrating in the middle of slot, then priority rules chance, hence
+ the different argument sent to the scheduling function *)
+ let req := edf_slack_crit (Next_slot s OLastCycle) slmap P in
+ if (early_start s c slmap req) then
+ (RUNNING s' slmap c' OSlot1 (Enqueue R (Dequeue req P)) req, (PRE, req))
+ else (IDLE s' slmap c' P', (NOP,req)))
+ end
+ | RUNNING s slmap c cnt_cmd P r =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cnt_cmd' := Next_cycle cnt_cmd in
+ if (cnt_cmd == OACT_date) then
+ (RUNNING s' slmap c' cnt_cmd' P' r, (ACT, r))
+ else if (cnt_cmd == OCAS_date) then
+ (RUNNING s' slmap c' cnt_cmd' P' r, (Kind_of_req r, r))
+ else if (cnt_cmd == OLastCycle) then
+ let req_id := r.(Requestor).(nb) in
+ (* slack can be gained in two ways:
+ either by request finishing in the middle of the slot or at the end *)
+ let slack' := if r.(Requestor).(crit) then
+ (SL.-1 - c) + ((dist SN (nat_of_ord s) req_id) * SL) else 0 in
+ (* replaces existing slack with new slack -- won't accumulate *)
+ let slmap' := NatMap.add req_id slack' slmap in
+ (IDLE s' slmap' c' P', (NOP, nullreq))
+ else
+ (RUNNING s' slmap c' cnt_cmd' P' r, (NOP, nullreq))
+ end.
+
+ Definition Init_state R :=
+ IDLE OZSlot empty_nat_map OZCycle (Enqueue R [::]).
+
+ Instance TDMes_implementation : Implementation_t :=
+ mkImplementation Init_state Next_state.
+
+ Program Definition TDMes_arbitrate t :=
+ mkTrace
+ (Default_arbitrate t).(Arbiter_Commands)
+ (Default_arbitrate t).(Arbiter_Time)
+ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _.
+ Admit Obligations.
+
+ Program Instance TDMes_arbiter : Arbiter_t :=
+ mkArbiter AF TDMes_arbitrate _ _.
+ Admit Obligations.
+
+End TDMes.
+
+Section TDMes_sim.
+
+ Program Instance SYS_CFG : System_configuration :=
+ {
+ BANKGROUPS := 1;
+ BANKS := 8;
+
+ T_BURST := 1;
+ T_WL := 1;
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+ T_FAW := 20;
+ T_RC := 3;
+ T_RP := 1;
+ T_RCD := 1;
+ T_RAS := 4;
+ T_RTP := 4;
+ T_WR := 1;
+ T_RTW := 10;
+ T_WTR_s := 1;
+ T_WTR_l := 10;
+ T_CCD_s := 1;
+ T_CCD_l := 12;
+
+ T_REFI := 10;
+ T_RFC := 10;
+ }.
+
+ Program Instance TDMds_CFG : TDMds_configuration :=
+ {
+ SN := 2;
+ SL := 8;
+ }.
+
+ Existing Instance REQUESTOR_CFG.
+ Existing Instance TDMes_implementation.
+ Existing Instance TDMes_arbiter.
+
+ Program Definition ReqA0 := mkReq
+ (mkRequestorSlack 0 true _) 2 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 5.
+
+ Program Definition ReqB0 := mkReq (* 3 instead of 14 *)
+ (mkRequestorSlack 1 true _) 14 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 10.
+
+ Program Definition ReqC0 := mkReq
+ (mkRequestorSlack 2 false _) 26 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqB1 := mkReq
+ (mkRequestorSlack 1 true _) 28 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqA1 := mkReq
+ (mkRequestorSlack 0 true _) 40 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqC1 := mkReq
+ (mkRequestorSlack 2 false _) 40 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqB2 := mkReq
+ (mkRequestorSlack 1 true _) 44 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqA2 := mkReq
+ (mkRequestorSlack 0 true _) 62 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Definition test_req_seq := [:: ReqA0;ReqB0;ReqC0;ReqB1;ReqA1;ReqC1;ReqB2;ReqA2].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t test_req_seq.
+
+ Compute (Arbitrate 80).(Commands).
+
+ (* Next: introduce the concepts of page open / closed *)
+ (* Do proofs about TDMes ? *)
+
+End TDMes_sim.
\ No newline at end of file
diff --git a/framework/DRAM/Trace.v b/framework/DRAM/Trace.v
index 25d8708ff01bf47adb49499d13d4d5f86ee12bb2..31c3af57a502b6c14716f89713907487a83d24fb 100644
--- a/framework/DRAM/Trace.v
+++ b/framework/DRAM/Trace.v
@@ -1,5 +1,6 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
+
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
From DRAM Require Export Commands.
@@ -157,7 +158,7 @@ Section Trace.
CWR_to_CRD a b -> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b (T_WTR_s + T_WL + T_BURST);
- (* Ensure that the time between a CAS and a CAS commands respects T_CCD *)
+ (* Ensure that the time between a CAS and a CAS commaCWR_to_PREnds respects T_CCD *)
Cmds_T_CCD_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> Same_Bankgroup a b ->
Apart_at_least a b T_CCD_l;
@@ -165,6 +166,14 @@ Section Trace.
Cmds_T_CCD_DBG_ok : BANKGROUPS > 1 -> forall a b, a \in Commands -> b \in Commands ->
CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b T_CCD_s;
+
+ (* Refresh related constraints *)
+ Cmds_T_RFC_ok : forall a b, a \in Commands -> b \in Commands ->
+ isREF a -> ~~ isNOP b -> Before a b -> Apart_at_least a b T_RFC;
+
+ (* Upper bound *)
+ Cmds_T_REFI_ok : forall a b, a \in Commands -> b \in Commands ->
+ isREF a -> isREF b -> Before a b -> b.(CDate) <= a.(CDate) + 9 * T_REFI;
(* ---------------------------------------------------------------------------------- *)
@@ -195,6 +204,20 @@ Section Trace.
(* Every CAS command is preceded by a matching ACT without another ACT or PRE in between *)
Cmds_row_ok : forall b c, b \in Commands -> c \in Commands ->
isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
- exists a, (a \in Commands) && (isACT a) && (Same_Row a b) && (After a c) && (Before a b)
+ exists a, (a \in Commands) && (isACT a) && (Same_Row a b) && (After a c) && (Before a b);
+
+ (* implies the init state of the memory *)
+ Cmds_initial : forall b, b \in Commands -> isCAS b ->
+ exists a, (a \in Commands) && (isACT a) && (Same_Row a b) && (Before a b);
+
+ (* Banks must be idle for at least T_RFC cycles before a REF is issued *)
+ Cmds_REF_ok : forall ref, ref \in Commands ->
+ (exists prea, (prea \in Commands) &&
+ (isPREA prea) && (Before prea ref) && (prea.(CDate) + T_RP <= ref.(CDate)))
+ \/
+ (forall bank, bank \in All_banks -> exists pre, (pre \in Commands) &&
+ (isPRE pre) && (Before pre ref) && (bank == pre.(Request).(Bank))
+ && (pre.(CDate) + T_RP <= ref.(CDate)))
}.
+
End Trace.
\ No newline at end of file