aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-06-22 10:08:14 +0100
committerYann Herklotz <git@yannherklotz.com>2020-06-22 10:08:14 +0100
commitc5170915a81ca1bca420cd4683855cc7ba8ff8c4 (patch)
tree8c4dc8009cb5ac09b4be976f5c2ec9cd87ad7ec8 /src
parent11ff840afe29c5340582e513613dc70c13879997 (diff)
parent9089af0dbd8dc079c16501c73727df82c34c530d (diff)
downloadvericert-c5170915a81ca1bca420cd4683855cc7ba8ff8c4.tar.gz
vericert-c5170915a81ca1bca420cd4683855cc7ba8ff8c4.zip
Merge branch 'master' into develop
Diffstat (limited to 'src')
-rw-r--r--src/translation/HTLgen.v10
-rw-r--r--src/verilog/PrintVerilog.ml39
-rw-r--r--src/verilog/PrintVerilog.mli2
3 files changed, 33 insertions, 18 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index b26b9e3..68f9900 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -260,7 +260,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex
| _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other")
end.
-(** Translate an instruction to a statement. *)
+(** Translate an instruction to a statement. FIX mulhs mulhu *)
Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
match op, args with
| Op.Omove, r::nil => ret (Vvar r)
@@ -269,8 +269,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
| Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
| Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
| Op.Omulimm n, r::nil => ret (boplit Vmul r n)
- | Op.Omulhs, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhs")
- | Op.Omulhu, _ => error (Errors.msg "Htlgen: Instruction not implemented: Omulhu")
+ | Op.Omulhs, r1::r2::nil => ret (bop Vmul r1 r2)
+ | Op.Omulhu, r1::r2::nil => ret (bop Vmul r1 r2)
| Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
| Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
| Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
@@ -291,8 +291,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
(Vlit (intToValue n))))
| Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
| Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
- | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
- | Op.Oshldimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshldimm")
+ | Op.Ororimm n, r::nil => ret (Vbinop Vor (boplit Vshr r n) (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) n)))
+ | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
| Op.Ocmp c, _ => translate_condition c args
| Op.Osel c AST.Tint, r1::r2::rl =>
do tc <- translate_condition c rl;
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index a0f3ab3..5dc0386 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -175,14 +175,29 @@ let testbench = "module testbench;
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 "; (extern_atom n);
- "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
- fold_map (pprint_module_item (i+1)) m.mod_body;
- indent i; "endmodule\n\n"
- ]
+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 =
+ if (extern_atom n) = "main" then
+ 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"
+ ]
+ else ""
let print_result pp lst =
let rec print_result_in pp = function
@@ -195,11 +210,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