Update compilation

5 files changed, 84 insertions, 17 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 7a88839..5b4ef0a 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -74,7 +74,7 @@ Proof.
   intros. destruct x; simpl. rewrite print_identity. auto. auto.
 Qed.
 
-Definition transf_backend (r : RTL.program) : res Verilog.verilog :=
+Definition transf_backend (r : RTL.program) : res  Verilog.module :=
   OK r
   @@@ Veriloggen.transf_program.
 
@@ -88,7 +88,7 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program :=
   @@@ RTLgen.transl_program
   @@ print (print_RTL 0).
 
-Definition transf_hls (p : Csyntax.program) : res Verilog.verilog :=
+Definition transf_hls (p : Csyntax.program) : res Verilog.module :=
   OK p
   @@@ transf_frontend
   @@@ transf_backend.
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 4403019..c7ebf8e 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -166,7 +166,7 @@ Set Extraction AccessOpaque.
 
 Cd "src/Extraction".
 Separate Extraction
-         Verilog.verilog Verilog.valueToZ coqup.Compiler.transf_hls
+         Verilog.module Verilog.valueToZ coqup.Compiler.transf_hls
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 04a35de..5199872 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -53,13 +53,13 @@ let unop = function
   | Vneg -> " ~ "
   | Vnot -> " ! "
 
-let register a = P.to_int a
+let register a = sprintf "reg_%d" (P.to_int a)
 
 let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l))
 
 let rec pprint_expr = function
   | Vlit l -> literal l
-  | Vvar s -> sprintf "reg_%d" (register s)
+  | Vvar s -> register s
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
   | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"]
   | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
@@ -69,12 +69,48 @@ let rec pprint_stmnt i =
   in function
   | Vskip -> concat [indent i; ";\n"]
   | Vseq s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"]
-  | Vcond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n";
-                                pprint_stmnt (i + 1) st; indent i; "else\n";
-                                pprint_stmnt (i + 1) sf]
-  | Vcase (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n";
-                            fold_map pprint_case es; indent i; "endcase\n"]
+  | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ")\n";
+                                  pprint_stmnt (i + 1) st; indent i; "else\n";
+                                  pprint_stmnt (i + 1) sf
+                                ]
+  | Vcase (e, es) -> concat [ indent i; "case ("; pprint_expr e; ")\n";
+                              fold_map pprint_case es; indent (i+1); "default:;\n";
+                              indent i; "endcase\n"
+                            ]
   | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"]
   | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"]
 
-let print_program pp v = pstr pp (fold_map (pprint_stmnt 0) v)
+let rec pprint_edge = function
+  | Vposedge r -> concat ["posedge "; register r]
+  | Vnegedge r -> concat ["negedge "; register r]
+  | Valledge -> "*"
+  | Voredge (e1, e2) -> concat [pprint_edge e1; " or "; pprint_edge e2]
+
+let pprint_edge_top i = function
+  | Vposedge r -> concat ["@(posedge "; register r; ")"]
+  | Vnegedge r -> concat ["@(negedge "; register r; ")"]
+  | Valledge -> "@*"
+  | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"]
+
+let pprint_module_item i = function
+  | Vdecl (r, n, e) ->
+    concat [indent i; "reg ["; sprintf "%d" (Nat.to_int n - 1); ":0] "; register r; " = "; pprint_expr e; ";\n"]
+  | Valways (e, s) ->
+    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
+
+let rec intersperse c = function
+  | [] -> []
+  | [x] -> [x]
+  | x :: xs -> x :: c :: intersperse c xs
+
+let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
+
+let pprint_module i n m =
+  let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
+  let outputs = [m.mod_finish; m.mod_return] in
+  concat [ indent i; "module "; n; "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
+           fold_map (make_io (i+1) "input") inputs; fold_map (make_io (i+1) "output") outputs;
+           fold_map (pprint_module_item (i+1)) m.mod_body; indent i; "endmodule\n"
+         ]
+
+let print_program pp v = pstr pp (pprint_module 0 "main" v)
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 4197d4a..181a9d2 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -16,4 +16,4 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-val print_program : out_channel -> Verilog.verilog -> unit
+val print_program : out_channel -> Verilog.coq_module -> unit
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index e91ca2d..212dbc0 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -39,9 +39,12 @@ Record value : Type := mkvalue {
 }.
 
 Definition posToValue (p : positive) : value :=
-  let size := Z.to_nat (log_sup p) in
+  let size := Z.to_nat (Z.succ (log_inf p)) in
   mkvalue size (Word.posToWord size p).
 
+Definition ZToValue (s : nat) (z : Z) : value :=
+  mkvalue s (Word.ZToWord s z).
+
 Definition intToValue (i : Integers.int) : value :=
   mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)).
 
@@ -94,13 +97,41 @@ Inductive stmnt : Type :=
 | Vcond : expr -> stmnt -> stmnt -> stmnt
 | Vcase : expr -> list (expr * stmnt) -> stmnt
 | Vblock : expr -> expr -> stmnt
-| Vnonblock : expr -> expr -> stmnt
-| Vdecl : reg -> nat -> expr -> stmnt.
+| Vnonblock : expr -> expr -> stmnt.
+
+(** [edge] is not part of [stmnt] in this formalisation because is closer to the
+    semantics that are used. *)
+Inductive edge : Type :=
+| Vposedge : reg -> edge
+| Vnegedge : reg -> edge
+| Valledge : edge
+| Voredge : edge -> edge -> edge.
+
+Inductive module_item : Type :=
+| Vdecl : reg -> nat -> expr -> module_item
+| Valways : edge -> stmnt -> module_item.
+
+(** [mod_start] If set, starts the computations in the module. *)
+(** [mod_reset] If set, reset the state in the module. *)
+(** [mod_clk] The clock that controls the computation in the module. *)
+(** [mod_args] The arguments to the module. *)
+(** [mod_finish] Bit that is set if the result is ready. *)
+(** [mod_return] The return value that was computed. *)
+(** [mod_body] The body of the module, including the state machine. *)
+Record module : Type := mkmodule {
+  mod_start : reg;
+  mod_reset : reg;
+  mod_clk : reg;
+  mod_finish : reg;
+  mod_return : reg;
+  mod_args : list reg;
+  mod_body : list module_item;
+}.
 
+(** Convert a [positive] to an expression directly, setting it to the right
+    size. *)
 Definition posToLit (p : positive) : expr :=
   Vlit (posToValue p).
 
-Definition verilog : Type := list stmnt.
-
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.