From 52dd50048bd0281d76a13b207fcd6926f55bd22e Mon Sep 17 00:00:00 2001
From: Felipe Lisboa <lisboafelipe5@gmail.com>
Date: Thu, 8 Sep 2022 13:06:15 +0200
Subject: [PATCH] DDR4: adapting proofs to DDR4 modification
---
framework/DDR3/FIFO_proofs.v | 9 +--
framework/DDR3/FIFO_sim.v | 2 +-
framework/DDR3/TDM.v | 48 +++++++++++++--
framework/DDR3/TDM_proofs.v | 115 +++++++++++++++++------------------
framework/DDR3/TDM_sim.v | 56 ++++++++---------
5 files changed, 129 insertions(+), 101 deletions(-)
diff --git a/framework/DDR3/FIFO_proofs.v b/framework/DDR3/FIFO_proofs.v
index c006fb2..8d8a9b8 100644
--- a/framework/DDR3/FIFO_proofs.v
+++ b/framework/DDR3/FIFO_proofs.v
@@ -1110,7 +1110,6 @@ Section FIFOPROOFS.
intros H. specialize FIFO.DDR3 as Hbug. by rewrite Hbug in H.
Qed.
-
(* ------------------------------------------------------------------ *)
(* -------------------- REQUEST PROOFS ------------------------------ *)
(* ------------------------------------------------------------------ *)
@@ -2542,11 +2541,7 @@ Section FIFOPROOFS.
(Cmds_ACT_ok t)
(Cmds_row_ok t).
- Global Program Instance FIFO_arbiter : Arbiter_t :=
- mkArbiter AF FIFO_arbitrate Requests_handled _.
- Next Obligation.
- intros.
- specialize Default_arbitrate_time with (t := t) as H; by apply /eqP.
- Qed.
+ Global Instance FIFO_arbiter : Arbiter_t :=
+ mkArbiter AF FIFO_arbitrate Requests_handled Default_arbitrate_time_match.
End FIFOPROOFS.
\ No newline at end of file
diff --git a/framework/DDR3/FIFO_sim.v b/framework/DDR3/FIFO_sim.v
index 231a991..203e9d9 100644
--- a/framework/DDR3/FIFO_sim.v
+++ b/framework/DDR3/FIFO_sim.v
@@ -10,7 +10,7 @@ Section FIFOsim.
Program Instance SYS_CFG : System_configuration :=
{
BANKGROUPS := 1;
- BANKS := 1;
+ BANKS := 4;
T_BURST := 1;
T_WL := 1;
diff --git a/framework/DDR3/TDM.v b/framework/DDR3/TDM.v
index a51ec18..6ddc974 100644
--- a/framework/DDR3/TDM.v
+++ b/framework/DDR3/TDM.v
@@ -5,8 +5,11 @@ From mathcomp Require Export fintype div.
Require Import Program.
Section TDM.
+
Context {SYS_CFG : System_configuration}.
+ #[local] Axiom DDR3: BANKGROUPS = 1.
+
Definition ACT_date := T_RP.+1.
Definition CAS_date := ACT_date + T_RCD.+1.
@@ -26,10 +29,10 @@ Section TDM.
T_RAS_SL : T_RP.+1 + T_RAS < SL;
T_RC_SL : T_RC < SL;
- T_RRD_SL : T_RRD < SL;
+ T_RRD_SL : T_RRD_l < SL;
T_RTW_SL : T_RTW < SL;
- T_CCD_SL : T_CCD < SL;
- WTR_SL : T_WTR + T_WL + T_BURST < 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;
}.
@@ -204,7 +207,7 @@ Section TDM.
(* Axiom ACommand_t : Command_t. *)
Definition nullreq :=
- mkReq OZSlot 0 RD (Nat_to_bank 0) 0.
+ mkReq OZSlot 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
(* The next-state function of the arbiter *)
Definition Next_state R (AS : TDM_state_t) : (TDM_state_t * (Command_kind_t * Request_t)) :=
@@ -235,7 +238,42 @@ Section TDM.
(RUNNING s' c' P' r, (NOP, nullreq))
end.
- Global Instance TDM_implementation : Implementation_t :=
+ Global Instance TDM_implementation : Implementation_t :=
mkImplementation Init_state Next_state.
+ Definition TDM_counter (AS : State_t) :=
+ match AS with
+ | IDLE _ c _ => c
+ | RUNNING _ c _ _ => c
+ end.
+
+ 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 TDM_slot (AS : State_t) :=
+ match AS with
+ | IDLE s _ _ => s
+ | RUNNING s _ _ _ => s
+ end.
+
+ Definition isRUNNING (AS : State_t) :=
+ match AS with
+ | IDLE _ _ _ => false
+ | RUNNING _ _ _ _ => true
+ end.
+
+ #[local] Axiom Private_Mapping :
+ forall a b, Same_Bank a b ->
+ nat_of_ord (TDM_slot (Default_arbitrate b.(CDate)).(Implementation_State)) =
+ nat_of_ord (TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)).
+
End TDM.
\ No newline at end of file
diff --git a/framework/DDR3/TDM_proofs.v b/framework/DDR3/TDM_proofs.v
index 599131a..9874586 100644
--- a/framework/DDR3/TDM_proofs.v
+++ b/framework/DDR3/TDM_proofs.v
@@ -18,44 +18,9 @@ Section TDMPROOFS.
Existing Instance TDM_implementation.
(*************************************************************************************************)
- (** UTILITY FUNCTIONS AND PROOFS *****************************************************************)
+ (** UTILITY PROOFS *******************************************************************************)
(*************************************************************************************************)
- Definition TDM_counter (AS : State_t) :=
- match AS with
- | IDLE _ c _ => c
- | RUNNING _ c _ _ => c
- end.
-
- 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 TDM_slot (AS : State_t) :=
- match AS with
- | IDLE s _ _ => s
- | RUNNING s _ _ _ => s
- end.
-
- Definition isRUNNING (AS : State_t) :=
- match AS with
- | IDLE _ _ _ => false
- | RUNNING _ _ _ _ => true
- end.
-
- Axiom Private_Mapping :
- forall a b, Same_Bank a b ->
- nat_of_ord (TDM_slot (Default_arbitrate b.(CDate)).(Implementation_State)) =
- nat_of_ord (TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)).
-
Lemma ACT_neq_ZCycle:
(OACT_date == OZCycle) = false.
Proof.
@@ -813,7 +778,7 @@ Section TDMPROOFS.
apply PRE_modulo_date in Hb_in as Hb.
2: exact iPb. clear iPb.
rewrite !Time_counter_modulo in Hb,Ha.
- apply Private_Mapping in sB.
+ apply TDM.Private_Mapping in sB.
set (d := SL.-1 - Next_cycle OCAS_date).
set (q := (Next_cycle OCAS_date - Next_cycle OZCycle)).
@@ -891,7 +856,7 @@ Section TDMPROOFS.
apply PRE_modulo_date in Hb_in as Hb.
2: exact iPb. clear iPb.
rewrite !Time_counter_modulo in Hb,Ha.
- apply Private_Mapping in sB.
+ apply TDM.Private_Mapping in sB.
set (d := SL.-1 - Next_cycle OCAS_date).
set (q := (Next_cycle OCAS_date - Next_cycle OZCycle)).
@@ -978,13 +943,13 @@ Section TDMPROOFS.
by rewrite leq_add2l leq_eqVlt T_RTW_SL orbT.
Qed.
- Theorem Cmds_T_WtoR_ok t a b:
+ Theorem Cmds_T_WtoR_SBG_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_CRD a b -> Before a b ->
- Apart_at_least a b (T_WTR + T_WL + T_BURST).
+ CWR_to_CRD a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b (T_WTR_l + T_WL + T_BURST).
Proof.
- intros Ha Hb Htype aBb; unfold Apart_at_least.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iA iB].
apply CAS_modulo_date in Ha.
2: by unfold isCWR in iA; unfold isCAS; rewrite iA orbT. clear iA.
@@ -999,13 +964,23 @@ Section TDMPROOFS.
by rewrite leq_add2l leq_eqVlt WTR_SL orbT.
Qed.
- Theorem Cmds_T_CCD_ok t a b:
+ Theorem Cmds_T_WtoR_DBG_ok t:
+ BANKGROUPS > 1 -> forall (a b : Command_t),
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b ->
- Apart_at_least a b T_CCD.
+ CWR_to_CRD a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b (T_WTR_s + T_WL + T_BURST).
+ Proof.
+ intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
+ Qed.
+
+ Theorem Cmds_T_CCD_SBG_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_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.
Proof.
- intros Ha Hb Htype aBb; unfold Apart_at_least.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
destruct Htype as [Htype | Htype].
2: unfold CWR_to_CWR in Htype; move: Htype => /andP [iWa iWb].
1: unfold CRD_to_CRD in Htype; move: Htype => /andP [iRa iRb].
@@ -1021,7 +996,17 @@ Section TDMPROOFS.
all: apply leq_trans with (n := a.(CDate) + SL).
all: try exact Ha.
all: by rewrite leq_add2l leq_eqVlt T_CCD_SL orbT.
- Qed.
+ Qed.
+
+ Theorem Cmds_T_CCD_DBG_ok t:
+ BANKGROUPS > 1 -> forall a b,
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_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.
+ Proof.
+ intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
+ Qed.
Lemma Cmds_T_FAW_ok t a b c d:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
@@ -1070,12 +1055,12 @@ Section TDMPROOFS.
by rewrite addnACl.
Qed.
- Lemma Cmds_T_RRD_ok t a b:
+ Theorem Cmds_T_RRD_SBG_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RRD.
+ ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_l.
Proof.
- intros Ha Hb AtA _ aBb.
+ intros Ha Hb AtA _ aBb sBG.
move : AtA => /andP [Aa Ab].
apply ACT_modulo_date in Ha.
2: exact Aa. clear Aa.
@@ -1092,6 +1077,14 @@ Section TDMPROOFS.
by rewrite leq_eqVlt T_RRD_SL orbT.
Qed.
+ Theorem Cmds_T_RRD_DBG_ok t: BANKGROUPS > 1 -> forall a b,
+ a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_s.
+ Proof.
+ intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
+ Qed.
+
(*************************************************************************************************)
(** REQUEST HANDLING PROOFS **********************************************************************)
(*************************************************************************************************)
@@ -2074,7 +2067,7 @@ Section TDMPROOFS.
Theorem Cmds_ACT_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
- exists c, (c \in (Default_arbitrate t).(Arbiter_Commands)) && isPRE c && Same_Bank b c && Same_Bank a c && ~~ Before_at c a && Before c b.
+ exists c, (c \in (Default_arbitrate t).(Arbiter_Commands)) && isPRE c && Same_Bank b c && Same_Bank a c && After c a && Before c b.
Proof.
intros Ha Hb iA iAb SB aBb.
(* info about b's counter *)
@@ -2093,7 +2086,7 @@ Section TDMPROOFS.
move: Hc_b => /eqP Hc_b. rewrite /Last_slot_start Hc_b in Hreq_b.
exists (PRE_of_req b.(Request) (b.(CDate) - Next_cycle OACT_date).+1).
rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isPRE /Same_Bank //= eq_refl andbT SB eq_refl andbT andbT /Before /Before_at //= -ltnNge.
+ rewrite /isPRE /Same_Bank //= eq_refl andbT SB eq_refl andbT andbT /Before /After //=.
clear SB.
(* solve Before c b*)
@@ -2223,7 +2216,7 @@ Section TDMPROOFS.
b \in (Default_arbitrate t).(Arbiter_Commands) -> c \in (Default_arbitrate t).(Arbiter_Commands) ->
isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
exists a, (a \in (Default_arbitrate t).(Arbiter_Commands))
- && isACT a && Same_Bank a b && ~~ Before_at a c && Before a b.
+ && isACT a && Same_Row a b && After a c && Before a b.
Proof.
intros Hb Hc iCb iPc SB cBb.
@@ -2238,7 +2231,7 @@ Section TDMPROOFS.
exists (ACT_of_req b.(Request) (b.(CDate) - CAS_date + ACT_date)).
rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /Same_Bank //= eq_refl andbT /isACT //= eq_refl andbT; clear SB; unfold Before,Before_at,ACT_of_req; simpl.
+ rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
apply /andP; split.
2: {
@@ -2255,7 +2248,6 @@ Section TDMPROOFS.
apply /andP; split.
2: {
- rewrite -ltnNge.
apply PRE_modulo_date in Hc as Hc_c. rewrite Time_counter_modulo in Hc_c.
2: exact iPc.
apply TDM_add_counter with (d := CAS_date) in Hc_c as Hc_c'.
@@ -2365,12 +2357,15 @@ Section TDMPROOFS.
(Cmds_T_RC_ok t)
(Cmds_T_RAS_ok t)
(Cmds_T_RTP_ok t)
- (Cmds_T_WTP_ok t)
+ (Cmds_T_WTP_ok t)
(Cmds_T_RtoW_ok t)
- (Cmds_T_WtoR_ok t)
- (Cmds_T_CCD_ok t)
+ (Cmds_T_WtoR_SBG_ok t)
+ (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_ok t)
+ (Cmds_T_RRD_SBG_ok t)
+ (Cmds_T_RRD_DBG_ok t)
(Cmds_ACT_ok t)
(Cmds_row_ok t).
diff --git a/framework/DDR3/TDM_sim.v b/framework/DDR3/TDM_sim.v
index 6c82708..0fefeef 100644
--- a/framework/DDR3/TDM_sim.v
+++ b/framework/DDR3/TDM_sim.v
@@ -6,34 +6,32 @@ Require Import Program.
From DDR3 Require Export TDM_proofs.
Section Test.
- Program Instance BANK_CFG : Bank_configuration :=
- {
- BANKS := 2;
-
- T_BURST := 1;
- T_WL := 1;
-
- T_RRD := 3;
- T_FAW := 20;
-
- T_RC := 3;
- T_RP := 7;
- T_RCD := 2;
- T_RAS := 4;
- T_RTP := 2;
- T_WR := 1;
-
- T_RTW := 10;
- T_WTR := 10;
- T_CCD := 12;
-
- T_WTR_s := 10;
- T_WTR_l := 10;
- T_CCD_s := 10;
- T_CCD_l := 10;
- T_RRD_s := 10;
- T_RRD_l := 10;
- }.
+
+ Program Instance SYS_CFG : System_configuration := {
+ BANKGROUPS := 1;
+ BANKS := 3;
+
+ T_BURST := 1;
+ T_WL := 1;
+
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+
+ T_FAW := 20;
+
+ T_RC := 3;
+ T_RP := 4;
+ T_RCD := 2;
+ 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;
+ }.
Program Instance TDM_CFG : TDM_configuration :=
{
@@ -42,6 +40,8 @@ Section Test.
}.
Existing Instance REQESTOR_CFG.
+ Existing Instance TDM_implementation.
+ Existing Instance TDM_arbiter.
Program Definition Req1 := mkReq (Ordinal (_ : 0 < SN)) 0 RD 0 0 0.
Program Definition Req2 := mkReq (Ordinal (_ : 1 < SN)) 4 WR 0 1 0.
--
GitLab