WIP

6 files changed, 160 insertions, 140 deletions

diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
index b024b9e..edd413c 100644
--- a/src/hls/ApplyExternctrl.v
+++ b/src/hls/ApplyExternctrl.v
@@ -89,14 +89,14 @@ Section APPLY_EXTERNCTRL.
     end.
 
   Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) :=
-    fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) :=
+    fix cases_apply_externctrl (cs : stmnt_expr_list) :=
       match cs with
-      | nil => OK nil
-      | (c_e, c_s) :: tl =>
+      | Stmntnil  => OK Stmntnil
+      | Stmntcons c_e c_s tl =>
         do c_e' <- expr_apply_externctrl c_e;
         do c_s' <- stmnt_apply_externctrl_ c_s;
         do tl' <- cases_apply_externctrl tl;
-        OK ((c_e', c_s') :: tl')
+        OK (Stmntcons c_e' c_s' tl')
       end.
 
   Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt :=
@@ -142,6 +142,12 @@ Section APPLY_EXTERNCTRL.
     do l <- xassocmap_apply_externctrl (AssocMap.elements regmap);
     OK (AssocMap_Properties.of_list l).
 
+
+  Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) :
+    option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive).
+  destruct mr.
+  - intros.
+
   Definition module_apply_externctrl : res HTL.module :=
     do mod_start' <- reg_apply_externctrl (HTL.mod_start m);
     do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m);
@@ -159,26 +165,33 @@ Section APPLY_EXTERNCTRL.
     do mod_externctrl' <- assocmap_apply_externctrl (HTL.mod_externctrl m);
 
     match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned,
-          zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with
-    | left LEDATA, left LECTRL =>
+          zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned,
+          decide_order mod_st' mod_finish' mod_return' mod_stk' mod_start' mod_reset' mod_clk',
+          max_list_dec mod_params' mod_st',
+          decide_ram_wf mod_clk' (HTL.mod_ram m) with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
       OK (HTL.mkmodule
-             mod_params'
-             mod_datapath'
-             mod_controllogic'
-             (HTL.mod_entrypoint m)
-             mod_st'
-             mod_stk'
-             (HTL.mod_stk_len m)
-             mod_finish'
-             mod_return'
-             mod_start'
-             mod_reset'
-             mod_clk'
-             mod_scldecls'
-             mod_arrdecls'
-             mod_externctrl'
-             (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
-    | _, _ => Error (Errors.msg "More than 2^32 states.")
+          mod_params'
+          mod_datapath'
+          mod_controllogic'
+          (HTL.mod_entrypoint m)
+          mod_st'
+          mod_stk'
+          (HTL.mod_stk_len m)
+          mod_finish'
+          mod_return'
+          mod_start'
+          mod_reset'
+          mod_clk'
+          mod_scldecls'
+          mod_arrdecls'
+          mod_externctrl'
+          (HTL.mod_ram m)
+          (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))
+          MORD
+          (HTL.mod_ram_wf m)
+          WFPARAMS)
+    | _, _, _, _ => Error (Errors.msg "ApplyExternctrl")
     end.
 End APPLY_EXTERNCTRL.
 
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 886f86d..c22497f 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -110,7 +110,6 @@ Record module: Type :=
     (** Map from registers in this module to control registers in other modules.
         These will be mapped to the same verilog register. *)
     mod_externctrl : AssocMap.t (ident * controlsignal);
-    mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
     mod_ram : option ram;
     mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath;
     mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk;
@@ -141,7 +140,7 @@ Definition prog_modmap (p : HTL.program) :=
                                (AST.prog_defs p)).
 
 Lemma max_pc_wf :
-  forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+  forall T m, (Z.pos (max_pc_map m) <= Integers.Int.max_unsigned)%Z ->
             @map_well_formed T m.
 Proof.
   unfold map_well_formed. intros.
@@ -257,7 +256,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       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 ->
+      (Z.pos pstval <= Integers.Int.max_unsigned)%Z ->
       step g
            (State sf mid m st     asr  asa) Events.E0
            (State sf mid m pstval asr' asa')
@@ -437,3 +436,14 @@ Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True
     ); auto.
   apply max_list_correct. apply Pos.ltb_lt in e. lia.
 Qed.
+
+Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
+  refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
+                          && (d <? e) && (e <? f) && (f <? g))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold module_ordering; auto.
+Defined.
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 0b7f3ec..84e1a0f 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -626,17 +626,6 @@ Proof.
   simplify. transitivity (Z.pos (max_pc_map m)); eauto.
 Qed.
 
-Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
-  refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
-                          && (d <? e) && (e <? f) && (f <? g))%positive true with
-          | left t => left _
-          | _ => _
-          end); auto.
-  simplify; repeat match goal with
-                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
-                   end; unfold module_ordering; auto.
-Defined.
-
 Definition transf_module (f: function) : mon HTL.module.
   refine (
   if stack_correct f.(fn_stacksize) then
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v
index b9fbcaa..6c816c2 100644
--- a/src/hls/Renaming.v
+++ b/src/hls/Renaming.v
@@ -102,12 +102,12 @@ Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) :=
     ret (Vcond e' s1' s2')
   | Vcase e cs def =>
     do e' <- renumber_expr e;
-    do cs' <- sequence (map
-                      (fun (c : (Verilog.expr * Verilog.stmnt)) =>
-                    let (c_expr, c_stmnt) := c in
+    do cs_list' <- sequence (map
+                      (fun '(c_expr, c_stmnt) =>
                     do expr' <- renumber_expr c_expr;
                     do stmnt' <- renumber_stmnt c_stmnt;
-                    ret (expr', stmnt')) cs);
+                    ret (expr', stmnt')) (stmnt_to_list cs));
+    let cs' := list_to_stmnt cs_list' in
     do def' <- match def with
               | None => ret None
               | Some d => do def' <- renumber_stmnt d; ret (Some def')
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index 1ded68a..1e7bb8e 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -62,8 +62,16 @@ Section TRANSLATE.
     | _ => Some it
     end.
 
-  Definition mod_body (m : HTL.module) :=
-
+  Definition inst_ram clk ram :=
+    Valways (Vnegedge clk)
+            (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram)))
+                   (Vseq (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)))))
+                         (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram))))
+                   Vskip).
 
   (* FIXME Remove the fuel parameter (recursion limit)*)
   Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module :=
@@ -85,8 +93,8 @@ Section TRANSLATE.
                                         translated_modules in
 
 
-      let case_el_ctrl := transl_states (PTree.elements (HTL.mod_controllogic m)) in
-      let case_el_data := transl_states (PTree.elements (HTL.mod_datapath m)) in
+      let case_el_ctrl := list_to_stmnt (transl_states (PTree.elements (HTL.mod_controllogic m))) in
+      let case_el_data := list_to_stmnt (transl_states (PTree.elements (HTL.mod_datapath m))) in
 
       let externctrl := HTL.mod_externctrl m in
 
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index c54f726..8ecab63 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -264,114 +264,114 @@ Admitted.
 (* Qed. *)
 (* Hint Resolve mis_stepp_decl : verilogproof. *)
 
-Lemma mis_stepp_negedge_decl :
-  forall l asr asa f,
-    mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa.
-Proof.
-  induction l.
-  - intros. constructor.
-  - intros. simplify. econstructor. constructor. auto.
-Qed.
-Hint Resolve mis_stepp_negedge_decl : verilogproof.
+(* Lemma mis_stepp_negedge_decl : *)
+(*   forall l asr asa f, *)
+(*     mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa. *)
+(* Proof. *)
+(*   induction l. *)
+(*   - intros. constructor. *)
+(*   - intros. simplify. econstructor. constructor. auto. *)
+(* Qed. *)
+(* Hint Resolve mis_stepp_negedge_decl : verilogproof. *)
 
-Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_stk_len_equiv m : mod_stk_len (transl_module m) = HTL.mod_stk_len m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_stk_len_equiv m : mod_stk_len (transl_module m) = HTL.mod_stk_len m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_finish_equiv m : mod_finish (transl_module m) = HTL.mod_finish m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_finish_equiv m : mod_finish (transl_module m) = HTL.mod_finish m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_reset_equiv m : mod_reset (transl_module m) = HTL.mod_reset m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_reset_equiv m : mod_reset (transl_module m) = HTL.mod_reset m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_clk_equiv m : mod_clk (transl_module m) = HTL.mod_clk m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_clk_equiv m : mod_clk (transl_module m) = HTL.mod_clk m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_return_equiv m : mod_return (transl_module m) = HTL.mod_return m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_return_equiv m : mod_return (transl_module m) = HTL.mod_return m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma mod_params_equiv m : mod_args (transl_module m) = HTL.mod_params m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma mod_params_equiv m : mod_args (transl_module m) = HTL.mod_params m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Lemma empty_stack_equiv m : empty_stack (transl_module m) = HTL.empty_stack m.
-Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+(* Lemma empty_stack_equiv m : empty_stack (transl_module m) = HTL.empty_stack m. *)
+(* Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. *)
 
-Ltac rewrite_eq := rewrite mod_return_equiv
-                   || rewrite mod_clk_equiv
-                   || rewrite mod_reset_equiv
-                   || rewrite mod_finish_equiv
-                   || rewrite mod_stk_len_equiv
-                   || rewrite mod_stk_equiv
-                   || rewrite mod_st_equiv
-                   || rewrite mod_entrypoint_equiv
-                   || rewrite mod_params_equiv
-                   || rewrite empty_stack_equiv.
+(* Ltac rewrite_eq := rewrite mod_return_equiv *)
+(*                    || rewrite mod_clk_equiv *)
+(*                    || rewrite mod_reset_equiv *)
+(*                    || rewrite mod_finish_equiv *)
+(*                    || rewrite mod_stk_len_equiv *)
+(*                    || rewrite mod_stk_equiv *)
+(*                    || rewrite mod_st_equiv *)
+(*                    || rewrite mod_entrypoint_equiv *)
+(*                    || rewrite mod_params_equiv *)
+(*                    || rewrite empty_stack_equiv. *)
 
-Lemma find_assocmap_get r i v : r ! i = Some v -> r # i = v.
-Proof.
-  intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. auto.
-Qed.
+(* Lemma find_assocmap_get r i v : r ! i = Some v -> r # i = v. *)
+(* Proof. *)
+(*   intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. auto. *)
+(* Qed. *)
 
-Lemma ram_exec_match :
-  forall f asr asa asr' asa' r clk,
-    HTL.exec_ram asr asa (Some r) asr' asa' ->
-    mi_stepp_negedge f asr asa (inst_ram clk r) asr' asa'.
-Proof.
-  inversion 1; subst; simplify.
-  { unfold inst_ram. econstructor.
-    eapply stmnt_runp_Vcond_false.
-    econstructor. econstructor. econstructor. auto.
-    econstructor. auto.
-    simplify.
-    unfold boolToValue, natToValue, valueToBool.
-    rewrite Int.eq_sym. rewrite H3. simplify.
-    auto. constructor. }
-  { unfold inst_ram. econstructor. econstructor. econstructor.
-    econstructor. econstructor. auto.
-    econstructor. auto.
-    simplify.
-    unfold boolToValue, natToValue, valueToBool.
-    pose proof H4 as X. apply find_assocmap_get in X.
-    rewrite X. rewrite Int.eq_sym. rewrite H1. auto.
-    econstructor. econstructor. econstructor. econstructor.
-    pose proof H5 as X. apply find_assocmap_get in X.
-    rewrite X.
-    unfold valueToBool. unfold ZToValue in *.
-    unfold Int.eq in H2.
-    unfold uvalueToZ.
-    assert (Int.unsigned wr_en =? 0 = false).
-    apply Z.eqb_neq. rewrite Int.unsigned_repr in H2 by (simplify; lia).
-    destruct (zeq (Int.unsigned wr_en) 0); crush.
-    rewrite H0. auto.
-    apply stmnt_runp_Vnonblock_arr. econstructor. econstructor. auto.
-    econstructor. econstructor.
-    apply find_assocmap_get in H9. rewrite H9.
-    apply find_assocmap_get in H6. rewrite H6.
-    repeat econstructor. apply find_assocmap_get; auto.
-  }
-  { econstructor. econstructor. econstructor. econstructor. auto.
-    econstructor. auto.
-    econstructor.
-    unfold boolToValue, natToValue, valueToBool.
-    apply find_assocmap_get in H3. rewrite H3.
-    rewrite Int.eq_sym. rewrite H1. auto.
-    econstructor.
-    eapply stmnt_runp_Vcond_false. econstructor. auto.
-    simplify. apply find_assocmap_get in H4. rewrite H4.
-    auto.
-    repeat (econstructor; auto). apply find_assocmap_get in H5.
-    rewrite H5. eassumption.
-    repeat econstructor. simplify. apply find_assocmap_get; auto.
-  }
-Qed.
+(* Lemma ram_exec_match : *)
+(*   forall f asr asa asr' asa' r clk, *)
+(*     HTL.exec_ram asr asa (Some r) asr' asa' -> *)
+(*     mi_stepp_negedge f asr asa (inst_ram clk r) asr' asa'. *)
+(* Proof. *)
+(*   inversion 1; subst; simplify. *)
+(*   { unfold inst_ram. econstructor. *)
+(*     eapply stmnt_runp_Vcond_false. *)
+(*     econstructor. econstructor. econstructor. auto. *)
+(*     econstructor. auto. *)
+(*     simplify. *)
+(*     unfold boolToValue, natToValue, valueToBool. *)
+(*     rewrite Int.eq_sym. rewrite H3. simplify. *)
+(*     auto. constructor. } *)
+(*   { unfold inst_ram. econstructor. econstructor. econstructor. *)
+(*     econstructor. econstructor. auto. *)
+(*     econstructor. auto. *)
+(*     simplify. *)
+(*     unfold boolToValue, natToValue, valueToBool. *)
+(*     pose proof H4 as X. apply find_assocmap_get in X. *)
+(*     rewrite X. rewrite Int.eq_sym. rewrite H1. auto. *)
+(*     econstructor. econstructor. econstructor. econstructor. *)
+(*     pose proof H5 as X. apply find_assocmap_get in X. *)
+(*     rewrite X. *)
+(*     unfold valueToBool. unfold ZToValue in *. *)
+(*     unfold Int.eq in H2. *)
+(*     unfold uvalueToZ. *)
+(*     assert (Int.unsigned wr_en =? 0 = false). *)
+(*     apply Z.eqb_neq. rewrite Int.unsigned_repr in H2 by (simplify; lia). *)
+(*     destruct (zeq (Int.unsigned wr_en) 0); crush. *)
+(*     rewrite H0. auto. *)
+(*     apply stmnt_runp_Vnonblock_arr. econstructor. econstructor. auto. *)
+(*     econstructor. econstructor. *)
+(*     apply find_assocmap_get in H9. rewrite H9. *)
+(*     apply find_assocmap_get in H6. rewrite H6. *)
+(*     repeat econstructor. apply find_assocmap_get; auto. *)
+(*   } *)
+(*   { econstructor. econstructor. econstructor. econstructor. auto. *)
+(*     econstructor. auto. *)
+(*     econstructor. *)
+(*     unfold boolToValue, natToValue, valueToBool. *)
+(*     apply find_assocmap_get in H3. rewrite H3. *)
+(*     rewrite Int.eq_sym. rewrite H1. auto. *)
+(*     econstructor. *)
+(*     eapply stmnt_runp_Vcond_false. econstructor. auto. *)
+(*     simplify. apply find_assocmap_get in H4. rewrite H4. *)
+(*     auto. *)
+(*     repeat (econstructor; auto). apply find_assocmap_get in H5. *)
+(*     rewrite H5. eassumption. *)
+(*     repeat econstructor. simplify. apply find_assocmap_get; auto. *)
+(*   } *)
+(* Qed. *)
 
 
 Section CORRECTNESS.