diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 12:34:35 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 12:34:35 +0100 |
| commit | f26f3887d0b0ac286c317a5425a3a4781871cfc2 (patch) | |
| tree | ef89abc630bcc6087b38aba18fd859311e2d3ed1 /src | |
| parent | ae3f6b6096ab2484c1b3dcfab7f3f72bcfd268d5 (diff) | |
| download | vericert-kvx-f26f3887d0b0ac286c317a5425a3a4781871cfc2.tar.gz vericert-kvx-f26f3887d0b0ac286c317a5425a3a4781871cfc2.zip | |
Add command line flags for initial block
Diffstat (limited to 'src')
| -rw-r--r-- | src/CoqupClflags.ml | 5 | ||||
| -rw-r--r-- | src/verilog/PrintVerilog.ml | 10 |
2 files changed, 15 insertions, 0 deletions
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" ] |