Add RAM semantics to HTL and fix proof

4 files changed, 132 insertions, 18 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 1949785..b83d313 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -51,6 +51,14 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
     In p0 (map fst (Maps.PTree.elements m)) ->
     Z.pos p0 <= Integers.Int.max_unsigned.
 
+Record ram := mk_ram {
+  ram_mem: reg;
+  ram_addr: reg;
+  ram_wr_en: reg;
+  ram_d_in: reg;
+  ram_d_out: reg;
+}.
+
 Record module: Type :=
   mkmodule {
     mod_params : list reg;
@@ -67,7 +75,7 @@ Record module: Type :=
     mod_clk : reg;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
-    mod_ram : option (reg * reg * reg * reg);
+    mod_ram : option ram;
     mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
   }.
 
@@ -112,12 +120,35 @@ Inductive state : Type :=
            (m : module)
            (args : list value), state.
 
+Inductive exec_ram:
+  Verilog.reg_associations -> Verilog.arr_associations ->
+  option ram ->
+  Verilog.reg_associations -> Verilog.arr_associations ->
+  Prop :=
+| exec_ram_Some_write:
+    forall ra ar ram d_in addr,
+      (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 1) ->
+      (Verilog.assoc_blocking ra)!(ram_d_in ram) = Some d_in ->
+      (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr ->
+      exec_ram ra ar (Some ram) ra
+               (Verilog.nonblock_arr (ram_mem ram) (valueToNat addr) ar d_in)
+| exec_ram_Some_load:
+    forall ra ar ram addr v_d_out,
+      (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 0) ->
+      (Verilog.assoc_blocking ra)!(ram_addr ram) = Some addr ->
+      Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem ram) (valueToNat addr) = Some v_d_out ->
+      exec_ram ra ar (Some ram) (Verilog.nonblock_reg (ram_d_out ram) ra v_d_out) ar
+| exec_ram_None:
+    forall r a,
+      exec_ram r a None r a.
+
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
     forall g m st sf ctrl data
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
+      basr3 basa3 nasr3 nasa3
       asr' asa'
       f pstval,
       asr!(mod_reset m) = Some (ZToValue 0) ->
@@ -138,8 +169,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         data
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
-      asr' = Verilog.merge_regs nasr2 basr2 ->
-      asa' = Verilog.merge_arrs nasa2 basa2 ->
+      exec_ram
+        (Verilog.mkassociations basr2 nasr2)
+        (Verilog.mkassociations basa2 nasa2)
+        (mod_ram m)
+        (Verilog.mkassociations basr3 nasr3)
+        (Verilog.mkassociations basa3 nasa3) ->
+      asr' = Verilog.merge_regs nasr3 basr3 ->
+      asa' = Verilog.merge_arrs nasa3 basa3 ->
       asr'!(m.(mod_st)) = Some (posToValue pstval) ->
       Z.pos pstval <= Integers.Int.max_unsigned ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 59ff55b..e3b0147 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1030,6 +1030,7 @@ Section CORRECTNESS.
 
   Ltac tac0 :=
     match goal with
+    | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor
     | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs
     | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr
     | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge
@@ -1701,7 +1702,7 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: crush.
+      all: try constructor; crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
@@ -1981,7 +1982,7 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: crush.
+      all: try constructor; crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
@@ -2229,7 +2230,7 @@ Section CORRECTNESS.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: crush.
+      all: try constructor; crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
@@ -2463,7 +2464,7 @@ Section CORRECTNESS.
       eapply eval_cond_correct; eauto. intros.
       intros. eapply RTL.max_reg_function_use. apply H22. auto.
       econstructor. auto.
-      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+      simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl.
       apply AssocMap.gss.
 
       inv MARR. inv CONST.
@@ -2480,7 +2481,7 @@ Section CORRECTNESS.
       eapply eval_cond_correct; eauto. intros.
       intros. eapply RTL.max_reg_function_use. apply H22. auto.
       econstructor. auto.
-      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+      simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl.
       apply AssocMap.gss.
 
       inv MARR. inv CONST.
@@ -2535,7 +2536,7 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
 
-      constructor. constructor.
+      constructor. constructor. constructor.
 
       unfold state_st_wf in WF; big_tac; eauto.
       destruct wf as [HCTRL HDATA]. apply HCTRL.
@@ -2564,6 +2565,7 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor. constructor. constructor.
       constructor. constructor. constructor.
+      constructor.
 
       unfold state_st_wf in WF; big_tac; eauto.
 
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index a845435..6219127 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -32,6 +32,7 @@ Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
 Require Import vericert.hls.HTL.
 Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.Array.
 
 Local Open Scope positive.
 
@@ -66,6 +67,43 @@ Definition transf_maps (st addr d_in d_out wr: reg)
     end
   end.
 
+Lemma transf_maps_wf :
+  forall st addr d_in d_out wr n d c n' d' c' i,
+  map_well_formed c /\ map_well_formed d ->
+  transf_maps st addr d_in d_out wr (n, d, c) i = (n', d', c') ->
+  map_well_formed c' /\ map_well_formed d'.
+Proof.
+  unfold map_well_formed; simplify;
+    repeat destruct_match;
+    match goal with | H: (_, _, _) = (_, _, _) |- _ => inv H end; eauto;
+      simplify.
+  apply H2.
+  exploit list_in_map_inv; eauto; intros.
+  inv H0. destruct x. inv H3. simplify.
+  replace p with (fst (p, s)) by auto.
+  apply in_map.
+  apply PTree.elements_correct.
+  apply PTree.elements_complete in H4.
+  Admitted.
+
+Definition set_mod_datapath d c wf m :=
+  mkmodule (mod_params m)
+           d
+           c
+           (mod_entrypoint m)
+           (mod_st m)
+           (mod_stk m)
+           (mod_stk_len m)
+           (mod_finish m)
+           (mod_return m)
+           (mod_start m)
+           (mod_reset m)
+           (mod_clk m)
+           (mod_scldecls m)
+           (mod_arrdecls m)
+           (mod_ram m)
+           wf.
+
 Lemma is_wf:
   forall A nc nd,
 @map_well_formed A nc /\ @map_well_formed A nd.
@@ -98,7 +136,7 @@ Definition transf_module (m: module): module :=
                (AssocMap.set d_in (None, VScalar 32)
                 (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls)))))
              (AssocMap.set m.(mod_stk) (None, VArray 32 (2 ^ Nat.log2_up m.(mod_stk_len)))%nat m.(mod_arrdecls))
-             (Some (addr, d_in, d_out, wr_en))
+             (Some (mk_ram (mod_stk m) addr wr_en d_in d_out))
              (is_wf _ nc nd)
   end.
 
@@ -116,11 +154,27 @@ Definition transf_fundef := transf_fundef transf_module.
 Definition transf_program (p : program) :=
   transform_program transf_fundef p.
 
+Inductive match_assocmaps : assocmap -> assocmap -> Prop :=
+  match_assocmap: forall rs rs',
+    (forall r v, rs!r = Some v -> rs'!r = Some v) ->
+    match_assocmaps rs rs'.
+
+Inductive match_arrs : assocmap_arr -> assocmap_arr -> Prop :=
+  match_assocmap_arr: forall ar ar',
+    (forall s arr arr',
+      ar!s = Some arr ->
+      ar'!s = Some arr' ->
+      forall addr,
+        array_get_error addr arr = array_get_error addr arr') ->
+    match_arrs ar ar'.
+
 Inductive match_states : HTL.state -> HTL.state -> Prop :=
 | match_state :
-    forall res m st asr asa,
+    forall res m st asr asr' asa asa'
+           (ASSOC: match_assocmaps asr asr')
+           (ARRS: match_arrs asa asa'),
       match_states (HTL.State res m st asr asa)
-                   (HTL.State res (transf_module m) st asr asa)
+                   (HTL.State res (transf_module m) st asr' asa')
 | match_returnstate :
     forall res v,
       match_states (HTL.Returnstate res v) (HTL.Returnstate res v)
@@ -148,6 +202,27 @@ Section CORRECTNESS.
 
   Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
 
+  Lemma transf_maps_preserves_behaviour :
+    forall m m' s addr d_in d_out wr n n' t stk rs ar d' c' wf' i,
+      m' = set_mod_datapath d' c' wf' m ->
+      transf_maps m.(mod_st) addr d_in d_out wr (n, mod_datapath m, mod_controllogic m) i = (n', d', c') ->
+      step ge (State stk m s rs ar) t (State stk m s rs ar) ->
+      forall R1,
+        match_states (State stk m s rs ar) R1 ->
+        exists R2, step ge R1 t R2 /\ match_states (State stk m s rs ar) R2.
+  Proof.
+    Admitted.
+
+  Lemma fold_transf_maps_preserves_behaviour :
+    forall m m' s addr d_in d_out wr n' t stk rs ar d' c' wf' l rs' ar',
+      fold_left (transf_maps m.(mod_st) addr d_in d_out wr) l
+                  (max_pc_function m + 1, m.(mod_datapath), m.(mod_controllogic)) = (n', d', c') ->
+      m' = set_mod_datapath d' c' wf' m ->
+      step ge (State stk m s rs ar) t (State stk m s rs' ar') ->
+      exists R2, step ge (State stk m' s rs ar) t R2 /\ match_states (State stk m s rs' ar') R2.
+  Proof.
+    Admitted.
+
   Theorem transf_step_correct:
     forall (S1 : state) t S2,
       step ge S1 t S2 ->
@@ -155,14 +230,14 @@ Section CORRECTNESS.
           match_states S1 R1 ->
             exists R2, Smallstep.plus step ge R1 t R2 /\ match_states S2 R2.
   Proof.
+    pose proof fold_transf_maps_preserves_behaviour.
     induction 1.
-    - intros. inv H11.
-      unfold transf_module.
+    - exploit fold_transf_maps_preserves_behaviour. intros. inv H13. inv ASSOC. inv ARRS.
       econstructor.
       econstructor.
       eapply Smallstep.plus_one.
-      econstructor.
-      simplify.
-      all: repeat destruct_match; try assumption; simplify.
+      econstructor; unfold transf_module; repeat destruct_match; try solve [crush].
+      + simplify.
+
 
 End CORRECTNESS.
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index cf36d27..3defe9c 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -52,7 +52,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in
   let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in
   match m.(HTL.mod_ram) with
-  | Some (addr, d_in, d_out, wr_en) =>
+  | Some (mk_ram ram addr wr_en d_in d_out) =>
     let body :=
         Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1)))
                                                   (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint))))