From 58b06e843eb3de6a6f683710bee5766a247b2629 Mon Sep 17 00:00:00 2001
From: Felipe Lisboa <lisboafelipe5@gmail.com>
Date: Thu, 8 Sep 2022 12:27:08 +0200
Subject: [PATCH] DDR4: updating trace & proofs
---
framework/DDR3/Arbiter.v | 4 +-
framework/DDR3/Bank.v | 23 +++++--
framework/DDR3/FIFO.v | 10 +--
framework/DDR3/FIFO_proofs.v | 79 ++++++++++++++++--------
framework/DDR3/FIFO_sim.v | 15 +++--
framework/DDR3/ImplementationInterface.v | 6 ++
framework/DDR3/Requests.v | 62 ++++++++++---------
framework/DDR3/System.v | 36 +++++------
framework/DDR3/Trace.v | 45 ++++++++++----
9 files changed, 177 insertions(+), 103 deletions(-)
diff --git a/framework/DDR3/Arbiter.v b/framework/DDR3/Arbiter.v
index 73b0278..e672512 100644
--- a/framework/DDR3/Arbiter.v
+++ b/framework/DDR3/Arbiter.v
@@ -1,11 +1,11 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
+
From DDR3 Require Export Trace.
Section Arbiter.
Context {REQESTOR_CFG : Requestor_configuration}.
- Context {ARBITER_CFG : Arbiter_configuration}.
Context {SYS_CFG : System_configuration}.
Class Arrival_function_t := mkArrivalFunction
@@ -18,7 +18,7 @@ Section Arbiter.
Arrival_uniq : forall t,
uniq (Arrival_at t);
}.
-
+
(* This is a type-class *)
Class Arbiter_t {AF : Arrival_function_t} := mkArbiter
{
diff --git a/framework/DDR3/Bank.v b/framework/DDR3/Bank.v
index b9132ad..2d869ee 100644
--- a/framework/DDR3/Bank.v
+++ b/framework/DDR3/Bank.v
@@ -1,17 +1,30 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
-(* Require Export System. *)
From DDR3 Require Export System.
-(* From DDR3 Require Export System. *)
Section Banks.
+
+ Context {SYS_CFG : System_configuration}.
+
+ Definition Bankgroup_t := { bg : nat | bg < BANKGROUPS }.
+
+ Program Definition Nat_to_bankgroup a : Bankgroup_t :=
+ match a < BANKGROUPS with
+ | true => (exist _ a _) (* blank here is the proof that a satisfies P a *)
+ | false => (exist _ (BANKGROUPS - 1) _)
+ end.
+ Next Obligation.
+ rewrite subn1 ltn_predL lt0n.
+ by specialize BANKGROUPS_pos.
+ Qed.
+
+ Definition Bankgroup_to_nat (a : Bankgroup_t) : nat :=
+ proj1_sig a.
Definition Row_t := nat.
- Context {SYS_CFG : System_configuration}.
- Definition Bank_t :=
- { a : nat | a < BANKS }.
+ Definition Bank_t := { a : nat | a < BANKS }.
Program Definition Nat_to_bank a : Bank_t :=
match a < BANKS with
diff --git a/framework/DDR3/FIFO.v b/framework/DDR3/FIFO.v
index 70a0e56..aac5846 100644
--- a/framework/DDR3/FIFO.v
+++ b/framework/DDR3/FIFO.v
@@ -9,6 +9,8 @@ Section FIFO.
Context {SYS_CFG : System_configuration}.
+ #[local] Axiom DDR3: BANKGROUPS = 1.
+
Instance REQESTOR_CFG : Requestor_configuration :=
{
Requestor_t := unit_eqType
@@ -37,12 +39,12 @@ Section FIFO.
WAIT_END_READ : CAS_date + T_RTP < WAIT;
RC_WAIT : T_RC < WAIT;
- CCD_WAIT : T_CCD < WAIT;
- RRD_WAIT : T_RRD < 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 + T_WL + T_BURST < WAIT;
+ WTR_WAIT : T_WTR_l + T_WL + T_BURST < WAIT;
FAW_WAIT : T_FAW < WAIT + WAIT + WAIT;
}.
@@ -84,7 +86,7 @@ Section FIFO.
IDLE OCycle0 (Enqueue R [::]).
Definition nullreq :=
- mkReq tt 0 RD (Nat_to_bank 0) 0.
+ mkReq tt 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
Definition Next_state R (AS : FIFO_state_t) : (FIFO_state_t * (Command_kind_t * Request_t)) :=
match AS return FIFO_state_t * (Command_kind_t * Request_t) with
diff --git a/framework/DDR3/FIFO_proofs.v b/framework/DDR3/FIFO_proofs.v
index d9e0967..c006fb2 100644
--- a/framework/DDR3/FIFO_proofs.v
+++ b/framework/DDR3/FIFO_proofs.v
@@ -13,13 +13,9 @@ Section FIFOPROOFS.
Existing Instance REQESTOR_CFG.
Context {AF : Arrival_function_t}.
- (* Internal state representation *)
Existing Instance ARBITER_CFG.
-
- (* Type Implementation_t *)
Existing Instance FIFO_implementation.
- (* It looks like this converts State_t to FIFO_state_t automatically, when FIFO is declared as a module *)
Definition FIFO_counter (AS : State_t) :=
match AS with
| IDLE c _ => nat_of_ord c
@@ -986,13 +982,13 @@ Section FIFOPROOFS.
by rewrite leq_add2l leq_eqVlt RTW_WAIT 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.
+ intros Ha Hb Htype aBb sBG.
rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iCWa iCRb].
apply FIFO_CAS_date in Ha as [Hc_a [Hrun_a _]].
apply FIFO_CAS_date in Hb as [Hc_b [Hrun_b _]].
@@ -1006,13 +1002,23 @@ Section FIFOPROOFS.
by rewrite leq_add2l leq_eqVlt WTR_WAIT 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) ->
+ 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 FIFO.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 ->
- Apart_at_least a b T_CCD.
+ 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].
@@ -1029,7 +1035,17 @@ Section FIFOPROOFS.
all: by rewrite leq_add2l leq_eqVlt CCD_WAIT orbT.
Qed.
- Lemma Cmds_T_FAW_ok t a b c d:
+ 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 FIFO.DDR3 as Hbug. by rewrite Hbug in H.
+ Qed.
+
+ Theorem Cmds_T_FAW_ok t a b c d:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
c \in (Default_arbitrate t).(Arbiter_Commands) -> d \in (Default_arbitrate t).(Arbiter_Commands) ->
isACT a -> isACT b -> isACT c -> isACT d -> Diff_Bank [::a;b;c;d] ->
@@ -1067,12 +1083,12 @@ Section FIFOPROOFS.
by rewrite -addnA -addnA leq_add2l addnA leq_eqVlt FAW_WAIT orbT.
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 nSb aBb; rewrite /Apart_at_least.
+ intros Ha Hb AtA nSb aBb sBG; rewrite /Apart_at_least.
move : AtA => /andP [Aa Ab].
apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
2: exact Aa; clear Aa.
@@ -1086,6 +1102,15 @@ Section FIFOPROOFS.
by rewrite leq_eqVlt RRD_WAIT 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 FIFO.DDR3 as Hbug. by rewrite Hbug in H.
+ Qed.
+
+
(* ------------------------------------------------------------------ *)
(* -------------------- REQUEST PROOFS ------------------------------ *)
(* ------------------------------------------------------------------ *)
@@ -2235,7 +2260,7 @@ Section FIFOPROOFS.
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.
apply FIFO_ACT_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
@@ -2248,7 +2273,7 @@ Section FIFOPROOFS.
rewrite /Slot_start Hsb in Hreq_b.
exists (PRE_of_req b.(Request) (b.(CDate) - c)).
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 //=.
(* Solving Before c b*)
apply /andP; split.
@@ -2353,14 +2378,13 @@ Section FIFOPROOFS.
apply FIFO_in_the_past with (t := b.(CDate) - c).
{ by apply leq_subr. }
exact Hreq_b.
-
Qed.
Theorem Cmds_row_ok t b c:
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.
apply FIFO_CAS_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
@@ -2372,7 +2396,7 @@ Section FIFOPROOFS.
rewrite /Slot_start Hsb in Hreq_b.
exists (ACT_of_req b.(Request) (b.(CDate) - c0 + Next_cycle OACT_date)).
rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isACT /Same_Bank //= eq_refl andbT SB eq_refl andbT /Before /Before_at //= -ltnNge.
+ rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
apply /andP; split.
2: {
@@ -2494,8 +2518,6 @@ Section FIFOPROOFS.
rewrite Default_arbitrate_time; apply Cmd_in_trace.
Qed.
- Obligation Tactic := simpl.
-
(* nat -> Trace *)
Definition FIFO_arbitrate t :=
mkTrace
@@ -2510,10 +2532,13 @@ Section FIFOPROOFS.
(Cmds_T_RTP_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/FIFO_sim.v b/framework/DDR3/FIFO_sim.v
index 6371ab3..231a991 100644
--- a/framework/DDR3/FIFO_sim.v
+++ b/framework/DDR3/FIFO_sim.v
@@ -9,12 +9,15 @@ Section FIFOsim.
Program Instance SYS_CFG : System_configuration :=
{
+ BANKGROUPS := 1;
BANKS := 1;
T_BURST := 1;
T_WL := 1;
- T_RRD := 3;
+ T_RRD_s := 1;
+ T_RRD_l := 3;
+
T_FAW := 20;
T_RC := 3;
@@ -25,8 +28,10 @@ Section FIFOsim.
T_WR := 1;
T_RTW := 10;
- T_WTR := 10;
- T_CCD := 12;
+ T_WTR_s := 1;
+ T_WTR_l := 10;
+ T_CCD_s := 1;
+ T_CCD_l := 12;
}.
Program Instance FIFO_CFG : FIFO_configuration :=
@@ -38,8 +43,8 @@ Section FIFOsim.
Existing Instance FIFO_implementation.
Existing Instance FIFO_arbiter.
- Program Definition Req1 := mkReq tt 1 RD 0 1.
- Program Definition Req2 := mkReq tt 2 RD 0 1.
+ Program Definition Req1 := mkReq tt 1 RD 0 0 1.
+ Program Definition Req2 := mkReq tt 2 RD 0 0 1.
Definition Input : Requests_t := [:: Req2; Req1].
diff --git a/framework/DDR3/ImplementationInterface.v b/framework/DDR3/ImplementationInterface.v
index 4281193..7eb0389 100644
--- a/framework/DDR3/ImplementationInterface.v
+++ b/framework/DDR3/ImplementationInterface.v
@@ -4,6 +4,12 @@ From DDR3 Require Export Arbiter.
Section ImplementationInterface.
+ (* The arbiter state *)
+ Class Arbiter_configuration :=
+ {
+ State_t : Type;
+ }.
+
Context {REQESTOR_CFG : Requestor_configuration}.
Context {ARBITER_CFG : Arbiter_configuration}.
Context {SYS_CFG : System_configuration}.
diff --git a/framework/DDR3/Requests.v b/framework/DDR3/Requests.v
index 457de7d..ce2b344 100644
--- a/framework/DDR3/Requests.v
+++ b/framework/DDR3/Requests.v
@@ -1,20 +1,19 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Export ssreflect eqtype.
-Set Printing Projections.
From DDR3 Require Export Util System Requestor Bank.
Section Requests.
Context {REQESTOR_CFG : Requestor_configuration}.
- Context {ARBITER_CFG : Arbiter_configuration}.
+ (* Context {ARBITER_CFG : Arbiter_configuration}. *)
Context {SYS_CFG : System_configuration}.
Inductive Request_kind_t : Set :=
RD |
WR.
- Local Definition Request_kind_eqdef (a b : Request_kind_t) :=
+ #[local] Definition Request_kind_eqdef (a b : Request_kind_t) :=
match a, b with
| RD, RD
| WR, WR => true
@@ -37,6 +36,7 @@ Section Requests.
Requestor : Requestor_t;
Date : nat;
Kind : Request_kind_t;
+ Bankgroup : Bankgroup_t;
Bank : Bank_t;
Row : Row_t
}.
@@ -45,37 +45,43 @@ Section Requests.
(a.(Requestor) == b.(Requestor)) &&
(a.(Date) == b.(Date)) &&
(a.(Kind) == b.(Kind)) &&
+ (a.(Bankgroup) == b.(Bankgroup)) &&
(a.(Bank) == b.(Bank)) &&
(a.(Row) == b.(Row)).
- Lemma Request_eqn : Equality.axiom Request_eqdef.
- Proof.
- unfold Equality.axiom. intros. destruct Request_eqdef eqn:H.
- {
- apply ReflectT. unfold Request_eqdef in *.
- move: H => /andP [/andP [/andP [ /andP [/eqP RQ /eqP Hdate /eqP Hkind /eqP B /eqP R]]]].
- destruct x,y; simpl in *. by subst.
- }
- apply ReflectF. unfold Request_eqdef, not in *.
- intro BUG.
- apply negbT in H. rewrite negb_and in H.
- destruct x, y.
- move: H => /orP [H | /eqP Row].
- rewrite negb_and in H.
- move: H => /orP [H | /eqP Bank].
- rewrite negb_and in H.
- move: H => /orP [H | /eqP Kind].
- rewrite negb_and in H.
- move: H => /orP [/eqP Req | /eqP Date].
- by apply Req; inversion BUG.
- by apply Date; inversion BUG.
- by apply Kind; inversion BUG.
- by apply Bank; inversion BUG.
- by apply Row; inversion BUG.
- Qed.
+
+ Lemma Request_eqn : Equality.axiom Request_eqdef.
+ Proof.
+ unfold Equality.axiom. intros. destruct Request_eqdef eqn:H.
+ {
+ apply ReflectT. unfold Request_eqdef in *.
+ move: H => /andP [/andP [/andP [/andP [ /andP [/eqP RQ /eqP Hdate /eqP Hkind /eqP Bg /eqP B /eqP R]]]]].
+ destruct x,y; simpl in *. by subst.
+ }
+ apply ReflectF. unfold Request_eqdef, not in *.
+ intro BUG.
+ apply negbT in H. rewrite negb_and in H.
+ destruct x, y.
+ move: H => /orP [H | /eqP Row].
+ rewrite negb_and in H.
+ move: H => /orP [H | /eqP Bank].
+ rewrite negb_and in H.
+ move: H => /orP [H | /eqP Bg].
+ rewrite negb_and in H.
+ move: H => /orP [H | /eqP Kind].
+ rewrite negb_and in H.
+ move: H => /orP [/eqP Req | /eqP Date].
+ by apply Req; inversion BUG.
+ by apply Date; inversion BUG.
+ by apply Kind; inversion BUG.
+ by apply Bg; inversion BUG.
+ by apply Bank; inversion BUG.
+ by apply Row; inversion BUG.
+ Qed.
Canonical Request_eqMixin := EqMixin Request_eqn.
Canonical Request_eqType := Eval hnf in EqType Request_t Request_eqMixin.
Definition Requests_t := seq Request_t.
+
End Requests.
\ No newline at end of file
diff --git a/framework/DDR3/System.v b/framework/DDR3/System.v
index 4baa92d..fec7f72 100644
--- a/framework/DDR3/System.v
+++ b/framework/DDR3/System.v
@@ -4,50 +4,46 @@ From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
Section System.
-(* The arbiter state *)
-Class Arbiter_configuration :=
-{
- State_t : Type;
-}.
-
-(* The system *)
Class System_configuration :=
{
+ BANKGROUPS : nat;
BANKS : nat;
T_BURST : nat; (* delay of a burst transfer RD/WR *)
T_WL : nat; (* delay between a WR and its bus transfer *)
-
- T_RRD : nat; (* ACT to ACT delay inter-bank *)
+ T_RRD_s : nat; (* ACT to ACT delay inter-bank : different bank groups *)
+ T_RRD_l : nat; (* ACT to ACT delay inter-bank : same bank groups*)
T_FAW : nat; (* Four ACT window inter-bank *)
-
T_RC : nat; (* ACT to ACT delay intra-bank *)
T_RP : nat; (* PRE to ACT delay intra-bank *)
T_RCD : nat; (* ACT to CAS delay intra-bank *)
T_RAS : nat; (* ACT to PRE delay intra-bank *)
T_RTP : nat; (* RD to PRE delay intra-bank *)
T_WR : nat; (* WR end to PRE delay intra-bank *)
-
T_RTW : nat; (* RD to WR delay intra- + inter-bank *)
- T_WTR : nat; (* WR to RD delay intra- + inter-bank *)
- T_CCD : nat; (* RD/WR to RD/WR delay intra- + inter-bank *)
+ T_WTR_s : nat; (* WR to RD delay intra- + inter-bank : different bank groups *)
+ T_WTR_l : nat; (* WR to RD delay intra- + inter-bank : same bank groups *)
+ 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 *)
(* POs *)
+ BANKGROUPS_pos : BANKGROUPS != 0;
BANKS_pos : BANKS != 0;
-
- T_RRD_pos : T_RRD != 0;
+
+ T_RRD_s_pos : T_RRD_s != 0;
+ T_RRD_l_pos : T_RRD_l != 0;
T_FAW_pos : T_FAW != 0;
-
T_RC_pos : T_RC != 0;
T_RP_pos : T_RP != 0;
T_RCD_pos : T_RCD != 0;
T_RAS_pos : T_RAS != 0;
T_RTP_pos : T_RTP != 0;
T_WR_pos : T_WR != 0;
-
T_RTW_pos : T_RTW != 0;
- T_WTR_pos : T_WTR != 0;
- T_CCD_pos : T_CCD != 0
+ 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
}.
-End System.
\ No newline at end of file
+End System.
\ No newline at end of file
diff --git a/framework/DDR3/Trace.v b/framework/DDR3/Trace.v
index 7b39f08..6253615 100644
--- a/framework/DDR3/Trace.v
+++ b/framework/DDR3/Trace.v
@@ -4,6 +4,7 @@ From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
From DDR3 Require Export Commands.
Section Trace.
+
Context {REQESTOR_CFG : Requestor_configuration}.
Context {SYS_CFG : System_configuration}.
@@ -13,6 +14,11 @@ Section Trace.
Definition Same_Bank (a b : Command_t) :=
a.(Request).(Bank) == b.(Request).(Bank).
+ Hypothesis Same_Row_and_Bank : forall (a b : Command_t), Same_Row a b -> Same_Bank a b.
+
+ Definition Same_Bankgroup (a b : Command_t) :=
+ a.(Request).(Bankgroup) == b.(Request).(Bankgroup).
+
Fixpoint Diff_Bank_ a (S : seq Command_t) :=
match S with
| [::] => true
@@ -66,7 +72,10 @@ Section Trace.
Definition Before_at (a b : Command_t) :=
a.(CDate) <= b.(CDate).
-
+
+ Definition After (a b : Command_t) :=
+ a.(CDate) > b.(CDate).
+
Definition Apart (a b : Command_t) t :=
a.(CDate) + t < b.(CDate).
@@ -140,14 +149,22 @@ Section Trace.
Apart_at_least a b T_RTW;
(* Ensure that the time between a CWR and a CRD commands respects T_WTR + T_WL + T_BURST *)
- Cmds_T_WtoR_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CRD a b -> Before a b ->
- Apart_at_least a b (T_WTR + T_WL + T_BURST);
+ Cmds_T_WtoR_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
+ CWR_to_CRD a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b (T_WTR_l + T_WL + T_BURST);
+
+ Cmds_T_WtoR_DBG_ok : BANKGROUPS > 1 -> forall a b, a \in Commands -> b \in Commands ->
+ 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 *)
- Cmds_T_CCD_ok : forall a b, a \in Commands -> b \in Commands ->
- CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b ->
- Apart_at_least a b 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;
+
+ 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;
(* ---------------------------------------------------------------------------------- *)
@@ -159,9 +176,13 @@ Section Trace.
Apart_at_least a d T_FAW;
(* Ensure that the time between two ACT commands respects T_RRD *)
- Cmds_T_RRD_ok : forall a b, a \in Commands -> b \in Commands ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RRD;
+ Cmds_T_RRD_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
+ ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_l;
+
+ Cmds_T_RRD_DBG_ok : BANKGROUPS > 1 -> forall a b, a \in Commands -> b \in 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;
(* ------------------------------------------------------------------------- *)
(* ------------------------Correctness of the command protocol ------------- *)
@@ -169,11 +190,11 @@ Section Trace.
Cmds_ACT_ok: forall a b, a \in Commands -> b \in Commands ->
isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
- exists c, ((c \in Commands) && (isPRE c) && (Same_Bank b c) && (Same_Bank a c) && (~~ Before_at c a) && (Before c b));
+ exists c, (c \in Commands) && (isPRE c) && (Same_Bank b c) && (Same_Bank a c) && (After c a) && (Before c b);
(* 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_Bank a b && ~~ Before_at a c && Before a b
+ exists a, (a \in Commands) && (isACT a) && (Same_Row a b) && (After a c) && (Before a b)
}.
End Trace.
\ No newline at end of file
--
GitLab