Update RAM generation proofs

3 files changed, 472 insertions, 70 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index b83d313..2e4987d 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -53,6 +53,7 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
 
 Record ram := mk_ram {
   ram_mem: reg;
+  ram_en: reg;
   ram_addr: reg;
   ram_wr_en: reg;
   ram_d_in: reg;
@@ -125,9 +126,16 @@ Inductive exec_ram:
   option ram ->
   Verilog.reg_associations -> Verilog.arr_associations ->
   Prop :=
+| exec_ram_Some_idle:
+    forall ra ar ram,
+    (Verilog.assoc_blocking ra)!(ram_en ram) = Some (ZToValue 0) ->
+    exec_ram ra ar (Some ram) ra ar
 | exec_ram_Some_write:
-    forall ra ar ram d_in addr,
-      (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some (ZToValue 1) ->
+    forall ra ar ram d_in addr en wr_en,
+      en <> ZToValue 0 ->
+      wr_en <> ZToValue 0 ->
+      (Verilog.assoc_blocking ra)!(ram_en ram) = Some en ->
+      (Verilog.assoc_blocking ra)!(ram_wr_en ram) = Some wr_en ->
       (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
@@ -170,8 +178,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
       exec_ram
-        (Verilog.mkassociations basr2 nasr2)
-        (Verilog.mkassociations basa2 nasa2)
+        (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap)
+        (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m))
         (mod_ram m)
         (Verilog.mkassociations basr3 nasr3)
         (Verilog.mkassociations basa3 nasa3) ->
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index 6219127..fa4946f 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -16,6 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+Require Import Coq.micromega.Lia.
+
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Globalenvs.
@@ -39,27 +41,76 @@ Local Open Scope positive.
 Definition max_pc_function (m: module) :=
   List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1.
 
-Definition transf_maps (st addr d_in d_out wr: reg)
-           (dc: node * PTree.t stmnt * PTree.t stmnt) i :=
+Fixpoint max_reg_expr (e: expr) :=
+  match e with
+  | Vlit _ => 1
+  | Vvar r => r
+  | Vvari r e => Pos.max r (max_reg_expr e)
+  | Vrange r e1 e2 => Pos.max r (Pos.max (max_reg_expr e1) (max_reg_expr e2))
+  | Vinputvar r => r
+  | Vbinop _ e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+  | Vunop _ e => max_reg_expr e
+  | Vternary e1 e2 e3 => Pos.max (max_reg_expr e1) (Pos.max (max_reg_expr e2) (max_reg_expr e3))
+  end.
+
+Fixpoint max_reg_stmnt (st: stmnt) :=
+  match st with
+  | Vskip => 1
+  | Vseq s1 s2 => Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2)
+  | Vcond e s1 s2 =>
+    Pos.max (max_reg_expr e)
+            (Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2))
+  | Vcase e stl None => Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl)
+  | Vcase e stl (Some s) =>
+    Pos.max (max_reg_stmnt s)
+            (Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl))
+  | Vblock e1 e2 => Pos.max (max_reg_expr e2) (max_reg_expr e2)
+  | Vnonblock e1 e2 => Pos.max (max_reg_expr e2) (max_reg_expr e2)
+  end
+with max_reg_stmnt_expr_list (stl: stmnt_expr_list) :=
+  match stl with
+  | Stmntnil => 1
+  | Stmntcons e s stl' =>
+    Pos.max (max_reg_expr e)
+            (Pos.max (max_reg_stmnt s)
+                     (max_reg_stmnt_expr_list stl'))
+  end.
+
+Definition max_list := fold_right Pos.max 1.
+
+Definition max_stmnt_tree t :=
+  PTree.fold (fun i _ st => Pos.max (max_reg_stmnt st) i) t 1.
+
+Definition max_reg_module m :=
+  Pos.max (max_list (mod_params m))
+   (Pos.max (max_stmnt_tree (mod_datapath m))
+     (Pos.max (max_stmnt_tree (mod_controllogic m))
+       (Pos.max (mod_st m)
+         (Pos.max (mod_stk m)
+           (Pos.max (mod_finish m)
+             (Pos.max (mod_return m)
+               (Pos.max (mod_start m)
+                 (Pos.max (mod_reset m) (mod_clk m))))))))).
+
+Definition transf_maps ram i (dc: node * PTree.t stmnt * PTree.t stmnt) :=
   match dc with
   | (n, d, c) =>
     match PTree.get i d, PTree.get i c with
     | Some d_s, Some c_s =>
       match d_s with
       | Vnonblock (Vvari r e1) e2 =>
-        let nd := Vseq (Vnonblock (Vvar wr) (Vlit (ZToValue 1)))
-                       (Vseq (Vnonblock (Vvar d_in) e2)
-                             (Vnonblock (Vvar addr) e1))
+        let nd := Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1)))
+                       (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2)
+                             (Vnonblock (Vvar (ram_addr ram)) e1))
         in
         (n, PTree.set i nd d, c)
       | Vnonblock e1 (Vvari r e2) =>
-        let nd := Vseq (Vnonblock (Vvar wr) (Vlit (ZToValue 0)))
-                       (Vnonblock (Vvar addr) e2)
+        let nd := Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0)))
+                       (Vnonblock (Vvar (ram_addr ram)) e2)
         in
-        let aout := Vnonblock e1 (Vvar d_out) in
-        let redirect := Vnonblock (Vvar st) (Vlit (posToValue n)) in
-        (n+1, PTree.set i nd
-                        (PTree.set n aout d),
+        let aout := Vnonblock e1 (Vvar (ram_d_out ram)) in
+        let redirect := Vnonblock (Vvar (ram_mem ram)) (Vlit (posToValue n)) in
+        (n+1, PTree.set i nd (PTree.set n aout d),
          PTree.set i redirect (PTree.set n c_s c))
       | _ => dc
       end
@@ -68,9 +119,9 @@ Definition transf_maps (st addr d_in d_out wr: reg)
   end.
 
 Lemma transf_maps_wf :
-  forall st addr d_in d_out wr n d c n' d' c' i,
+  forall ram 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') ->
+  transf_maps ram i (n, d, c) = (n', d', c') ->
   map_well_formed c' /\ map_well_formed d'.
 Proof.
   unfold map_well_formed; simplify;
@@ -84,7 +135,7 @@ Proof.
   apply in_map.
   apply PTree.elements_correct.
   apply PTree.elements_complete in H4.
-  Admitted.
+  Abort.
 
 Definition set_mod_datapath d c wf m :=
   mkmodule (mod_params m)
@@ -109,16 +160,26 @@ Lemma is_wf:
 @map_well_formed A nc /\ @map_well_formed A nd.
 Admitted.
 
+Definition max_pc {A: Type} (m: PTree.t A) :=
+  fold_right Pos.max 1%positive (map fst (PTree.elements m)).
+
+Definition transf_code ram d c :=
+  match fold_right (transf_maps ram)
+                   (max_pc c + 1, d, c)
+                   (map fst (PTree.elements d)) with
+  | (_, d', c') => (d', c')
+  end.
+
 Definition transf_module (m: module): module :=
-  let addr := m.(mod_clk)+1 in
-  let d_in := m.(mod_clk)+2 in
-  let d_out := m.(mod_clk)+3 in
-  let wr_en := m.(mod_clk)+4 in
-  match fold_left (transf_maps m.(mod_st) addr d_in d_out wr_en)
-                  (map fst (PTree.elements m.(mod_datapath)))
-                  (max_pc_function m + 1, m.(mod_datapath), m.(mod_controllogic))
-  with
-  | (_, nd, nc) =>
+  let max_reg := max_reg_module m in
+  let addr := max_reg+1 in
+  let en := max_reg+2 in
+  let d_in := max_reg+3 in
+  let d_out := max_reg+4 in
+  let wr_en := max_reg+5 in
+  let ram := mk_ram (mod_stk m) en addr d_in d_out wr_en in
+  match transf_code ram (mod_datapath m) (mod_controllogic m) with
+  | (nd, nc) =>
     mkmodule m.(mod_params)
              nd
              nc
@@ -136,19 +197,10 @@ 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 (mk_ram (mod_stk m) addr wr_en d_in d_out))
+             (Some ram)
              (is_wf _ nc nd)
   end.
 
-Lemma fold_has_value:
-  forall st d c addr d_in d_out wr_en mst data ctrl l n dstm cstm,
-    data ! st = Some dstm ->
-    ctrl ! st = Some cstm ->
-    fold_left (transf_maps st addr d_in d_out wr_en) l
-              (mst, data, ctrl) = (n, d, c) ->
-    exists dstm' cstm', d ! st = Some dstm' /\ c ! st = Some cstm'.
-Admitted.
-
 Definition transf_fundef := transf_fundef transf_module.
 
 Definition transf_program (p : program) :=
@@ -184,6 +236,175 @@ Inductive match_states : HTL.state -> HTL.state -> Prop :=
       (HTL.Callstate nil (transf_module m) nil).
 Hint Constructors match_states : htlproof.
 
+Inductive match_reg_assocs : reg_associations -> reg_associations -> Prop :=
+  match_reg_association:
+    forall rab rab' ran ran',
+      match_assocmaps rab rab' ->
+      match_assocmaps ran ran' ->
+      match_reg_assocs (mkassociations rab ran) (mkassociations rab' ran').
+
+Inductive match_arr_assocs : arr_associations -> arr_associations -> Prop :=
+  match_arr_association:
+    forall rab rab' ran ran',
+      match_arrs rab rab' ->
+      match_arrs ran ran' ->
+      match_arr_assocs (mkassociations rab ran) (mkassociations rab' ran').
+
+Ltac mgen_crush := crush; eauto with mgen.
+
+Lemma match_assocmaps_equiv : forall a, match_assocmaps a a.
+Proof. constructor; auto. Qed.
+Hint Resolve match_assocmaps_equiv : mgen.
+
+Lemma match_arrs_equiv : forall a, match_arrs a a.
+Proof. constructor; mgen_crush. Qed.
+Hint Resolve match_arrs_equiv : mgen.
+
+Lemma match_reg_assocs_equiv : forall a, match_reg_assocs a a.
+Proof. destruct a; constructor; mgen_crush. Qed.
+Hint Resolve match_reg_assocs_equiv : mgen.
+
+Lemma match_arr_assocs_equiv : forall a, match_arr_assocs a a.
+Proof. destruct a; constructor; mgen_crush. Qed.
+Hint Resolve match_arr_assocs_equiv : mgen.
+
+Definition forall_ram (P: reg -> Prop) ram :=
+  P (ram_mem ram)
+  /\ P (ram_en ram)
+  /\ P (ram_addr ram)
+  /\ P (ram_wr_en ram)
+  /\ P (ram_d_in ram)
+  /\ P (ram_d_out ram).
+
+Definition exec_all d_s c_s r rs1 ar1 rs4 ar4 :=
+  exists f rs2 ar2 rs3 ar3,
+    stmnt_runp f rs1 ar1 d_s rs2 ar2
+    /\ stmnt_runp f rs2 ar2 c_s rs3 ar3
+    /\ exec_ram
+         (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap)
+         (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m))
+         r rs4 ar4.
+
+Definition behaviour_correct d c r d' c' r' :=
+  forall rs1 ar1 rs4 ar4 d_s c_s i,
+    PTree.get i d = Some d_s ->
+    PTree.get i c = Some c_s ->
+    exec_all d_s c_s r rs1 ar1 rs4 ar4 ->
+    exists d_s' c_s' trs4 tar4,
+      PTree.get i d' = Some d_s'
+      /\ PTree.get i c' = Some c_s'
+      /\ exec_all d_s' c_s' r' rs1 ar1 trs4 tar4
+      /\ match_reg_assocs rs4 trs4
+      /\ match_arr_assocs ar4 tar4.
+
+Lemma behaviour_correct_equiv :
+  forall d c r, behaviour_correct d c r d c r.
+Proof. intros; unfold behaviour_correct; repeat (eexists; mgen_crush). Qed.
+Hint Resolve behaviour_correct_equiv : mgen.
+
+Lemma stmnt_runp_gtassoc :
+  forall st rs1 ar1 rs2 ar2 f,
+    stmnt_runp f rs1 ar1 st rs2 ar2 ->
+    forall p v,
+      max_reg_stmnt st < p ->
+      (assoc_nonblocking rs1)!p = None ->
+      exists rs2',
+        stmnt_runp f (nonblock_reg p rs1 v) ar1 st rs2' ar2
+        /\ match_reg_assocs rs2 rs2'
+        /\ (assoc_nonblocking rs2')!p = Some v.
+Proof.
+  Admitted.
+(*  induction 1; simplify.
+  - repeat econstructor. destruct (nonblock_reg p ar v) eqn:?; destruct ar. simplify.
+    constructor. inv Heqa. mgen_crush.
+    inv Heqa. constructor. intros.
+  - econstructor; [apply IHstmnt_runp1; lia | apply IHstmnt_runp2; lia].
+  - econstructor; eauto; apply IHstmnt_runp; lia.
+  - eapply stmnt_runp_Vcond_false; eauto; apply IHstmnt_runp; lia.
+  - econstructor; simplify; eauto; apply IHstmnt_runp;
+    destruct def; lia.
+  - eapply stmnt_runp_Vcase_match; simplify; eauto; apply IHstmnt_runp;
+    destruct def; lia.
+  - eapply stmnt_runp_Vcase_default; simplify; eauto; apply IHstmnt_runp; lia.
+  -*)
+
+Lemma transf_not_changed :
+  forall ram n d c i d_s c_s,
+    (forall e1 e2 r, d_s <> Vnonblock (Vvari r e1) e2) ->
+    (forall e1 e2 r, d_s <> Vnonblock e1 (Vvari r e2)) ->
+    d!i = Some d_s ->
+    c!i = Some c_s ->
+    transf_maps ram i (n, d, c) = (n, d, c).
+Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed.
+
+Lemma transf_store :
+  forall ram n d c i c_s r e1 e2,
+    d!i = Some (Vnonblock (Vvari r e1) e2) ->
+    c!i = Some c_s ->
+    exists n' d' c' d_s' c_s',
+      transf_maps ram i (n, d, c) = (n', d', c')
+      /\ d'!i = d_s'
+      /\ c'!i = c_s'
+      /\ exec_all d_s' c_s'.
+Proof.
+  unfold transf_maps; intros; do 3 econstructor; repeat destruct_match; mgen_crush.
+  unfold behaviour_correct. simplify.
+  destruct (Pos.eq_dec i i0). subst.
+    unfold exec_all in *.
+  inv H1. inv H2. inv H1. inv H2. inv H1. inv H2. inv H3. inv H4.
+  rewrite Heqo in H.
+  rewrite Heqo0 in H0. inv H. inv H0.
+  inv H1.
+  simplify.
+  do 4 econstructor.
+  econstructor.
+  apply PTree.gss.
+  econstructor.
+  eauto.
+  split.
+  do 5 econstructor.
+  split. repeat econstructor.
+  simplify. eauto. simplify.
+  inv H6.
+  split.
+Qed.
+
+Lemma transf_load :
+  forall stk addr d_in d_out wr_en n d c d' c' i c_s r e1 e2 aout nd redirect,
+    (forall e2 r, e1 <> Vvari r e2) ->
+    d!i = Some (Vnonblock e1 (Vvari r e2)) ->
+    c!i = Some c_s ->
+    d!n = None ->
+    c!n = None ->
+    nd = Vseq (Vnonblock (Vvar wr_en) (Vlit (ZToValue 0)))
+              (Vnonblock (Vvar addr) e2) ->
+    aout = Vnonblock e1 (Vvar d_out) ->
+    redirect = Vnonblock (Vvar stk) (Vlit (posToValue n)) ->
+    d' = PTree.set i nd (PTree.set n aout d) ->
+    c' = PTree.set i redirect (PTree.set n c_s c) ->
+    (transf_maps stk addr d_in d_out wr_en i (n, d, c) = (n+1, d', c')
+     ).
+Proof. unfold transf_maps; intros; repeat destruct_match; crush. Qed.
+
+Lemma transf_all :
+  forall stk addr d_in d_out wr_en d c d' c',
+    transf_code stk addr d_in d_out wr_en d c = (d', c') ->
+    behaviour_correct d c d' c' (Some (mk_ram stk addr wr_en d_in d_out)).
+Proof.
+
+Lemma transf_code_correct:
+  forall stk addr d_in d_out wr_en d c d' c',
+    transf_code stk addr d_in d_out wr_en d c = (d', c') ->
+    (forall i d_s c_s,
+        d!i = Some d_s ->
+        c!i = Some c_s ->
+        tr_code stk addr d_in d_out wr_en d c d' c' i).
+Proof.
+  simplify.
+  unfold transf_code in H.
+  destruct_match. destruct_match. inv H.
+  econstructor; eauto.
+
 Definition match_prog (p: program) (tp: program) :=
   Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
 
@@ -194,50 +415,219 @@ Proof.
   apply Linking.match_transform_program.
 Qed.
 
-Section CORRECTNESS.
+Lemma exec_all_Vskip :
+  forall rs ar,
+    exec_all Vskip Vskip None rs ar rs ar.
+Proof.
+  unfold exec_all.
+  intros. repeat econstructor.
+  Unshelve. unfold fext. exact tt.
+Qed.
+
+Lemma match_assocmaps_trans:
+  forall rs1 rs2 rs3,
+    match_assocmaps rs1 rs2 ->
+    match_assocmaps rs2 rs3 ->
+    match_assocmaps rs1 rs3.
+Proof.
+  intros. inv H. inv H0. econstructor; eauto.
+Qed.
 
-  Context (prog: program).
+Lemma match_reg_assocs_trans:
+  forall rs1 rs2 rs3,
+    match_reg_assocs rs1 rs2 ->
+    match_reg_assocs rs2 rs3 ->
+    match_reg_assocs rs1 rs3.
+Proof.
+  intros. inv H. inv H0.
+  econstructor; eapply match_assocmaps_trans; eauto.
+Qed.
 
-  Let tprog := transf_program prog.
+Lemma transf_maps_correct:
+  forall st addr d_in d_out wr_en n d c n' d' c' i,
+    transf_maps st addr d_in d_out wr_en i (n, d, c) = (n', d', c') ->
+    behaviour_correct d c d' c' (Some (mk_ram st addr wr_en d_in d_out)).
+Proof.
+  Admitted.
 
-  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) ->
+
+
+Lemma transf_maps_correct2:
+  forall l st addr d_in d_out wr_en n d c n' d' c',
+    fold_right (transf_maps st addr d_in d_out wr_en) (n, d, c) l = (n', d', c') ->
+    behaviour_correct d c d' c' (Some (mk_ram st addr wr_en d_in d_out)).
+Proof.
+  induction l.
+  - intros. simpl in *. inv H. mgen_crush.
+  - intros. simpl in *.
+    destruct (fold_right (transf_maps st addr d_in d_out wr_en) (n, d, c) l) eqn:?.
+    destruct p.
+    eapply behaviour_correct_trans.
+    eapply transf_maps_correct.
+    apply H. eapply IHl. apply Heqp.
+Qed.
+
+Lemma transf_maps_preserves_behaviour :
+  forall ge m m' s addr d_in d_out wr_en n n' t stk rs ar d' c' wf' i,
+    m' = mkmodule (mod_params m)
+                  d'
+                  c'
+                  (mod_entrypoint m)
+                  (mod_st m)
+                  (mod_stk m)
+                  (2 ^ Nat.log2_up m.(mod_stk_len))%nat
+                  (mod_finish m)
+                  (mod_return m)
+                  (mod_start m)
+                  (mod_reset m)
+                  (mod_clk m)
+                  (AssocMap.set wr_en (None, VScalar 32)
+                   (AssocMap.set d_out (None, VScalar 32)
+                    (AssocMap.set d_in (None, VScalar 32)
+                     (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls)))))
+                  (AssocMap.set (mod_stk m) (None, VArray 32 (2 ^ Nat.log2_up m.(mod_stk_len)))%nat m.(mod_arrdecls))
+                  (Some (mk_ram (mod_stk m) addr wr_en d_in d_out))
+                  wf' ->
+    transf_maps m.(mod_st) addr d_in d_out wr_en i (n, mod_datapath m, mod_controllogic m) = (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.
+Proof.
+Admitted.
+
+Lemma fold_transf_maps_preserves_behaviour :
+  forall ge m m' s addr d_in d_out wr_en n' t stk rs ar d' c' wf' l rs' ar' trs tar,
+    fold_right (transf_maps m.(mod_st) addr d_in d_out wr_en)
+              (max_pc_function m + 1, m.(mod_datapath), m.(mod_controllogic)) l = (n', d', c') ->
+    m' = mkmodule (mod_params m)
+                  d'
+                  c'
+                  (mod_entrypoint m)
+                  (mod_st m)
+                  (mod_stk m)
+                  (2 ^ Nat.log2_up m.(mod_stk_len))%nat
+                  (mod_finish m)
+                  (mod_return m)
+                  (mod_start m)
+                  (mod_reset m)
+                  (mod_clk m)
+                  (AssocMap.set wr_en (None, VScalar 32)
+                   (AssocMap.set d_out (None, VScalar 32)
+                    (AssocMap.set d_in (None, VScalar 32)
+                     (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls)))))
+                  (AssocMap.set (mod_stk m) (None, VArray 32 (2 ^ Nat.log2_up m.(mod_stk_len)))%nat m.(mod_arrdecls))
+                  (Some (mk_ram (mod_stk m) addr wr_en d_in d_out))
+                  wf' ->
+    match_arrs ar tar ->
+    match_assocmaps rs trs ->
+    step ge (State stk m s rs ar) t (State stk m s rs' ar') ->
+    exists trs' tar', step ge (State stk m' s trs tar) t (State stk m' s trs' tar')
+                      /\ match_arrs ar' tar'
+                      /\ match_assocmaps rs' trs'.
+Proof.
+Admitted.
+
+Lemma fold_transf_maps_preserves_behaviour2 :
+  forall ge m m' s t stk rs ar rs' ar' trs tar s',
+    transf_module m = m' ->
+    match_arrs ar tar ->
+    match_assocmaps rs trs ->
+    step ge (State stk m s rs ar) t (State stk m s' rs' ar') ->
+    exists trs' tar', step ge (State stk m' s trs tar) t (State stk m' s' trs' tar')
+                      /\ match_arrs ar' tar'
+                      /\ match_assocmaps rs' trs'.
+Proof.
+  intros.
+  unfold transf_module in *. destruct_match. destruct_match. apply transf_maps_correct2 in Heqp. inv H2.
+  unfold behaviour_correct in *. eexists. eexists. econstructor. econstructor; simplify; eauto.
+
+Lemma add_stack_len_no_effect :
+  forall ge m m' stk s rs ar t wr_en d_out d_in addr,
+    m' = mkmodule (mod_params m)
+                  (mod_datapath m)
+                  (mod_controllogic m)
+                  (mod_entrypoint m)
+                  (mod_st m)
+                  (mod_stk m)
+                  (2 ^ Nat.log2_up m.(mod_stk_len))%nat
+                  (mod_finish m)
+                  (mod_return m)
+                  (mod_start m)
+                  (mod_reset m)
+                  (mod_clk m)
+                  (AssocMap.set wr_en (None, VScalar 32)
+                   (AssocMap.set d_out (None, VScalar 32)
+                    (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))
+                  (mod_ram m)
+                  (mod_wf m) ->
+    step ge (State stk m s rs ar) t (State stk m s rs ar) ->
+    step ge (State stk m' s rs ar) t (State stk m' s rs ar).
+  Admitted.
+
+Section CORRECTNESS.
+
+  Context (prog tprog: program).
+  Context (TRANSL: match_prog prog tprog).
+
+  Let ge : HTL.genv := Genv.globalenv prog.
+  Let tge : HTL.genv := Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Hint Resolve symbols_preserved : rtlgp.
+
+  Lemma function_ptr_translated:
+    forall (b: Values.block) (f: fundef),
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf,
+        Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = tf.
+  Proof using TRANSL.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transf_fundef f = tf.
+  Proof using TRANSL.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof (Genv.senv_transf TRANSL).
+  Hint Resolve senv_preserved : rtlgp.
 
   Theorem transf_step_correct:
     forall (S1 : state) t S2,
       step ge S1 t S2 ->
         forall R1,
           match_states S1 R1 ->
-            exists R2, Smallstep.plus step ge R1 t R2 /\ match_states S2 R2.
+            exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    pose proof fold_transf_maps_preserves_behaviour.
     induction 1.
-    - exploit fold_transf_maps_preserves_behaviour. intros. inv H13. inv ASSOC. inv ARRS.
+    - intros. inv H12. inv ASSOC. inv ARRS.
+      repeat destruct_match; try solve [crush].
+      simplify.
+      exploit fold_transf_maps_preserves_behaviour2.
+      eauto. eauto. econstructor. eauto. econstructor. eauto. econstructor; eauto.
+      intros.
+      inv H12. inv H13.
+      simplify.
       econstructor.
       econstructor.
       eapply Smallstep.plus_one.
-      econstructor; unfold transf_module; repeat destruct_match; try solve [crush].
-      + simplify.
-
+      eapply H13.
+      econstructor; eauto.
+    - intros. inv H1. inv ASSOC. inv ARRS.
+      repeat econstructor; eauto.
 
 End CORRECTNESS.
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index 3defe9c..26dba7a 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -42,23 +42,27 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
 
 Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
-Definition inst_ram clk stk addr d_in d_out wr_en :=
+Definition inst_ram clk ram :=
   Valways (Vnegedge clk)
-          (Vcond (Vvar wr_en)
-                 (Vnonblock (Vvari stk (Vvar addr)) (Vvar d_in))
-                 (Vnonblock (Vvar d_out) (Vvari stk (Vvar addr)))).
+          (Vcond (Vvar (ram_en ram))
+                 (Vcond (Vvar (ram_wr_en ram))
+                        (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram)))
+                                   (Vvar (ram_d_in ram)))
+                        (Vnonblock (Vvar (ram_d_out ram))
+                                   (Vvari (ram_mem ram) (Vvar (ram_addr ram)))))
+                 Vskip).
 
 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 (mk_ram ram addr wr_en d_in d_out) =>
+  | Some ram =>
     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))))
                                                   (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip)))
                 :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip))
-                :: inst_ram m.(HTL.mod_clk) m.(HTL.mod_stk) addr d_in d_out wr_en
+                :: inst_ram m.(HTL.mod_clk) ram
                 :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
                                                           ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
     Verilog.mkmodule m.(HTL.mod_start)