aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--driver/CoqupDriver.ml5
-rw-r--r--src/verilog/PrintVerilog.ml23
-rw-r--r--src/verilog/PrintVerilog.mli2
3 files changed, 23 insertions, 7 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 3dd0ed1..2932a50 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -40,6 +40,7 @@ open Coqup.Diagnostics
(* Coqup flags *)
let option_simulate = ref false
let option_hls = ref true
+let option_debug_hls = ref false
(* Name used for version string etc. *)
let tool_name = "C verified high-level synthesis"
@@ -100,7 +101,7 @@ let compile_c_file sourcename ifile ofile =
let loc = file_loc sourcename in
fatal_error loc "%a" print_error msg in
let oc = open_out ofile in
- Coqup.PrintVerilog.print_program oc verilog;
+ Coqup.PrintVerilog.print_program !option_debug_hls oc verilog;
close_out oc
end
@@ -213,6 +214,7 @@ Processing options:
-o <file> Generate output in <file>
--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.
|} ^
prepro_help ^
language_support_help ^
@@ -313,6 +315,7 @@ let cmdline_actions =
(* Use HLS *)
[Exact "--no-hls", Unset option_hls;
Exact "--simulate", Set option_simulate;
+ Exact "--debug-hls", Set option_debug_hls;
]
(* Getting version info *)
@ version_options tool_name @
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a0f3ab3..2d8af02 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -175,12 +175,25 @@ let testbench = "module testbench;
endmodule
"
-let pprint_module i n m =
+let debug_always i clk state = concat [
+ indent i; "reg [31:0] count;\n";
+ indent i; "initial count = 0;\n";
+ indent i; "always @(posedge " ^ register clk ^ ") begin\n";
+ indent (i+1); "if(count[0:0] == 10'd0) begin\n";
+ indent (i+2); "$display(\"Cycle count %d\", count);\n";
+ indent (i+2); "$display(\"State %d\\n\", " ^ register state ^ ");\n";
+ indent (i+1); "end\n";
+ indent (i+1); "count <= count + 1;\n";
+ indent i; "end\n"
+ ]
+
+let pprint_module debug 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 "; (extern_atom n);
"("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
fold_map (pprint_module_item (i+1)) m.mod_body;
+ if debug then debug_always i m.mod_clk m.mod_st else "";
indent i; "endmodule\n\n"
]
@@ -195,11 +208,11 @@ let print_result pp lst =
let print_value pp v = fprintf pp "%s" (literal v)
-let print_globdef pp (id, gd) =
+let print_globdef debug pp (id, gd) =
match gd with
- | Gfun(Internal f) -> pstr pp (pprint_module 0 id f)
+ | Gfun(Internal f) -> pstr pp (pprint_module debug 0 id f)
| _ -> ()
-let print_program pp prog =
- List.iter (print_globdef pp) prog.prog_defs;
+let print_program debug pp prog =
+ List.iter (print_globdef debug pp) prog.prog_defs;
pstr pp testbench
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 0df9d06..6544e52 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,6 +18,6 @@
val print_value : out_channel -> Value.value -> unit
-val print_program : out_channel -> Verilog.program -> unit
+val print_program : bool -> out_channel -> Verilog.program -> unit
val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit