From 8659e1b672a9b28a78c5b026312e7f3c0cb87c36 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 2 Apr 2020 14:54:14 +0100
Subject: Handle loops and conditionals correctly

---
 src/verilog/PrintVerilog.ml | 50 ++++++++++++++++++++++++++++++++++++++++-----
 src/verilog/Verilog.v       | 15 +++++++-------
 2 files changed, 53 insertions(+), 12 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5199872..292fcf2 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -92,9 +92,13 @@ let pprint_edge_top i = function
   | Valledge -> "@*"
   | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"]
 
+let declare i t =
+  function (r, sz) ->
+    concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
+             register r; ";\n" ]
+
 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"]
+  | Vdecl (r, sz) -> declare i "reg" (r, sz)
   | Valways (e, s) ->
     concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
 
@@ -105,12 +109,48 @@ let rec intersperse c = function
 
 let make_io i io r = concat [indent i; io; " "; register r; ";\n"]
 
+let compose f g x = g x |> f
+
+let init_inputs i r = declare i "input" r
+
+let init_outputs i r = declare i "output reg" r
+
+let testbench = "module testbench;
+   reg start, reset, clk;
+   wire finish;
+   wire [31:0] return_val;
+
+   main m(start, reset, clk, finish, return_val);
+
+   initial begin
+      clk = 0;
+      start = 0;
+      reset = 0;
+      @(posedge clk) reset = 1;
+      @(posedge clk) reset = 0;
+   end
+
+   always #5 clk = ~clk;
+
+   always @(posedge clk) begin
+      if (finish == 1) begin
+         $display(\"finished: %d\", return_val);
+         $finish;
+      end
+   end
+endmodule
+"
+
 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"
+  concat [ indent i; "module "; n;
+           "("; concat (intersperse ", " (List.map (compose register fst) (inputs @ outputs))); ");\n";
+           fold_map (init_inputs (i+1)) inputs;
+           fold_map (init_outputs (i+1)) outputs;
+           fold_map (pprint_module_item (i+1)) m.mod_body;
+           indent i; "endmodule\n\n";
+           testbench
          ]
 
 let print_program pp v = pstr pp (pprint_module 0 "main" v)
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 212dbc0..b9200b7 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -32,6 +32,7 @@ From compcert Require Integers.
 Import ListNotations.
 
 Definition reg : Type := positive.
+Definition szreg : Type := reg * nat.
 
 Record value : Type := mkvalue {
   vsize : nat;
@@ -108,7 +109,7 @@ Inductive edge : Type :=
 | Voredge : edge -> edge -> edge.
 
 Inductive module_item : Type :=
-| Vdecl : reg -> nat -> expr -> module_item
+| Vdecl : reg -> nat -> module_item
 | Valways : edge -> stmnt -> module_item.
 
 (** [mod_start] If set, starts the computations in the module. *)
@@ -119,12 +120,12 @@ Inductive module_item : Type :=
 (** [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_start : szreg;
+  mod_reset : szreg;
+  mod_clk : szreg;
+  mod_finish : szreg;
+  mod_return : szreg;
+  mod_args : list szreg;
   mod_body : list module_item;
 }.
 
-- 
cgit