From f26f3887d0b0ac286c317a5425a3a4781871cfc2 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 30 Jun 2020 12:34:35 +0100
Subject: Add command line flags for initial block

---
 driver/CoqupDriver.ml       |  8 +++-----
 src/CoqupClflags.ml         |  5 +++++
 src/verilog/PrintVerilog.ml | 10 ++++++++++
 test/loop.c                 |  6 ++++--
 4 files changed, 22 insertions(+), 7 deletions(-)
 create mode 100644 src/CoqupClflags.ml

diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 2932a50..afbe4d0 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -36,11 +36,7 @@ open Coqup.Frontend
 open Coqup.Assembler
 open Coqup.Linker
 open Coqup.Diagnostics
-
-(* Coqup flags *)
-let option_simulate = ref false
-let option_hls = ref true
-let option_debug_hls = ref false
+open Coqup.CoqupClflags
 
 (* Name used for version string etc. *)
 let tool_name = "C verified high-level synthesis"
@@ -215,6 +211,7 @@ Processing options:
   --no-hls       Do not use HLS and generate standard flow.
   --simulate     Simulate the result with the Verilog semantics.
   --debug-hls    Add debug logic to the Verilog.
+  --initialise-stack initialise the stack to all 0s.
 |} ^
   prepro_help ^
   language_support_help ^
@@ -316,6 +313,7 @@ let cmdline_actions =
   [Exact "--no-hls", Unset option_hls;
    Exact "--simulate", Set option_simulate;
    Exact "--debug-hls", Set option_debug_hls;
+   Exact "--initialise-stack", Set option_initial;
   ]
 (* Getting version info *)
   @ version_options tool_name @
diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml
new file mode 100644
index 0000000..83dd31d
--- /dev/null
+++ b/src/CoqupClflags.ml
@@ -0,0 +1,5 @@
+(* Coqup flags *)
+let option_simulate = ref false
+let option_hls = ref true
+let option_debug_hls = ref false
+let option_initial = ref false
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5dc0386..6d10887 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -22,9 +22,12 @@ open Datatypes
 
 open Camlcoq
 open AST
+open Clflags
 
 open Printf
 
+open CoqupClflags
+
 let concat = String.concat ""
 
 let indent i = String.make (2 * i) ' '
@@ -187,6 +190,12 @@ let debug_always i clk state = concat [
     indent i; "end\n"
   ]
 
+let print_initial i n stk = concat [
+    indent i; "integer i;\n";
+    indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n";
+    indent (i+1); register stk; "[i] = 0;\n"
+  ]
+
 let pprint_module debug i n m =
   if (extern_atom n) = "main" then
     let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
@@ -194,6 +203,7 @@ let pprint_module debug 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;
+             if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
              if debug then debug_always i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
            ]
diff --git a/test/loop.c b/test/loop.c
index b459e3a..52e4fe9 100644
--- a/test/loop.c
+++ b/test/loop.c
@@ -1,10 +1,12 @@
 int main() {
     int max = 5;
     int acc = 0;
+    int b = 1;
+    int c = 2;
     
-    for (int i = 0; i < max; i++) {
+    for (int i = 0; i < max; i = i + b) {
         acc += i;
     }
 
-    return acc + 2;
+    return acc + c;
 }
-- 
cgit