Add wires and use them for output of instances

[WIP] Add wires to HTL
[WIP] Add wires to verilog
[WIP] Use wire for finished signal
[WIP] merge wire and scl
[WIP] Fix wrong reg in ICall translation

5 files changed, 55 insertions, 23 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index b6c4a25..be473fc 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -34,7 +34,7 @@ Record state: Type := mkstate {
   st_st : reg;
   st_freshreg: reg;
   st_freshstate: node;
-  st_scldecls: AssocMap.t (option io * scl_decl);
+  st_scldecls: AssocMap.t scl_decl;
   st_arrdecls: AssocMap.t (option io * arr_decl);
   st_insts: AssocMap.t instantiation;
   st_datapath: datapath;
@@ -45,7 +45,7 @@ Definition init_state (st : reg) : state :=
   mkstate st
           1%positive
           1%positive
-          (AssocMap.empty (option io * scl_decl))
+          (AssocMap.empty scl_decl)
           (AssocMap.empty (option io * arr_decl))
           (AssocMap.empty instantiation)
           (AssocMap.empty stmnt)
@@ -140,7 +140,7 @@ Lemma declare_reg_state_incr :
        s.(st_st)
        s.(st_freshreg)
        s.(st_freshstate)
-       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+       (AssocMap.set r (VScalar i sz) s.(st_scldecls))
        s.(st_arrdecls)
        s.(st_insts)
        s.(st_datapath)
@@ -152,7 +152,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
                 s.(st_st)
                 s.(st_freshreg)
                 s.(st_freshstate)
-                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
+                (AssocMap.set r (VScalar i sz) s.(st_scldecls))
                 s.(st_arrdecls)
                 s.(st_insts)
                 s.(st_datapath)
@@ -274,7 +274,7 @@ Lemma add_instance_state_incr :
 Proof.
 Admitted.
 
-Definition add_instance (mod_name: ident) (args: list reg) (rst: reg) (finished: reg) (dst: reg) : mon unit :=
+Definition add_instance (mod_name: ident) (args: list reg) (finished: reg) (dst: reg) : mon unit :=
   fun s =>
         let instname := assocmap_nextavailable s.(st_insts) in
         let inst := HTL.HTLinstantiation mod_name instname args dst finished in
@@ -507,7 +507,7 @@ Lemma create_reg_state_incr:
          s.(st_st)
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+         (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls))
          s.(st_arrdecls)
          s.(st_insts)
          (st_datapath s)
@@ -520,13 +520,39 @@ Definition create_reg (i : option io) (sz : nat) : mon reg :=
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+                   (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls))
                    (st_arrdecls s)
                    (st_insts s)
                    (st_datapath s)
                    (st_controllogic s))
               (create_reg_state_incr s sz i).
 
+Lemma create_wire_state_incr:
+  forall s sz,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls))
+         s.(st_arrdecls)
+         s.(st_insts)
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_wire (sz : nat) : mon reg :=
+  fun s => let r := s.(st_freshreg) in
+           OK r (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls))
+                   (st_arrdecls s)
+                   (st_insts s)
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_wire_state_incr s sz).
+
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
@@ -555,9 +581,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.")
     | Icall sig (inr fn) args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
-        do rst <- create_reg None 1;
-        do finished <- create_reg None 1;
-        add_instance fn args rst finished dst
+        do finished <- create_wire 1;
+        do res <- create_wire 32;
+        add_instance fn args finished res
       else error (Errors.msg "State is larger than 2^32.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -678,7 +704,7 @@ Definition max_state (f: function) : state :=
   mkstate st
           (Pos.succ st)
           (Pos.succ (max_pc_function f))
-          (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
+          (AssocMap.set st (VScalar None 32) (st_scldecls (init_state st)))
           (st_arrdecls (init_state st))
           (st_insts (init_state st))
           (st_datapath (init_state st))
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index f9c88bf..07034cc 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -30,8 +30,11 @@ Definition transl_list_fun (a : node * Verilog.stmnt) :=
 
 Definition transl_list st := map transl_list_fun st.
 
-Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
-  match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end.
+Definition scl_to_Vdecl_fun (a : reg * scl_decl) :=
+  match a with
+  | (r, (VScalar io sz)) => (Vdecl io r sz)
+  | (r, VWire sz) => (Vdeclwire r sz)
+  end.
 
 Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
 
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 4d0ba42..2432e7e 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -63,7 +63,7 @@ Record module: Type :=
     mod_reset : reg;
     mod_clk : reg;
     mod_insts : AssocMap.t instantiation;
-    mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
+    mod_scldecls : AssocMap.t Verilog.scl_decl;
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
     mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
   }.
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 6fe2292..a355a17 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -141,6 +141,7 @@ let print_io = function
 let decl i = function
   | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
   | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)]
+  | Vdeclwire (r, sz) -> concat [indent i; declare "wire" (r, sz)]
   | Vinstancedecl (m, name, args) -> concat [
       indent i; vmodule m; " ";
       instance name; "("; concat (intersperse ", " (List.map register args)); ")";
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 6f65fdc..27522b4 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -100,7 +100,15 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
-Inductive scl_decl : Type := VScalar (sz : nat).
+Inductive io : Type :=
+| Vinput : io
+| Voutput : io
+| Vinout : io.
+
+Inductive scl_decl : Type :=
+| VScalar (io: option Verilog.io) (sz : nat)
+| VWire (sz : nat).
+
 Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
 (** * Verilog AST
@@ -194,18 +202,12 @@ Inductive edge : Type :=
 
 (** ** Module Items
 
-Module items can either be declarations ([Vdecl]) or always blocks ([Valways]).
-The declarations are always register declarations as combinational logic can be
-done using combinational always block instead of continuous assignments. *)
-
-Inductive io : Type :=
-| Vinput : io
-| Voutput : io
-| Vinout : io.
+Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). *)
 
 Inductive declaration : Type :=
 | Vdecl : option io -> reg -> nat -> declaration
 | Vdeclarr : option io -> reg -> nat -> nat -> declaration
+| Vdeclwire : reg -> nat -> declaration
 | Vinstancedecl : ident -> ident -> list reg -> declaration.
 
 Inductive module_item : Type :=