Finish most of Veriloggenproof

1 files changed, 16 insertions, 18 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index b550ff9..f0ec576 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -19,32 +19,30 @@
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST.
-From coqup Require Import Verilog HTL Coquplib AssocMap Value.
+From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt.
 
-Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr * Verilog.stmnt) :=
-  match st with
-  | (n, stmt) :: ls => (Vlit (posToValue 32 n), stmt) :: transl_list ls
-  | nil => nil
-  end.
+Definition transl_list_fun (a : node * Verilog.stmnt) :=
+  let (n, stmnt) := a in
+  (Vlit (posToValue n), stmnt).
 
-Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item :=
-  match scldecl with
-  | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
-  | nil => nil
-  end.
+Definition transl_list st := map transl_list_fun st.
 
-Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item :=
-  match arrdecl with
-  | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
-  | nil => nil
-  end.
+Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
+  match a with (r, (io, VScalar sz)) => Vdeclaration (Vdecl io r sz) end.
+
+Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
+
+Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
+  match a with (r, (io, VArray sz l)) => Vdeclaration (Vdeclarr io r sz l) end.
+
+Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
 Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
   let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
   let body :=
-      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1))
-                                               (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint)))
+      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1)))
+                                               (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
                                                (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
       :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
       :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))