Fix declaring function arguments correctly

3 files changed, 69 insertions, 12 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 15100bf..bbce47c 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -125,28 +125,28 @@ Proof.
 Qed.
 
 Lemma declare_reg_state_incr :
-  forall s r sz,
+  forall i s r sz,
     st_incr s
     (mkstate
        s.(st_st)
        s.(st_freshreg)
        s.(st_freshstate)
-       (AssocMap.set r (None, Scalar sz) s.(st_scldecls))
+       (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
        s.(st_arrdecls)
        s.(st_datapath)
        s.(st_controllogic)).
 Proof. auto with htlh. Qed.
 
-Definition declare_reg (r : reg) (sz : nat) : mon unit :=
+Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
   fun s => OK tt (mkstate
                 s.(st_st)
                 s.(st_freshreg)
                 s.(st_freshstate)
-                (AssocMap.set r (None, Scalar sz) s.(st_scldecls))
+                (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
                 s.(st_arrdecls)
                 s.(st_datapath)
                 s.(st_controllogic))
-              (declare_reg_state_incr s r sz).
+              (declare_reg_state_incr i s r sz).
 
 Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
   fun s =>
@@ -359,7 +359,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Inop n' => add_instr n n' Vskip
     | Iop op args dst n' =>
       do instr <- translate_instr op args;
-      do _ <- declare_reg dst 32;
+      do _ <- declare_reg None dst 32;
       add_instr n n' (nonblock dst instr)
     | Iload mem addr args dst n' =>
       do src <- translate_arr_access mem addr args stack;
@@ -437,6 +437,7 @@ Definition transf_module (f: function) : mon module :=
   do rtrn <- create_reg (Some Voutput) 32;
   do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
   do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
+  do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
   do start <- create_reg (Some Vinput) 1;
   do rst <- create_reg (Some Vinput) 1;
   do clk <- create_reg (Some Vinput) 1;
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 8bb90c6..770b372 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -209,6 +209,20 @@ Lemma create_reg_controllogic_trans :
 Proof. intros. monadInv H. trivial. Qed.
 Hint Resolve create_reg_controllogic_trans : htlspec.
 
+Lemma declare_reg_datapath_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_datapath_trans : htlspec.
+
+Lemma declare_reg_controllogic_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_controllogic_trans : htlspec.
+
 Lemma create_arr_datapath_trans :
   forall sz ln s s' x i iop,
     create_arr iop sz ln s = OK x s' i ->
@@ -255,6 +269,44 @@ Ltac inv_incr :=
   | [ H: st_incr _ _ |- _ ] => destruct st_incr
   end.
 
+Lemma collect_controllogic_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_datapath_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_declare_controllogic_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_controllogic) = s'.(st_controllogic).
+Proof.
+  intros. eapply collect_controllogic_trans; try eassumption.
+  intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption.
+Qed.
+
+Lemma collect_declare_datapath_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_datapath) = s'.(st_datapath).
+Proof.
+  intros. eapply collect_datapath_trans; try eassumption.
+  intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption.
+Qed.
+
 Ltac rewrite_states :=
   match goal with
   | [ H: ?x ?s = ?x ?s' |- _ ] =>
@@ -395,9 +447,13 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (STC: st_controllogic s9 = st_controllogic s3) by congruence.
-  assert (STD: st_datapath s9 = st_datapath s3) by congruence.
-  assert (STST: st_st s9 = st_st s3) by congruence.
+  assert (EQ3D := EQ3).
+  destruct x3.
+  apply collect_declare_datapath_trans in EQ3.
+  apply collect_declare_controllogic_trans in EQ3D.
+  assert (STC: st_controllogic s10 = st_controllogic s3) by congruence.
+  assert (STD: st_datapath s10 = st_datapath s3) by congruence.
+  assert (STST: st_st s10 = st_st s3) by congruence.
   rewrite STC. rewrite STD. rewrite STST.
   eapply iter_expand_instr_spec; eauto with htlspec.
   apply PTree.elements_complete.
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index d81bf18..700b8e3 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -180,8 +180,7 @@ let pprint_module i n m =
   concat [ indent i; "module "; (extern_atom n);
            "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
            fold_map (pprint_module_item (i+1)) m.mod_body;
-           indent i; "endmodule\n\n";
-           testbench
+           indent i; "endmodule\n\n"
          ]
 
 let print_result pp lst =
@@ -201,4 +200,5 @@ let print_globdef pp (id, gd) =
   | _ -> ()
 
 let print_program pp prog =
-  List.iter (print_globdef pp) prog.prog_defs
+  List.iter (print_globdef pp) prog.prog_defs;
+  pstr pp testbench