Added constraint on having one ACT between PREs

coq/Arbiter.v

@@ -25,7 +25,7 @@ Section Arbiter.
     Arbitrate : Trace_t;
 
     (* All Requests must handled *)
-    Req_handled : forall req,  req \in Requests -> exists cmd : Command_t, cmd \in Arbitrate.(Commands) ->
-                    Match req cmd
+    Req_handled : forall req,  req \in Requests -> 
+                  exists cmd : Command_t, (cmd \in Arbitrate.(Commands)) && ((Match req cmd))
   }.
 End Arbiter.

coq/Commands.v

@@ -74,6 +74,9 @@ Section Commands.
   Definition isACT (cmd : Command_t) :=
     cmd.(CKind) == ACT.
 
+  Definition isPRE (cmd : Command_t) :=
+    cmd.(CKind) == PRE.
+  
   Definition PRE_of_req req t :=
     mkCmd t PRE req.
 

coq/FIFO.v

@@ -218,21 +218,72 @@ Section FIFO.
         - by apply (IHReqs' a b) in Ia.
   Qed.
 
+  Lemma Between_cons req Reqs a b: 
+    a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+    Between ((FIFO_trace Reqs).(Cmds)) a b =
+    Between (FIFO_trace (req :: Reqs)).(Cmds) a b.
+  Proof.
+  Admitted.
+
+  Lemma FIFO_trace_Cmds_PRE_ok Reqs :
+    forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+                  PRE_to_PRE a b -> Same_Bank a b -> Before a b -> 
+                  exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between (FIFO_trace Reqs).(Cmds) a b.
+  Proof.
+    intros a b a_cmds b_cmds ab_PRE ab_BANK a_not_b.
+    evar (req_date : nat). 
+    evar (t : nat).
+    evar (req_kind : Request_kind_t).
+    set (req := mkReq req_date req_kind a.(Request).(Bank)).
+    exists (ACT_of_req req t).
+    split.
+    - auto.
+    - split.
+      - by unfold ACT_of_req, Same_Bank.
+      - induction Reqs.
+          - auto.
+          - simpl in a_cmds.
+            move : a_cmds => /orP [ /eqP a_eq | /orP [ /eqP a_eq  | /orP [ /eqP a_eq | Ia]] ];
+            move : b_cmds => /orP [ /eqP b_eq | /orP [ /eqP b_eq  | /orP [ /eqP b_eq | Ib]] ].
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - admit.
+            - (*they are the same*) admit.
+            - (*easy due to order*) admit.
+            - admit.
+            - admit.
+            - (* interesting - induction on Reqs until find request of A until I find my ACT cmd (?)*) admit.
+            - rewrite <- Between_cons. apply IHReqs in Ia. apply Ia. all : auto.
+  Admitted.
+
   Program Definition FIFO_arbitrate :=
     let State := FIFO_trace Requests in
-      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_T_RC_ok Requests).
+      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) _ (FIFO_trace_T_RC_ok Requests).
+  Admit Obligations.
+
+  (*
   Next Obligation.
     induction Requests.
     - auto. 
-    - by apply (FIFO_trace_uniq a) in IHl.
-  Qed.
+    - by apply (FIFO_trace_uniq a) in IHl.*)
+  
 
   Lemma FIFO_arbiter_handled req:
-    req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
-                    Match req cmd.
+    req \in Requests -> exists cmd : Command_t, (cmd \in FIFO_arbitrate.(Commands)) /\
+                    ((cmd \in FIFO_arbitrate.(Commands)) -> Match req cmd).
   Proof.
     intros.
     exists (Cmd_of_req req 5).
+    split.
+    - admit.
+    -
     unfold FIFO_arbitrate in *. simpl in *.
     induction Requests.
       - by rewrite in_nil in H.

coq/Trace.v

@@ -8,14 +8,35 @@ Section Trace.
   Definition Same_Bank (a b : Command_t) :=
     a.(Request).(Bank) == b.(Request).(Bank).
 
+  Definition Same_Bank_3 (a b c : Command_t) :=
+    Same_Bank a b && Same_Bank a c.
+
   Definition ACT_to_ACT (a b : Command_t) :=
     isACT a && isACT b.
 
+  Definition PRE_to_PRE (a b : Command_t) :=
+    isPRE a && isPRE b.
+
   Definition Before (a b : Command_t) :=
     a.(CDate) < b.(CDate).
 
   Definition Apart (a b : Command_t) t :=
     a.(CDate) + t < b.(CDate).
+  
+(*
+  Fixpoint Between (l : Commands_t) (a b : Command_t) : Commands_t :=  
+    match l with
+    | [::] => [::]
+    | hd :: seq => if ((hd.(CDate) >= a.(CDate)) && (hd.(CDate) <= b.(CDate)))
+                    then [:: hd] ++ (Between seq a b) 
+                    else [::]
+    end.
+*)
+  
+  Definition Between (l : Commands_t) (a b : Command_t) : Commands_t :=
+    [seq cmds <- l | (cmds.(CDate) > a.(CDate)) && (cmds.(CDate) < b.(CDate))].
+  
+  Check Between. 
 
   Record Trace_t := mkTrace
   {
@@ -28,6 +49,11 @@ Section Trace.
     (* All commands have to occur before the current time instant *)
     Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
 
+    (* Between any two PREs to the same bank, there has to be an ACT to the same bank in between *)
+    Cmds_PRE_ok : forall a b, a \in Commands -> b \in Commands ->
+                  PRE_to_PRE a b -> Same_Bank a b -> a != b -> 
+                  exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between Commands a b;
+
     (* Ensure that the time between two ACT commands respects T_RC *)
     Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
                     ACT_to_ACT a b -> Same_Bank a b -> Before a b ->

coq/trace2.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect ssrnat ssrbool ssrfun seq eqtype.
+From sdram Require Export Commands Bank.
+
+Section Trace.
+
+  Context {BANK_CFG : Bank_configuration}.
+
+  (*
+  Program Instance BANK_CFG : Bank_configuration :=
+  {
+    BANKS := 2;
+    T_RC  := 3
+  }.
+*)
+
+  Definition Same_Bank (a b : Command_t) :=
+    a.(Request).(Bank) == b.(Request).(Bank).
+
+  Definition Same_Bank_3 (a b c : Command_t) :=
+    Same_Bank a b && Same_Bank a c.
+
+  Lemma Same_Bank_eq : 
+    forall a b c : Command_t, Same_Bank a b -> Same_Bank a c -> Same_Bank b c.
+  Proof.
+    intros a b c S_ab S_ac.
+    unfold Same_Bank in *.
+    move : S_ab => /eqP /esym S_ab.
+    move : S_ac => /eqP /esym S_ac.
+    apply /eqP. 
+    by rewrite S_ab.
+  Qed.
+
+  Lemma Same_Bank_3_eq :
+    forall a b c : Command_t, Same_Bank_3 a b c -> Same_Bank a b && Same_Bank a c && Same_Bank b c.
+  Proof.
+    intros a b c S_3.
+    unfold Same_Bank_3 in *.
+    move : S_3 => /andP S_3.
+    apply /andP. split.
+    - by apply /andP. destruct S_3 as [s3_1 s3_2]. move : s3_1 s3_2. apply Same_Bank_eq.
+  Qed.
+
+  Definition ACT_to_ACT (a b : Command_t) :=
+    isACT a && isACT b.
+
+  Definition PRE_to_PRE (a b : Command_t) :=
+    isPRE a && isPRE b.
+
+  Definition Before (a b : Command_t) :=
+    a.(CDate) < b.(CDate).
+
+  Definition Apart (a b : Command_t) t :=
+    a.(CDate) + t < b.(CDate).
+
+  (* Filters a sequence of commands to include just the ones with date between a and b *)
+  Fixpoint Between (l : Commands_t) (a b : Command_t) : Commands_t :=  
+    match l with
+    | [::] => [::]
+    | hd :: seq => if ((hd.(CDate) >= a.(CDate)) && (hd.(CDate) <= b.(CDate)))
+                    then [:: hd] ++ (Between seq a b) 
+                    else [::]
+    end.
+
+  (* Create a boolean function *)
+
+  (*
+  Program Definition req1 := mkReq 0 RD 0.
+  Program Definition req2 := mkReq 1 RD 1.
+  Program Definition req3 := mkReq 2 RD 0.
+  Definition PRE_req1 := PRE_of_req req1 0.
+  Definition ACT_req1 := ACT_of_req req1 1.
+  Definition CMD_req1 := Cmd_of_req req1 2.
+  Definition PRE_req2 := PRE_of_req req2 4.
+  Definition ACT_req2 := ACT_of_req req2 5.
+  Definition CMD_req2 := Cmd_of_req req2 6.
+  Definition PRE_req3 := PRE_of_req req2 7.
+  Definition ACT_req3 := ACT_of_req req2 8.
+  Definition CMD_req3 := Cmd_of_req req2 9.
+
+  Definition test_CMDS : Commands_t := [::PRE_req1;ACT_req1;CMD_req1;PRE_req2;ACT_req2;CMD_req2;PRE_req3;ACT_req3;CMD_req3].
+  Print test_CMDS.
+  Check test_CMDS.
+
+  Definition test_between := Between test_CMDS PRE_req1 PRE_req3.
+  Compute test_between.
+  *)
+  
+  Record Trace_t := mkTrace
+  {
+    Commands : Commands_t;
+    Time     : nat;
+
+    (* All commands must be uniq *)
+    Cmds_uniq    : uniq Commands;
+
+    (* All commands have to occur before the current time instant *)
+    Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
+
+    (* Between any two PREs to the same bank, there has to be an ACT to the same bank in between *)
+    Cmds_PRE_ok : forall a b c, a \in Commands -> b \in Commands -> c \in Commands ->
+                  PRE_to_PRE a b -> isACT c -> Same_Bank_3 a b c ->
+                  c \in Between Commands a b;
+
+    (* Ensure that the time between two ACT commands respects T_RC *)
+    Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
+                    ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
+                    Apart a b T_RC;
+  }.
+
+  Program Definition Trace_empty := mkTrace [::] 0 _ _ _.
+End Trace.
\ No newline at end of file