diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-03 17:13:56 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-03 17:13:56 +0100 |
commit | 0b118f8dca9068e0075e72f4d0c24cf707df44c7 (patch) | |
tree | 4697b2ce306c4271b92a46589685603d62a0848a /debug/CoqupTest.ml | |
parent | d2c3d5a4fdb35b861be9df0795ef83f9b83c7bb7 (diff) | |
download | vericert-0b118f8dca9068e0075e72f4d0c24cf707df44c7.tar.gz vericert-0b118f8dca9068e0075e72f4d0c24cf707df44c7.zip |
Add code to debug execution of HLS
Diffstat (limited to 'debug/CoqupTest.ml')
-rw-r--r-- | debug/CoqupTest.ml | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/debug/CoqupTest.ml b/debug/CoqupTest.ml new file mode 100644 index 0000000..f961f64 --- /dev/null +++ b/debug/CoqupTest.ml @@ -0,0 +1,59 @@ +open Coqup + +open Test +open Camlcoq +open FMapPositive + +let test_function_transf () = + print_endline "Testing transformation"; + print_endline "TL PROGRAM: "; + PrintRTL.print_program stdout testinputprogram; + print_endline "VERILOG PROGRAM: "; + + let v = match Veriloggen.transf_program testinputprogram with + | Errors.OK v -> v + | Errors.Error _ -> + raise (Failure "Error") in + PrintVerilog.print_program stdout v + +let cvalue n = Value.natToValue (Nat.of_int 32) (Nat.of_int n) + +let test_values () = + print_endline "Testing values"; + let v1 = cvalue 138 in + let v2 = cvalue 12 in + let v3 = Value.natToValue (Nat.of_int 16) (Nat.of_int 21) in + PrintVerilog.print_value stdout v1; + print_newline(); + PrintVerilog.print_value stdout v2; + print_newline(); + PrintVerilog.print_value stdout v3; + print_newline(); + print_string "Addition: "; + PrintVerilog.print_value stdout (Value.vplus v1 v2); + print_newline(); + print_string "Wrong addition: "; + PrintVerilog.print_value stdout (Value.vplus v1 v3); + print_newline(); + print_string "Opt addition: "; + match Value.vplus_opt v1 v2 with + | Some x -> begin + PrintVerilog.print_value stdout x; + print_endline ""; + match Value.vplus_opt v1 v3 with + | Some x -> PrintVerilog.print_value stdout x; print_newline() + | None -> print_endline "Correctly failed in addition" + end + | None -> raise (Failure "Error") + +let simulate_test () = + print_endline "Simulation test"; + let v = + match Veriloggen.transf_program testinputprogram with + | Errors.OK v -> v + | _ -> raise (Failure "HLS Error") in + match Verilog.module_run (Nat.of_int 10) v with + | Errors.OK lst -> PrintVerilog.print_result stdout (PositiveMap.elements lst) + | _ -> raise (Failure "Simulation error") + +let () = test_function_transf () |