diff --git a/framework/CavaDRAM/Implementations/CavaFIFOREF/CavaFIFOREFProperties.v b/framework/CavaDRAM/Implementations/CavaFIFOREF/CavaFIFOREFProperties.v
index 0f984862ab51456c604bf252d6049a6986183b05..cabe06f15dc833acaf8bb4b548f952f104dae168 100644
--- a/framework/CavaDRAM/Implementations/CavaFIFOREF/CavaFIFOREFProperties.v
+++ b/framework/CavaDRAM/Implementations/CavaFIFOREF/CavaFIFOREFProperties.v
@@ -47,9 +47,13 @@ Section CavaFIFOProperties.
Definition mem_cells_ :=
mem_cells (Vec Bit REQUEST_WIDTH) ADDR_WIDTH (Nat.pow 2 ADDR_WIDTH) InitMem.
+ Check Cells_read.
+ Locate mem_cells.
+
Lemma nth_cells_read {T W I} (ad : Bvector W) c_req def
(c : circuit_state (mem_cells T W (2 ^ W) I)) :
nth_default def (N.to_nat (Bv2N ad)) (Cells_read true (N.to_nat (Bv2N ad)) c_req c) = c_req.
+ Proof.
Admitted.
Lemma nth_cells_read_ {T W I N} (ad : Bvector (Nat.log2 N)) c_req def
@@ -75,7 +79,8 @@ Section CavaFIFOProperties.
specialize (@length_to_list_shiftin (combType T) N memvec c_req) as HH.
assert (N = (Datatypes.length (Vector.to_list (Vector.shiftin c_req memvec))) - 1)%coq_nat; [ lia | ].
apply nth_last with (d := def) in H1; rewrite H1.
- by rewrite last_shiftin. }
+ by rewrite last_shiftin.
+ }
{ unfold memvec.
specialize (IHN (VectorDef.tl ad) c0); apply IHN in H as IH; clear IHN.
rewrite (Vector.eta ad) Bv2N_cons.
@@ -302,13 +307,18 @@ Section CavaFIFOProperties.
Lemma notfull_rd (wr rd : Bvector ADDR_WIDTH) :
let rdp1 := N2Bv_sized ADDR_WIDTH (Bv2N rd + 1) in
- wr <> rd -> wr <> rdp1 -> ~~ fullQueue wr rd ->
+ wr <> rd ->
+ wr <> rdp1 ->
+ ~~ fullQueue wr rd ->
~~ fullQueue wr rdp1.
Proof.
intros rdp1 Hdif1 Hdif2 HF; unfold fullQueue in HF.
destruct (leq _ _) eqn:Hleq.
{ rewrite leq_eqVlt in Hleq; move: Hleq => /orP [/eqP Heq | Hleq].
- { admit. (* impossible *)}
+ { contradict Heq.
+ specialize (@Bv2N_neq_inj ADDR_WIDTH wr rd) as H; apply H in Hdif1.
+ apply not_eq_sym; lia.
+ }
unfold fullQueue.
destruct (Bv2N rdp1 <= _) eqn:Hleq2.
{ apply /negPf. apply N.eqb_neq.
@@ -317,7 +327,9 @@ Section CavaFIFOProperties.
move: HF => /negPf HF; apply N.eqb_neq in HF.
apply (N.lt_gt_cases (Bv2N wr - Bv2N rd) (N.of_nat QUEUE_MAX_SIZE - 1)) in HF as HF';
destruct HF' as [H0 | H1].
- 2: admit. (* Impossible, Bv2N wr - Bv2N rd cannot be bigger than QMS *)
+ 2: {
+ admit. (* Impossible, Bv2N wr - Bv2N rd cannot be bigger than QMS *)
+ }
apply (N.lt_trans (Bv2N wr - Bv2N rdp1) (Bv2N wr - Bv2N rd) (N.of_nat QUEUE_MAX_SIZE - 1));
[ | exact H0 ].
assert (N.lt (Bv2N rd) (Bv2N rdp1)); [ admit | ].
@@ -783,7 +795,7 @@ Section CavaFIFOProperties.
(cref + WAIT < PREA_date) = false ->
(nat_of_ord cref == PREA_date - 1) = false ->
(* Start of conclusion *)
- let f_state := (Default_arbitrate t).(Implementation_State) in
+ (* let f_state := (Default_arbitrate t).(Implementation_State) in *)
let R := Arrival_at t in
R == [:: arriving_req] ->
EqReq (Some arriving_req) c_req ->
@@ -791,7 +803,9 @@ Section CavaFIFOProperties.
State_Eq S c_state ->
let '(f_nextstate,f_cmd_o) := Next_state R S in
let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step CavaFIFOREF c_state (true,c_req) in
- (State_Eq f_nextstate c_nextstate) && (EqCmd f_cmd_o c_cmd_o).
+ (State_Eq f_nextstate c_nextstate) && (EqCmd f_cmd_o c_cmd_o).
+ Admitted.
+ (*
Proof.
intros Href_service Href_prea f_state R NF EqR S H; unfold CavaFIFOREF.
unfold R in *; clear R.
@@ -803,7 +817,6 @@ Section CavaFIFOProperties.
(* What we know from State_Eq *)
autounfold with get_state in H; cbn [fst snd] in H.
-
move: H => /andP [/andP [/andP [/andP [EqS EqCnt] EqCref] Mem] HQ].
(* Queue not empty -> wra <> rda *)
@@ -858,8 +871,6 @@ Section CavaFIFOProperties.
destruct H as [cs_requeue' [Hx H]]; destruct Hx as [Hrw [Hwra' Hrda']].
autounfold with get_state.
- apply /andP; split.
- 2 : exact EqReqNil.
apply /andP; split.
2 : unfold EqCmd; by apply BVEq_iff_eq.
apply /andP; split.
@@ -867,15 +878,16 @@ Section CavaFIFOProperties.
rewrite (surjective_pairing (step RequestQueue' _ _)) H.
cbv [get_addr_RequestQueue] in Hwra'; rewrite Hwra'; clear Hwra'.
cbv [get_addr_RequestQueue] in Hrda'; rewrite Hrda'; clear Hrda'.
- rewrite /Enqueue /R NF.
- apply (EqQueue_aux wra rda r0 r1 r); done.
+ rewrite /Enqueue NF.
+ apply (EqQueue_aux wra rda r0 P arriving_req); try done.
+ by apply NFULL.
}
apply /andP; split.
2 : {
rewrite /EqMem (surjective_pairing (step RequestQueue' _ _)) H Hrda'; cbn [fst snd];
- unfold R; rewrite NF Hrw /Enqueue.
+ rewrite NF Hrw /Enqueue.
cbv [get_memcells_RequestQueue get_mem_RequestQueue get_memcells].
- apply EqMem_rcons; try done.
+ apply EqMem_rcons; done.
}
apply /andP; split.
2 : {
@@ -884,18 +896,19 @@ Section CavaFIFOProperties.
| |- context [ match ?p with pair _ _ => _ end ] => rewrite (surjective_pairing p)
end; cbn [fst snd].
rewrite //= /Next_cycle_ref.
- set Hc := c1.+1 < PREA_date; dependent destruction Hc;
+ set Hc := cref.+1 < PREA_date; dependent destruction Hc;
apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro.
- { rewrite /cref2Bv //= Bv2N_N2Bv_sized.
- 2: apply to_nat_lt_pow; rewrite Nat2N.id; apply cref_bound.
+ { rewrite /cref2Bv. rewrite //=.
+ rewrite Bv2N_N2Bv_sized.
+ 2: { apply to_nat_lt_pow. rewrite Nat2N.id. apply cref_bound. }
rewrite /N2Bv_sized.
- destruct (N.of_nat c1 + 1)%N eqn:Hbug;
+ destruct (N.of_nat cref + 1)%N eqn:Hbug;
[ rewrite N.add_1_r in Hbug; contradict Hbug; apply N.neq_succ_0 | ].
apply BVEq_iff_eq; f_equal; lia.
}
- { specialize (cref_bound c1) as Hc1_bound.
- destruct c1; clear H Hrw Hwra' Hrda' cs_requeue' cs_nextcr; simpl in *.
- apply ltn_gt in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x]; [ | lia].
+ { specialize (cref_bound cref) as Hc1_bound.
+ destruct cref; clear H Hrw Hwra' Hrda' cs_requeue' cs_nextcr; simpl in *.
+ apply gtF_leq in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x]; [ | lia].
assert (m = PREA_date.-1); [ lia | ].
rewrite H in Href_prea; contradict Href_prea; apply not_false_iff_true; by rewrite subn1 eq_refl.
}
@@ -909,7 +922,7 @@ Section CavaFIFOProperties.
rewrite /cnt2Bv //=; apply BVEq_iff_eq; f_equal; apply Nat2N.inj_iff.
rewrite /Bv2cnt /Next_cycle //= Bv2N_N2Bv_sized //=.
2: {
- destruct c0; rewrite //= /COUNTER_WIDTH.
+ destruct cnt; rewrite //= /COUNTER_WIDTH.
rewrite WAIT_PW_2_N; apply N_lt_inj; by apply /ltP.
}
set (Hc := _ < WAIT); dependent destruction Hc;
@@ -922,32 +935,46 @@ Section CavaFIFOProperties.
end; cbn [fst snd].
by [].
Qed.
+ *)
- Theorem SM_Eq_3a (t : nat) (c_state : State_t) c0 (r : Request_t)
- (c1 : Counter_ref_t) (c_req : Bvector REQUEST_WIDTH) :
- (c1 + WAIT < PREA_date) = false ->
- (nat_of_ord c1 == PREA_date - 1) = false ->
+ Theorem SM_Eq_3a (t : nat) (c_state : State_t) cnt (r arriving_req: Request_t)
+ (cref : Counter_ref_t) (c_req : Bvector REQUEST_WIDTH) :
+ (cref + WAIT < PREA_date) = false ->
+ (nat_of_ord cref == PREA_date - 1) = false ->
+ (* Start of conclusion*)
let f_state := (Default_arbitrate t).(Implementation_State) in
- let R := HW_Arrival_at t in
- R == [:: r] -> EqReq r c_req -> State_Eq (IDLE c0 c1 []) c_state ->
- let '(f_nextstate,(f_cmd_o,f_req_o)) := Next_state R (IDLE c0 c1 []) in
- let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step FIFOSM_ c_state (true,c_req) in
- (State_Eq f_nextstate c_nextstate) &&
- (EqCmd f_cmd_o c_cmd_o) && (EqReq f_req_o c_req_o).
+ let R := Arrival_at t in
+ R == [:: arriving_req] ->
+ EqReq (Some arriving_req) c_req ->
+ let S := IDLE cnt cref [] in
+ State_Eq S c_state ->
+ let '(f_nextstate,f_cmd_o) := Next_state R S in
+ let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step CavaFIFOREF c_state (true,c_req) in
+ (State_Eq f_nextstate c_nextstate) && (EqCmd f_cmd_o c_cmd_o).
+ Admitted.
+ (*
Proof.
- intros Href_service Href_prea f_state R NF EqR H; unfold FIFOSM_.
- unfold R in NF; specialize (HaltIfFull t c_state) as NFULL; move: NF => /eqP NF.
+ intros Href_service Href_prea f_state R NF EqR S H; unfold CavaFIFOREF.
+ unfold R in *; clear R.
+ specialize (HaltIfFull t c_state) as NFULL; move: NF => /eqP NF.
unfold State_t in c_state; simpl in c_state; destruct_products.
rewrite NF //= in NFULL; cbv [get_wra get_rda get_fields] in NFULL.
- rename t0 into s, t1 into cnt, t2 into cref, t3 into cr, t4 into wra, t5 into rda.
- rewrite /State_Eq /EqMem in H; autounfold with get_state in H; cbn [fst snd] in H.
-
+ rename t0 into s, t1 into cnt_, t2 into cref_, t3 into cr, t4 into wra, t5 into rda.
+ rewrite /State_Eq /EqMem in H; unfold S in H.
+
+ (* What we know from State_Eq *)
+ autounfold with get_state in H; cbn [fst snd] in H.
move: H => /andP [/andP [/andP [/andP [EqS EqCnt] EqCref] Mem] Hadr].
- simpl in Hadr.
- apply BVEq_iff_eq in EqS, EqCnt, EqCref, Hadr; subst s cnt cref.
+
+ apply BVEq_iff_eq in EqS, EqCnt, EqCref; subst s cnt_ cref_.
+ unfold S in *; clear S.
+
cbv [LoopInit]; cbn [step fst snd]; simpl_ret; cbv [and2]; cbn [fst snd].
+
+ simpl in Hadr.
+ apply BVEq_iff_eq in Hadr.
- assert ((Sidle STATE_IDLE_VEC && CrefPREA_lt (cref2Bv c1)) = false) as Haux;
+ assert ((Sidle STATE_IDLE_VEC && CrefPREA_lt (cref2Bv cref)) = false) as Haux;
[ apply CrefPREA_lt_CNT_REF_WAIT_F in Href_service; by rewrite Href_service andb_false_r | ].
rewrite Haux; clear Haux.
@@ -959,26 +986,27 @@ Section CavaFIFOProperties.
rewrite H; clear H; cbn [fst snd].
set tr := nth_default req_null (N.to_nat (Bv2N rda)) _.
- specialize NextCR_equiv with (c := (u7, (u8, cr))) (cnt := cnt2Bv c0)
- (cref := cref2Bv c1) (tr := tr) as [cs_nextcr H].
- rewrite H; cbv [fst]; clear H. cbn [snd].
+ specialize NextCR_equiv with (c := (u7, (u8, cr))) (cnt := cnt2Bv cnt)
+ (cref := cref2Bv cref) (tr := tr) as [cs_nextcr H].
+ rewrite H; cbv [fst]; clear H; cbn [snd].
apply cref_preadate_false in Href_prea as Href_prea_.
- apply (CmdGen_equiv_idle_to_idle_E u5 (cnt2Bv c0) (cref2Bv c1)) in Href_prea_ as H.
+ apply (CmdGen_equiv_idle_to_idle_E u5 (cnt2Bv cnt) (cref2Bv cref)) in Href_prea_ as H.
destruct H as [cs_CmdGen H]; rewrite H; clear H; cbn [snd].
- apply (Update_equiv_idle_idle_E u3 (cnt2Bv c0) (cref2Bv c1)) in Href_prea_ as H.
+ apply (Update_equiv_idle_idle_E u3 (cnt2Bv cnt) (cref2Bv cref)) in Href_prea_ as H.
destruct H as [cs_update H]; rewrite H; clear H; cbn [fst snd].
+ cbn [constant].
+
rewrite /Next_state Href_prea Href_service /State_Eq.
+
specialize (Queue_WR_NF_E_fst (u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
(u24, c, u23), u22, (u20, u21),(u14, (u16, (u18, u19, u17), u15)), u13, rda), wra)) c_req false) as S.
- apply S in NFULL as H; clear S; apply H in Hadr as H'; clear H; rename H' into H.
+ apply S in NFULL as H; clear S; [ | trivial]; apply H in Hadr as H'; clear H; rename H' into H.
destruct H as [cs_requeue' [Hx H]]; destruct Hx as [Hrw [Hwra' Hrda']].
autounfold with get_state.
- apply /andP; split.
- 2 : exact EqReqNil.
apply /andP; split.
2 : unfold EqCmd; by apply BVEq_iff_eq.
apply /andP; split.
@@ -986,7 +1014,7 @@ Section CavaFIFOProperties.
rewrite (surjective_pairing (step RequestQueue' _ _)) H.
cbv [get_addr_RequestQueue] in Hwra'; rewrite Hwra'; clear Hwra'.
cbv [get_addr_RequestQueue] in Hrda'; rewrite Hrda'; clear Hrda'.
- simpl; rewrite Hadr; unfold R; rewrite NF //=.
+ simpl; rewrite Hadr; rewrite NF //=.
apply /andP; split.
{ apply /negPf; apply (@N2Bv_sized_eq_p1_false ADDR_WIDTH rda);
specialize ADDR_WIDTH_pos as Hpos; by move: Hpos => /ltP Hpos. }
@@ -996,11 +1024,12 @@ Section CavaFIFOProperties.
2 : {
rewrite (surjective_pairing (step RequestQueue' _ _)) H.
cbv [get_addr_RequestQueue] in Hrda'; rewrite Hrda'; clear Hrda'.
- simpl; unfold R; rewrite NF //= /EqMem //= andb_true_r.
- rewrite Hrw; autounfold with get_state; rewrite Hadr VectorSpec.map_id.
+ simpl. rewrite NF. rewrite /EqMem //= andb_true_r.
+ rewrite Hrw. autounfold with get_state. rewrite Hadr VectorSpec.map_id.
specialize (@nth_cells_read (Vec Bit REQUEST_WIDTH) ADDR_WIDTH InitMem rda c_req
(Bvect_false REQUEST_WIDTH) c) as H'.
- rewrite H'; exact EqR.
+ rewrite H'.
+ exact EqR.
}
apply /andP; split.
2 : {
@@ -1009,18 +1038,18 @@ Section CavaFIFOProperties.
| |- context [ match ?p with pair _ _ => _ end ] => rewrite (surjective_pairing p)
end; cbn [fst snd].
rewrite //= /Next_cycle_ref.
- set Hc := c1.+1 < PREA_date; dependent destruction Hc;
+ set Hc := cref.+1 < PREA_date; dependent destruction Hc;
apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro.
{ rewrite /cref2Bv //= Bv2N_N2Bv_sized.
2: apply to_nat_lt_pow; rewrite Nat2N.id; apply cref_bound.
rewrite /N2Bv_sized.
- destruct (N.of_nat c1 + 1)%N eqn:Hbug;
+ destruct (N.of_nat cref + 1)%N eqn:Hbug;
[ rewrite N.add_1_r in Hbug; contradict Hbug; apply N.neq_succ_0 | ].
apply BVEq_iff_eq; f_equal; lia.
}
- { specialize (cref_bound c1) as Hc1_bound.
- destruct c1; clear H Hrw Hwra' Hrda' cs_requeue' cs_nextcr; simpl in *.
- apply ltn_gt in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x]; [ | lia].
+ { specialize (cref_bound cref) as Hc1_bound.
+ destruct cref; clear H Hrw Hwra' Hrda' cs_requeue' cs_nextcr; simpl in *.
+ apply gtF_leq in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x]; [ | lia].
assert (m = PREA_date.-1); [ lia | ].
rewrite H in Href_prea; contradict Href_prea; apply not_false_iff_true; by rewrite subn1 eq_refl.
}
@@ -1034,7 +1063,7 @@ Section CavaFIFOProperties.
rewrite /cnt2Bv //=; apply BVEq_iff_eq; f_equal; apply Nat2N.inj_iff.
rewrite /Bv2cnt /Next_cycle //= Bv2N_N2Bv_sized //=.
2: {
- destruct c0; rewrite //= /COUNTER_WIDTH.
+ destruct cnt; rewrite //= /COUNTER_WIDTH.
rewrite WAIT_PW_2_N; apply N_lt_inj; by apply /ltP.
}
set (Hc := _ < WAIT); dependent destruction Hc;
@@ -1047,79 +1076,80 @@ Section CavaFIFOProperties.
end; cbn [fst snd].
by [].
Qed.
+ *)
- Theorem SM_Eq_2b (t : nat) (c_state : State_t) c0 r0 r1
- (c1 : Counter_ref_t) (c_req : Bvector REQUEST_WIDTH) r :
- (c1 + WAIT < PREA_date) = true ->
- (nat_of_ord c1 == PREA_date - 1) = false ->
- let f_state := (Default_arbitrate t).(Implementation_State) in
- let R := HW_Arrival_at t in
- R == [:: r] -> EqReq r c_req -> State_Eq (IDLE c0 c1 (r0 :: r1)) c_state ->
- let '(f_nextstate,(f_cmd_o,f_req_o)) := Next_state R (IDLE c0 c1 (r0 :: r1)) in
- let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step FIFOSM_ c_state (true,c_req) in
- (State_Eq f_nextstate c_nextstate) &&
- (EqCmd f_cmd_o c_cmd_o) && (EqReq f_req_o c_req_o).
+ (* IDLE -> RUNING, start processing request *)
+ Theorem SM_Eq_2b (t : nat) (c_state : State_t) cnt r0 P
+ (cref : Counter_ref_t) (c_req : Bvector REQUEST_WIDTH) arriving_req :
+ (cref + WAIT < PREA_date) = true ->
+ (nat_of_ord cref == PREA_date - 1) = false ->
+ (* let f_state := (Default_arbitrate t).(Implementation_State) in *)
+ let R := Arrival_at t in
+ R == [:: arriving_req] ->
+ EqReq (Some arriving_req) c_req ->
+ let S := IDLE cnt cref (r0 :: P) in
+ State_Eq S c_state ->
+ let '(f_nextstate,f_cmd_o) := Next_state R S in
+ let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step CavaFIFOREF c_state (true,c_req) in
+ (State_Eq f_nextstate c_nextstate) && (EqCmd f_cmd_o c_cmd_o).
Proof.
- intros Href_service Href_prea f_state R NF EqR H; unfold FIFOSM_.
- unfold R in NF; specialize (HaltIfFull t c_state) as NFULL; move: NF => /eqP NF.
+ intros Href_service Href_prea R NF EqR S H; unfold CavaFIFOREF.
+ unfold R in *; clear R.
+ specialize (HaltIfFull t c_state) as NFULL; move: NF => /eqP NF.
unfold State_t in c_state; simpl in c_state; destruct_products.
rewrite NF //= in NFULL; cbv [get_wra get_rda get_fields] in NFULL.
- rename t0 into s, t1 into cnt, t2 into cref, t3 into cr, t4 into wra, t5 into rda.
- rewrite /State_Eq /EqMem in H; autounfold with get_state in H; cbn [fst snd] in H.
+ rename t0 into s, t1 into cnt_, t2 into cref_, t3 into cr, t4 into wra, t5 into rda.
+ rewrite /State_Eq /EqMem in H; unfold S in H.
+ autounfold with get_state in H; cbn [fst snd] in H.
move: H => /andP [/andP [/andP [/andP [EqS EqCnt] EqCref] Mem] HQ].
apply EqQueue_diff_adr in HQ as Hadr.
-
- apply BVEq_iff_eq in EqS, EqCnt, EqCref; subst s cnt cref.
+ apply BVEq_iff_eq in EqS, EqCnt, EqCref; subst s cnt_ cref_.
cbv [LoopInit]; cbn [step fst snd]; simpl_ret; cbv [and2].
- assert ((Sidle STATE_IDLE_VEC && CrefPREA_lt (cref2Bv c1)) = true) as Haux; [
+
+ assert ((Sidle STATE_IDLE_VEC && CrefPREA_lt (cref2Bv cref)) = true) as Haux; [
rewrite //= ; apply CrefPREA_lt_CNT_REF_WAIT;
[ by apply cref_preadate_false in Href_prea | done ] | ]; rewrite Haux; clear Haux; cbn [snd].
rewrite (surjective_pairing (step RequestQueue' _ _)).
+ unfold S in *; clear S.
specialize (Queue_WR_NF_NE_snd ((u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
(u24, c, u23), u22, (u20, u21), (u14, (u16, (u18, u19, u17), u15)),u13, rda), wra))) c_req true) as S.
cbv [get_addr_RequestQueue get_memcells_RequestQueue get_mem_RequestQueue get_memcells] in S.
- apply S in NFULL as S'; [ | done]; clear S; destruct S' as [full_o H].
+ apply S in NFULL as S'; try done; clear S; destruct S' as [full_o H].
rewrite H; clear H; cbn [fst snd].
set tr := nth_default req_null (N.to_nat (Bv2N rda)) _.
- apply NextCR_equiv_IDLE_RUNNING with (c := (u7, (u8, cr))) (cnt := cnt2Bv c0)
- (cref := c1) (tr := tr) in Href_service as H.
+ apply NextCR_equiv_IDLE_RUNNING with (c := (u7, (u8, cr))) (cnt := cnt2Bv cnt)
+ (cref := cref) (tr := tr) in Href_service as H.
2: by apply cref_preadate_false in Href_prea.
destruct H as [cs_nextcr H]; destruct H as [H Htr].
rewrite H; clear H; cbv [fst snd].
- specialize (CmdGen_equiv_idle_to_running u5 (cnt2Bv c0) c1 tr) as S.
+ specialize (CmdGen_equiv_idle_to_running u5 (cnt2Bv cnt) cref tr) as S.
specialize Href_service as Href_service_.
apply S in Href_service; clear S; rename Href_service into H.
2: by apply cref_preadate_false in Href_prea.
destruct H as [cs_CmdGen H]; rewrite H; clear H; cbn [snd].
- specialize (Update_equiv_idle_running u3 (cnt2Bv c0) c1) as S;
+ specialize (Update_equiv_idle_running u3 (cnt2Bv cnt) cref) as S;
apply S in Href_service_ as S'; clear S.
2: by apply cref_preadate_false in Href_prea.
destruct S' as [cs_update H]; rewrite H; clear H; cbn [fst snd].
+ cbn [constant].
+
rewrite /Next_state Href_prea Href_service_ /State_Eq.
- specialize Queue_NF_WR_RD_fst with (c := (u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
- (u24, c, u23), u22, (u20, u21),(u14, (u16, (u18, u19, u17), u15)), u13, rda), wra))) (c_req := c_req) as S.
- apply S in NFULL as H; clear S.
+ specialize (Queue_WR_NF_NE_fst (u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
+ (u24, c, u23), u22, (u20, u21),(u14, (u16, (u18, u19, u17), u15)), u13, rda), wra)) c_req true) as S;
+ apply S in NFULL as H; [ | trivial ]; clear S.
apply H in Hadr as H'; clear H; rename H' into H.
destruct H as [cs_requeue' [Hx H]]; destruct Hx as [Hrw [Hwra' Hrda']].
autounfold with get_state.
apply /andP; split.
- 2: {
- unfold tr; simpl in Mem; move: Mem => /andP [EqReq_r0 Mem].
- rewrite {2}/get_memcells_RequestQueue /get_mem_RequestQueue /get_memcells in Hrw.
- apply (memcell_nch c wra rda c_req req_null) in Hadr as HH.
- rewrite /req_null //= in HH.
- rewrite VectorSpec.map_id /Bvect_false HH in EqReq_r0.
- by rewrite /req_null //=.
- }
- apply /andP; split.
- 2 : unfold EqCmd; by apply BVEq_iff_eq.
+ 2: unfold EqCmd; by apply BVEq_iff_eq.
+
apply /andP; split.
2 : {
repeat lazymatch goal with
@@ -1132,26 +1162,29 @@ Section CavaFIFOProperties.
rewrite VectorSpec.map_id /Bvect_false HH in EqReq_r0.
by rewrite /req_null //=.
}
+
apply /andP; split.
2 : {
rewrite (surjective_pairing (step RequestQueue' _ _)) H Hwra' Hrda'.
simpl; rewrite eq_refl.
- rewrite /Enqueue /R NF.
+ rewrite /Enqueue NF.
simpl in HQ.
- specialize (EqQueue_aux wra rda r0 r1 r) as HH.
+ specialize (EqQueue_aux wra rda r0 P arriving_req) as HH.
apply HH in NFULL as HH'; clear HH; try done.
move: HH'; simpl; intros HH.
by move: HH => /andP [_ HH].
}
+
apply /andP; split.
2 : {
rewrite /EqMem (surjective_pairing (step RequestQueue' _ _)) H Hrda' /Enqueue.
- simpl; unfold R; rewrite NF //=.
+ simpl; rewrite NF //=.
rewrite Hrw eq_refl.
simpl in Mem; move: Mem => /andP [_ Mem].
apply EqMem_rcons; try done.
simpl in HQ; by move: HQ => /andP [_ HQ].
}
+
apply /andP; split.
2 : {
rewrite (surjective_pairing (step RequestQueue' _ _)) H //=.
@@ -1160,34 +1193,25 @@ Section CavaFIFOProperties.
end.
rewrite VectorSpec.map_id; cbn [fst snd].
rewrite /Next_cycle_ref.
- set Hc := c1.+1 < WAIT_REF; dependent destruction Hc;
+ set Hc := cref.+1 < PREA_date; dependent destruction Hc;
apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro.
{ rewrite /cref2Bv //= Bv2N_N2Bv_sized.
- 2: {
- unfold COUNTER_REF_WIDTH; rewrite WAIT_REF_PW_N.
- destruct c1; simpl; apply N_lt_inj; by apply /ltP.
- }
+ 2: apply to_nat_lt_pow; rewrite Nat2N.id; apply cref_bound.
rewrite /N2Bv_sized.
- destruct (N.of_nat c1 + 1)%N eqn:Hbug;
+ destruct (N.of_nat cref + 1)%N eqn:Hbug;
[ rewrite N.add_1_r in Hbug; contradict Hbug; apply N.neq_succ_0 | ].
apply BVEq_iff_eq; f_equal; lia.
}
{ apply cref_preadate_false in Href_prea as Href_prea_.
- destruct c1; simpl in x,e,Hc0,Href_service_,Href_prea,Href_prea_.
+ destruct cref; simpl in x,e,Hc0,Href_service_,Href_prea,Href_prea_.
rewrite /cref2Bv VectorSpec.map_id //= in Href_prea_.
- apply ltn_gt in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x].
- { assert (m = WAIT_REF.-1); [ lia | ].
+ apply gtF_leq in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x].
+ { assert (m = PREA_date.-1); [ lia | ].
rewrite H0 addnC -ltn_subRL in Href_service_.
- rewrite -subn1 ltn_subLR in Href_service_; [ | exact WAIT_REF_pos ].
+ rewrite -subn1 ltn_subLR in Href_service_; [ | exact PREA_date_pos ].
contradict Href_service_; apply /negP.
rewrite -leqNgt leq_eqVlt addnC.
- specialize WAIT_REF_PREA_date as HH.
- apply ltn_trans with (m := PREA_date - WAIT + 1) in HH;
- [ by rewrite HH orb_true_r | ].
- rewrite -subnA.
- { by rewrite ltn_subrL subn_gt0 WAIT_gt_one PREA_date_pos. }
- { exact WAIT_pos. }
- { by rewrite leq_eqVlt PREA_date_WAIT orb_true_r. }
+ apply /orP; right. lia.
}
{ rewrite ltnS in x; contradict x; apply /negP; by rewrite -ltnNge. }
}
@@ -1206,72 +1230,84 @@ Section CavaFIFOProperties.
| |- context [ match ?p with pair _ _ => _ end ] => rewrite (surjective_pairing p)
end; cbn [fst snd]. by [].
Qed.
+ *)
- Theorem SM_Eq_2a (t : nat) (c_state : State_t) c0
- (c1 : Counter_ref_t) (c_req : Bvector REQUEST_WIDTH) r :
- (c1 + WAIT < PREA_date) = true ->
- (nat_of_ord c1 == PREA_date - 1) = false ->
+ Theorem SM_Eq_2a (t : nat) (c_state : State_t) cnt
+ (cref : Counter_ref_t) (c_req : Bvector REQUEST_WIDTH) arriving_req :
+ (cref + WAIT < PREA_date) = true ->
+ (nat_of_ord cref == PREA_date - 1) = false ->
let f_state := (Default_arbitrate t).(Implementation_State) in
- let R := HW_Arrival_at t in
- R == [:: r] -> EqReq r c_req -> State_Eq (IDLE c0 c1 []) c_state ->
- let '(f_nextstate,(f_cmd_o,f_req_o)) := Next_state R (IDLE c0 c1 []) in
- let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step FIFOSM_ c_state (true,c_req) in
- (State_Eq f_nextstate c_nextstate) &&
- (EqCmd f_cmd_o c_cmd_o) && (EqReq f_req_o c_req_o).
- Admitted.
- (* Proof.
- intros Href_service Href_prea f_state R NF EqR H; unfold FIFOSM_.
- unfold R in NF; specialize (HaltIfFull t c_state) as NFULL; move: NF => /eqP NF.
+ let R := Arrival_at t in
+ R == [:: arriving_req] ->
+ EqReq (Some arriving_req) c_req ->
+ let S := IDLE cnt cref [] in
+ State_Eq S c_state ->
+ let '(f_nextstate,f_cmd_o) := Next_state R S in
+ let '(c_nextstate,(_,c_cmd_o,c_req_o)) := step CavaFIFOREF c_state (true,c_req) in
+ (State_Eq f_nextstate c_nextstate) && (EqCmd f_cmd_o c_cmd_o).
+ Proof.
+
+ intros Href_service Href_prea f_state R NF EqR S H; unfold CavaFIFOREF.
+ unfold R in *; clear R.
+ specialize (HaltIfFull t c_state) as NFULL; move: NF => /eqP NF.
unfold State_t in c_state; simpl in c_state; destruct_products.
- rewrite NF //= in NFULL.
- rename t0 into s, t1 into cnt, t2 into cref, t3 into cr, t4 into wra, t5 into rda.
- rewrite /State_Eq /EqMem in H; autounfold with get_state in H; cbn [fst snd] in H.
+ rewrite NF //= in NFULL; cbv [get_wra get_rda get_fields] in NFULL.
+ rename t0 into s, t1 into cnt_, t2 into cref_, t3 into cr, t4 into wra, t5 into rda.
+ rewrite /State_Eq /EqMem in H; unfold S in H.
+
+ (* What we know from State_Eq *)
+ autounfold with get_state in H; cbn [fst snd] in H.
move: H => /andP [/andP [/andP [/andP [EqS EqCnt] EqCref] Mem] Hadr].
+
+ apply BVEq_iff_eq in EqS, EqCnt, EqCref; subst s cnt_ cref_.
+ unfold S in *; clear S.
+
+ cbv [LoopInit]; cbn [step fst snd]; simpl_ret; cbv [and2]; cbn [fst snd].
+
simpl in Hadr.
+ apply BVEq_iff_eq in Hadr.
- apply BVEq_iff_eq in EqS, EqCnt, EqCref, Hadr; subst s cnt cref.
- cbv [LoopInit]; cbn [step fst snd]; simpl_ret.
- cbv [and2].
- assert ((Sidle STATE_IDLE_VEC && CrefPREA_lt (cref2Bv c1)) = true) as Haux; [
+ assert ((Sidle STATE_IDLE_VEC && CrefPREA_lt (cref2Bv cref)) = true) as Haux; [
rewrite //= ; apply CrefPREA_lt_CNT_REF_WAIT;
- [ by apply cref_preadate_false in Href_prea | done ] | ]; rewrite Haux; clear Haux.
- cbn [snd].
+ [ by apply cref_preadate_false in Href_prea | done ] | ]. rewrite Haux; clear Haux.
rewrite (surjective_pairing (step RequestQueue' _ _)).
- specialize (Queue_EMP_WR_snd ((u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
+ specialize (Queue_WR_E_snd ((u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
(u24, c, u23), u22, (u20, u21), (u14, (u16, (u18, u19, u17), u15)),u13, rda), wra))) c_req true) as S.
cbv [get_addr_RequestQueue get_memcells_RequestQueue get_mem_RequestQueue get_memcells] in S.
apply S in Hadr as H; clear S; destruct H as [full_o H].
rewrite H; clear H; cbn [fst snd].
set tr := nth_default req_null (N.to_nat (Bv2N rda)) _.
- specialize NextCR_equiv with (c := (u7, (u8, cr))) (cnt := cnt2Bv c0)
- (cref := cref2Bv c1) (tr := tr) as [cs_nextcr H].
- rewrite H; cbv [fst]; clear H. cbn [snd].
+ specialize NextCR_equiv with (c := (u7, (u8, cr))) (cnt := cnt2Bv cnt)
+ (cref := cref2Bv cref) (tr := tr) as [cs_nextcr H].
+ rewrite H; cbv [fst]; clear H; cbn [snd].
apply cref_preadate_false in Href_prea as Href_prea_.
- apply (CmdGen_equiv_idle_to_idle_E u5 (cnt2Bv c0) (cref2Bv c1)) in Href_prea_ as H.
+ apply (CmdGen_equiv_idle_to_idle_E u5 (cnt2Bv cnt) (cref2Bv cref)) in Href_prea_ as H.
destruct H as [cs_CmdGen H]; rewrite H; clear H; cbn [snd].
- apply (Update_equiv_idle_idle_E u3 (cnt2Bv c0) (cref2Bv c1)) in Href_prea_ as H.
+ apply (Update_equiv_idle_idle_E u3 (cnt2Bv cnt) (cref2Bv cref)) in Href_prea_ as H.
destruct H as [cs_update H]; rewrite H; clear H; cbn [fst snd].
- cbv [get_rda get_wra get_fields] in NFULL.
+ cbn [constant].
+ (* cbv [get_rda get_wra get_fields] in NFULL. *)
rewrite /Next_state Href_prea Href_service /State_Eq.
- specialize Queue_NF_EMP_WR_fst with (c := (u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
- (u24, c, u23), u22, (u20, u21),(u14, (u16, (u18, u19, u17), u15)), u13, rda), wra))) (c_req := c_req) as S.
- apply S in NFULL as H; clear S. apply H in Hadr as H'; clear H; rename H' into H.
+
+ specialize (Queue_WR_NF_E_fst (u11,(u12,(u26, (u27, (u29, (u31, u32, u30), u28)), u25,
+ (u24, c, u23), u22, (u20, u21),(u14, (u16, (u18, u19, u17), u15)), u13, rda), wra)) c_req true) as S.
+ apply S in NFULL as H; clear S; [ | trivial]; apply H in Hadr as H'; clear H; rename H' into H.
destruct H as [cs_requeue' [Hx H]]; destruct Hx as [Hrw [Hwra' Hrda']].
autounfold with get_state.
- apply /andP; split.
- 2 : exact EqReqNil.
apply /andP; split.
2 : unfold EqCmd; by apply BVEq_iff_eq.
apply /andP; split.
2 : {
- rewrite (surjective_pairing (step RequestQueue' _ _)) H Hwra' Hrda'.
- simpl; rewrite Hadr; unfold R; rewrite NF //=.
+ rewrite (surjective_pairing (step RequestQueue' _ _)) H.
+ cbv [get_addr_RequestQueue] in Hwra'; rewrite Hwra'; clear Hwra'.
+ cbv [get_addr_RequestQueue] in Hrda'; rewrite Hrda'; clear Hrda'.
+ simpl; rewrite Hadr; rewrite NF //=.
apply /andP; split.
{ apply /negPf; apply (@N2Bv_sized_eq_p1_false ADDR_WIDTH rda);
specialize ADDR_WIDTH_pos as Hpos; by move: Hpos => /ltP Hpos. }
@@ -1279,8 +1315,9 @@ Section CavaFIFOProperties.
}
apply /andP; split.
2 : {
- rewrite (surjective_pairing (step RequestQueue' _ _)) H Hrda'.
- simpl; unfold R; rewrite NF //= /EqMem //= andb_true_r.
+ rewrite (surjective_pairing (step RequestQueue' _ _)) H.
+ cbv [get_addr_RequestQueue] in Hrda'; rewrite Hrda'; clear Hrda'.
+ simpl; rewrite NF //= /EqMem //= andb_true_r.
rewrite Hrw; autounfold with get_state; rewrite Hadr VectorSpec.map_id.
specialize (@nth_cells_read (Vec Bit REQUEST_WIDTH) ADDR_WIDTH InitMem rda c_req
(Bvect_false REQUEST_WIDTH) c) as H'.
@@ -1288,66 +1325,49 @@ Section CavaFIFOProperties.
}
apply /andP; split.
2 : {
- rewrite (surjective_pairing (step RequestQueue' _ _)) H //=.
+ rewrite (surjective_pairing (step RequestQueue' _ _)) H;
repeat lazymatch goal with
| |- context [ match ?p with pair _ _ => _ end ] => rewrite (surjective_pairing p)
- end.
- cbn [fst snd].
- rewrite /Next_cycle_ref.
- set Hc := c1.+1 < WAIT_REF; dependent destruction Hc;
+ end; cbn [fst snd].
+ rewrite //= /Next_cycle_ref.
+ set Hc := cref.+1 < PREA_date; dependent destruction Hc;
apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro.
{ rewrite /cref2Bv //= Bv2N_N2Bv_sized.
- 2: {
- unfold COUNTER_REF_WIDTH; rewrite WAIT_REF_PW_N.
- destruct c1; simpl; apply N_lt_inj; by apply /ltP.
- }
+ 2: apply to_nat_lt_pow; rewrite Nat2N.id; apply cref_bound.
rewrite /N2Bv_sized.
- destruct (N.of_nat c1 + 1)%N eqn:Hbug;
+ destruct (N.of_nat cref + 1)%N eqn:Hbug;
[ rewrite N.add_1_r in Hbug; contradict Hbug; apply N.neq_succ_0 | ].
apply BVEq_iff_eq; f_equal; lia.
}
- { destruct c1; simpl in x,e,Hc0,Href_prea,Href_prea_,Href_service.
- rewrite /cref2Bv VectorSpec.map_id //= in Href_prea_.
- apply ltn_gt in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x].
- { assert (m = WAIT_REF.-1); [ lia | ].
- rewrite H0 addnC -ltn_subRL in Href_service.
- rewrite -subn1 ltn_subLR in Href_service; [ | exact WAIT_REF_pos ].
- contradict Href_service; apply /negP.
- rewrite -leqNgt leq_eqVlt addnC.
- specialize WAIT_REF_PREA_date as HH.
- apply ltn_trans with (m := PREA_date - WAIT + 1) in HH;
- [ by rewrite HH orb_true_r | ].
- rewrite -subnA.
- { by rewrite ltn_subrL subn_gt0 WAIT_gt_one PREA_date_pos. }
- { exact WAIT_pos. }
- { by rewrite leq_eqVlt PREA_date_WAIT orb_true_r. }
- }
- { rewrite ltnS in x; contradict x; apply /negP; by rewrite -ltnNge. }
+ { specialize (cref_bound cref) as Hc1_bound.
+ destruct cref; clear H Hrw Hwra' Hrda' cs_requeue' cs_nextcr; simpl in *.
+ apply gtF_leq in x; rewrite leq_eqVlt in x; move: x => /orP [/eqP x | x]; [ | lia].
+ assert (m = PREA_date.-1); [ lia | ].
+ rewrite H in Href_prea; contradict Href_prea; apply not_false_iff_true; by rewrite subn1 eq_refl.
}
}
apply /andP; split.
2 : {
- rewrite (surjective_pairing (step RequestQueue' _ _)) H //=.
+ rewrite (surjective_pairing (step RequestQueue' _ _)) H;
repeat lazymatch goal with
| |- context [ match ?p with pair _ _ => _ end ] => rewrite (surjective_pairing p)
- end. cbn [fst snd].
- rewrite /cnt2Bv; apply BVEq_iff_eq; f_equal.
- apply Nat2N.inj_iff.
+ end; cbn [fst snd].
+ rewrite /cnt2Bv //=; apply BVEq_iff_eq; f_equal; apply Nat2N.inj_iff.
rewrite /Bv2cnt /Next_cycle //= Bv2N_N2Bv_sized //=.
2: {
- destruct c0; rewrite //= /COUNTER_WIDTH.
+ destruct cnt; rewrite //= /COUNTER_WIDTH.
rewrite WAIT_PW_2_N; apply N_lt_inj; by apply /ltP.
}
set (Hc := _ < WAIT); dependent destruction Hc;
apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; try rewrite Nat2N.id;
try by rewrite Nat2N.id in x; move: Logic.eq_refl; rewrite {2 3}x; simpl; intro.
}
- rewrite (surjective_pairing (step RequestQueue' _ _)) H //=.
+ rewrite (surjective_pairing (step RequestQueue' _ _)) H;
repeat lazymatch goal with
| |- context [ match ?p with pair _ _ => _ end ] => rewrite (surjective_pairing p)
- end; cbn [fst snd]. by [].
- Qed. *)
-
+ end; cbn [fst snd].
+ by [].
+ Qed.
(* Assuming a non-full regime, i.e., the front-end has yielded a valid request *)
(* If R is non empty than the queue is not full *)
diff --git a/framework/DRAM/Core/Commands.v b/framework/DRAM/Core/Commands.v
index 9b390584608393656b0c62747dba88634ca8f22e..32d22667569ddf388898ba7bf2451e6537be7f6b 100644
--- a/framework/DRAM/Core/Commands.v
+++ b/framework/DRAM/Core/Commands.v
@@ -135,6 +135,12 @@ Section Commands.
Definition isREF (cmd : Command_t) := (cmd.(CKind) == REF).
+ Definition isREF_cmdkind (cmd : Command_kind_t) :=
+ match cmd with
+ | REF => true
+ | _ => false
+ end.
+
Definition ACT_of_req req t := mkCmd t (ACT req).
Definition CAS_of_req req t := mkCmd t ((Kind_of_req req) req).
diff --git a/framework/DRAM/Core/InterfaceSubLayer.v b/framework/DRAM/Core/InterfaceSubLayer.v
index 80475d73bcd3ea53b832c7cb47e6305113cd4218..c1f1c6c503a61b589a6a19a048b33606c6fdd189 100644
--- a/framework/DRAM/Core/InterfaceSubLayer.v
+++ b/framework/DRAM/Core/InterfaceSubLayer.v
@@ -313,7 +313,6 @@ Section InterfaceSubLayer.
rewrite /isNOP //= in Hnop; move: HH => /eqP HH; rewrite HH in Hnop; done.
Qed.
- Check IssueREF.
Lemma command_matches_between_valid_states n IS_prev IS_cur cmd:
cmd.(CDate) = n.+1 -> ~~ isNOP cmd ->
cmd \in (Default_arbitrate n.+1).(Arbiter_Commands) ->
diff --git a/framework/DRAM/Core/Trace.v b/framework/DRAM/Core/Trace.v
index f2ccd080889d2476e4419eda7a9a1bfc9b78ffa7..547120ca86a11d9d1401612840bf32a04b37e33d 100644
--- a/framework/DRAM/Core/Trace.v
+++ b/framework/DRAM/Core/Trace.v
@@ -8,7 +8,6 @@ Section Trace.
Context {SYS_CFG : System_configuration}.
Context {REQESTOR_CFG : Requestor_configuration}.
- (* Context {BK_MAP : BankMap}. *)
Definition isACT_or_PRE cmd :=
(isACT cmd || isPRE cmd).
@@ -129,8 +128,14 @@ Section Trace.
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;
- 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;
+ Cmds_T_REFI_max_dist_ok : forall a, a \in Commands -> isREF a ->
+ exists b, b \in Commands /\ isREF b /\ b.(CDate) <= a.(CDate) + 9 * T_REFI;
+
+ Cmds_T_REFI_density1_ok : forall t,
+ size ([seq cmd <- Commands | isREF cmd && (t <= cmd.(CDate)) && (cmd.(CDate) <= t + 2 * T_REFI)]) <= 16;
+
+ Cmds_T_REFI_density2_ok : forall x,
+ (x+1) - 8 < size ([seq cmd <- Commands | isREF cmd && (cmd.(CDate) <= x * T_REFI)]);
(* ------------------ Exclusively inter-bank constraints ------------------- *)
Cmds_T_FAW_ok : forall a b c d,
diff --git a/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v
index eeafdf586529d74b7d4fd667b2693119a8eab7cd..d98c10780ff3d07e866ebc31b1b314d8d5361032 100644
--- a/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v
+++ b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve.v
@@ -136,12 +136,17 @@ Section TDMShelve.
(* The total number of non-critical requestors *)
Definition NCreq := Treq - SN.
+ Inductive Grant_t :=
+ | NoGrant : Grant_t
+ | SomeGrant : RequestorID_t -> Grant_t
+ | RefreshGrant : Grant_t.
+
Record TDMShelve_internal_state := mkTDMShelve_internal_state {
(* Typical TDM slot and cycle counters *)
Slot : Slot_t;
Counter : TDMShelve_counter_t;
(* Who has the grant to issue commands *)
- Grant : option RequestorID_t;
+ Grant : Grant_t;
(* Both critical and non-critical have associated deadlines *)
Deadlines : { deadline_cnts : seq.seq nat | seq.size deadline_cnts == Treq};
(* A list used to track the arrival of requests *)
@@ -150,6 +155,8 @@ Section TDMShelve.
Slack : { slack_cnts : seq.seq nat | seq.size slack_cnts == SN };
}.
+ (* add another counter to count for cycles elapsed after REF has been issued ? *)
+
#[global] Instance SCH_ST : SchedulerInternalState := mkSIS TDMShelve_internal_state.
(* Pick the first command from a given request *)
@@ -158,8 +165,15 @@ Section TDMShelve.
(req_id : RequestorID_t) : Command_kind_t :=
let f := filter (fun cmd =>
match cmd with
- | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r =>
- r.(Requestor).(ID) == req_id
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r.(Requestor).(ID) == req_id
+ | _ => false
+ end) map in seq.head NOP f.
+
+ Definition Pick_refresh_cmd
+ (map : ReqCmdMap_t) : Command_kind_t :=
+ let f := filter (fun cmd =>
+ match cmd with
+ | PREA | REF => true
| _ => false
end) map in seq.head NOP f.
@@ -168,8 +182,9 @@ Section TDMShelve.
(SS : SystemState_t)
(TDM_st : TDMShelve_internal_state) : Command_kind_t :=
match TDM_st.(Grant) with
- | None => NOP
- | Some requestor_id => Pick_cmd_from_requestorID map requestor_id
+ | NoGrant => NOP
+ | SomeGrant requestor_id => Pick_cmd_from_requestorID map requestor_id
+ | RefreshGrant => Pick_refresh_cmd map
end.
(* ------------------------------------------------------------------ *)
@@ -228,25 +243,6 @@ Section TDMShelve.
Definition checkIfPendingFromSlot (u_map : seq Command_kind_t) (s : Slot_t) :=
checkIfPendingFromID u_map (` (Slot_to_RequestorID s)).
- (* let f := seq.find (fun cmd =>
- match cmd with
- | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r =>
- match r.(Requestor).(ReqSlot) with
- | None => false
- | Some s' => s' == s
- end
- | _ => false
- end
- ) unfiltered_cmd_map in ~~ (f == seq.size unfiltered_cmd_map).
- *)
- (* Wrong because have to look at the actual request and not the mapping *)
- (* Definition filter_diff_bank (s : Slot_t) : seq RequestorID_t :=
- filter (fun req_id =>
- let s_id := Slot_to_RequestorID s in
- let s_bank := Mapping s_id in
- (` req_id == ` s_id) || (NoIntersection (Mapping req_id) s_bank)
- ) All_requestors_sig. *)
-
(* Maybe just look at Arrivals to simplify things ?! *)
Definition PendingReqs u_map (sub_list : seq RequestorID_t) : seq (option RequestorID_t) :=
seq.map (fun x =>
@@ -305,7 +301,7 @@ Section TDMShelve.
exist (fun (s : seq bool) => seq.size s == Treq) (repeat false _) (repeat_size false Treq).
Definition InitSchState (cmd_map : ReqCmdMap_t) := mkTDMShelve_internal_state
- OZSlot OZCycle None InitialDeadlines InitialArrivals InitialSlack.
+ OZSlot OZCycle NoGrant InitialDeadlines InitialArrivals InitialSlack.
(* ------------------------------------------------------------------ *)
(* ----------- Defining update functions ---------------------------- *)
@@ -337,7 +333,7 @@ Section TDMShelve.
end
) None requestors.
- Definition BankFiltering
+ Definition BankFiltering_
(u_map : ReqCmdMap_t)
(TDM_st : TDMShelve_internal_state) : option RequestorID_t :=
let cnt := TDM_st.(Counter) in
@@ -360,43 +356,75 @@ Section TDMShelve.
) else (
EDF TDM_st (filter_diff_bank_ u_map ns_slot)
)
-
end.
- (* Decides who gets the grant grant *)
- Definition UpdateGrant
+ Definition BankFiltering u_map TDM_st :=
+ match BankFiltering_ u_map TDM_st with
+ | None => NoGrant
+ | Some req => SomeGrant req
+ end.
+
+ Definition UpdateGrantRunning
(u_map : ReqCmdMap_t)
(sch_cmd : Command_kind_t)
- (TDM_st : TDMShelve_internal_state) : option RequestorID_t :=
+ (TDM_st : TDMShelve_internal_state) : Grant_t :=
let slt := TDM_st.(Slot) in
let grant := TDM_st.(Grant) in
let cur_slack := getSlackFromSlot TDM_st slt in
let cnt := TDM_st.(Counter) in
if (cnt == OZCycle) then ( (* Beginning of slot -> might abort requests *)
match grant with
- | None => if (u_map == [::]) then None else (BankFiltering u_map TDM_st) (* EDF (implement choice based on slack inside of EDF function) *)
- | Some requestor_id => (* May be preempted or not *)
+ | NoGrant => if (u_map == [::]) then NoGrant else (BankFiltering u_map TDM_st) (* EDF (implement choice based on slack inside of EDF function) *)
+ | SomeGrant requestor_id => (* May be preempted or not *)
match checkIfPendingFromSlot u_map slt with
- | false => if (isCAS_cmdkind sch_cmd) then None else (BankFiltering u_map TDM_st)
+ | false => if (isCAS_cmdkind sch_cmd) then NoGrant else (BankFiltering u_map TDM_st)
| true =>
let preq := Slot_to_RequestorID slt in
let preq_deadl := getDeadlineFromID TDM_st (` preq) in
if (preq_deadl <= SL)
- then (Some preq) (* have to abort ! *) (* Rule 1 *)
- else (
- if (isCAS_cmdkind sch_cmd) then None else (BankFiltering u_map TDM_st)
- )
- (* BankFiltering u_map TDM_st) (Some requestor_id) *)
+ then (SomeGrant preq) (* have to abort ! *) (* Rule 1 *)
+ else (if (isCAS_cmdkind sch_cmd) then NoGrant else (BankFiltering u_map TDM_st))
end
+ | RefreshGrant => RefreshGrant (* should not happen *)
end
) else ( (* Middle of the slot - EDF rules when a scheduling decision comes *)
match grant with (* Rule 4 *)
- | None => if (u_map == [::]) then None else (BankFiltering u_map TDM_st)
- | Some requestor_id =>
- if (isCAS_cmdkind sch_cmd) then None else (Some requestor_id)
+ | NoGrant => if (u_map == [::]) then NoGrant else (BankFiltering u_map TDM_st)
+ | SomeGrant requestor_id =>
+ if (isCAS_cmdkind sch_cmd) then NoGrant else (SomeGrant requestor_id)
+ | RefreshGrant => RefreshGrant (* should not happen *)
end
).
+ (* to-do : account for t_RFC cycles ... *)
+ (* bank machine signal enter of refresh cycle and end *)
+ Definition UpdateGrantRefresh
+ (u_map : ReqCmdMap_t)
+ (sch_cmd : Command_kind_t)
+ (TDM_st : TDMShelve_internal_state) : Grant_t :=
+ match TDM_st.(Grant) with
+ | NoGrant => NoGrant (* Should not happen *)
+ | SomeGrant r => SomeGrant r (* Should not happen *)
+ | RefreshGrant => if (isREF_cmdkind sch_cmd) then NoGrant else RefreshGrant
+ end.
+
+ Definition checkIfREForPREA (unfiltered_cmd_map : seq Command_kind_t) : bool :=
+ let f := seq.find (fun cmd =>
+ match cmd with
+ | PREA | REF => true
+ | _ => false
+ end
+ ) unfiltered_cmd_map in ~~ (f == seq.size unfiltered_cmd_map).
+
+ Definition UpdateGrant
+ (u_map : ReqCmdMap_t)
+ (sch_cmd : Command_kind_t)
+ (TDM_st : TDMShelve_internal_state) : Grant_t :=
+ match TDM_st.(Grant) with
+ | NoGrant | SomeGrant _ => if (checkIfREForPREA u_map) then RefreshGrant else UpdateGrantRunning u_map sch_cmd TDM_st
+ | RefreshGrant => UpdateGrantRefresh u_map sch_cmd TDM_st
+ end.
+
Definition UpdateDeadlines sch_cmd u_map TDM_st :=
exist (fun s => seq.size s == Treq) (seq.map (fun requestor_id =>
(* Cycle counter *)
@@ -458,13 +486,25 @@ Section TDMShelve.
) All_C_requestors) (size_map_iota _ _ _).
Definition UpdatSchState sch_cmd cmd_map (SS : SystemState_t) TDM_st :=
- mkTDMShelve_internal_state
- (Next_slot TDM_st.(Slot) TDM_st.(Counter))
- (Next_cycle TDM_st.(Counter))
- (UpdateGrant cmd_map sch_cmd TDM_st)
- (UpdateDeadlines sch_cmd cmd_map TDM_st)
- (UpdateArrivals sch_cmd cmd_map TDM_st)
- (UpdateSlack sch_cmd TDM_st).
+ let next_grant := UpdateGrant cmd_map sch_cmd TDM_st in
+ match next_grant with
+ | NoGrant | SomeGrant _ =>
+ mkTDMShelve_internal_state
+ (Next_slot TDM_st.(Slot) TDM_st.(Counter))
+ (Next_cycle TDM_st.(Counter))
+ (next_grant)
+ (UpdateDeadlines sch_cmd cmd_map TDM_st)
+ (UpdateArrivals sch_cmd cmd_map TDM_st)
+ (UpdateSlack sch_cmd TDM_st)
+ | RefreshGrant =>
+ mkTDMShelve_internal_state
+ (TDM_st.(Slot))
+ (TDM_st.(Counter))
+ (next_grant)
+ (TDM_st.(Deadlines))
+ (UpdateArrivals sch_cmd cmd_map TDM_st)
+ (TDM_st.(Slack))
+ end.
Lemma eqb_false_Some_inj {T : eqType} (a b : T) :
(a == b) = false -> Some a <> Some b.
@@ -480,26 +520,25 @@ Section TDMShelve.
mkScheduler TDMShelve_schedule _ _ _ InitSchState UpdatSchState.
Next Obligation.
unfold TDMShelve_schedule.
- destruct SCH_ST0.(Grant); [ | reflexivity].
- unfold Pick_cmd_from_requestorID; simpl; reflexivity.
+ destruct SCH_ST0.(Grant); reflexivity.
Defined.
Next Obligation.
unfold TDMShelve_schedule; destruct SCH_ST0.(Grant);
- [ | right; reflexivity ].
- unfold Pick_cmd_from_requestorID; simpl.
+ [ right; reflexivity | | ];
+ unfold Pick_cmd_from_requestorID; simpl;
destruct hd; simpl;
try destruct (_ == r); simpl; try (by left; reflexivity); by right; reflexivity.
Defined.
Next Obligation.
unfold TDMShelve_schedule; destruct SCH_ST0.(Grant);
- [ | left; reflexivity ].
- unfold Pick_cmd_from_requestorID;
+ [ left; reflexivity | | ].
+ all: unfold Pick_cmd_from_requestorID;
induction m; simpl; [ left; reflexivity | ];
destruct IHm as [IHm | IHm];
destruct a; try destruct (_ == r); simpl;
try (by left; assumption);
- try (by right; rewrite in_cons eq_refl orTb).
- all: by right; rewrite in_cons IHm orbT.
+ try (by right; rewrite in_cons eq_refl orTb);
+ by right; rewrite in_cons IHm orbT.
Defined.
(* The one defined in Interface SubLayer *)
diff --git a/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v
index cbf279cdc511cf9d4aad5173423cbd694e60269f..8f7b6bab80547c9a8772844fa4c39d6a8eaf7129 100644
--- a/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v
+++ b/framework/DRAM/Implementations/BM/TDMShelve/TDMShelve_sim.v
@@ -215,10 +215,11 @@ Section TDMShelve_sim.
Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
- Definition computeGrant (g : option RequestorID_t) : option nat :=
+ Definition computeGrant (g : Grant_t) : option nat :=
match g with
- | None => None
- | Some r => Some (proj1_sig r)
+ | NoGrant => None
+ | SomeGrant r => Some (proj1_sig r)
+ | RefreshGrant => None
end.
(* Ignore proofs for testing *)
diff --git a/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v b/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v
index b320c1a74071e333f68a5c908f342f979e5d8a68..8c1159c3c054b2702fb1ac9b028b69677f3321ca 100644
--- a/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v
+++ b/framework/DRAM/Implementations/TS/FIFOREF/FIFOREF.v
@@ -155,7 +155,7 @@ Section FIFOREF.
| [::] => (IDLE c' cref' P', NOP)
| r :: PP => (RUNNING OCycle0 cref' (Enqueue R (Dequeue r P)) r, (PRE r))
end
- else (IDLE c' cref' P', NOP)
+ else (IDLE c' cref' P', NOP) (* Cases 3a/3b *)
| RUNNING c cref P r =>
let P' := Enqueue R P in
let c' := Next_cycle c in