diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-12-09 20:03:41 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-12-09 20:03:41 +0000 |
| commit | a64ccb64e16175b520a0dc4badde44a1cc46f17d (patch) | |
| tree | 41ff3b4511e40a809f1fefb4e0c02da643de92ad | |
| parent | 1c91db6b6d4cd20994fdfc40283b003c1ec93d50 (diff) | |
| download | vericert-a64ccb64e16175b520a0dc4badde44a1cc46f17d.tar.gz vericert-a64ccb64e16175b520a0dc4badde44a1cc46f17d.zip | |
Remove debug directory
| -rw-r--r-- | debug/CoqupTest.ml | 59 | ||||
| -rw-r--r-- | debug/dune | 5 |
2 files changed, 0 insertions, 64 deletions
diff --git a/debug/CoqupTest.ml b/debug/CoqupTest.ml deleted file mode 100644 index 2fe1389..0000000 --- a/debug/CoqupTest.ml +++ /dev/null @@ -1,59 +0,0 @@ -open Vericert - -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 () diff --git a/debug/dune b/debug/dune deleted file mode 100644 index feee97c..0000000 --- a/debug/dune +++ /dev/null @@ -1,5 +0,0 @@ -(include_subdirs no) - -(executable - (name VericertTest) - (libraries vericert)) |