Add code to debug execution of HLSsave/old-step

3 files changed, 137 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 ()
diff --git a/debug/dune b/debug/dune
new file mode 100644
index 0000000..7f0c6a6
--- /dev/null
+++ b/debug/dune
@@ -0,0 +1,5 @@
+(include_subdirs no)
+
+(executable
+ (name CoqupTest)
+ (libraries coqup))
diff --git a/src/verilog/Test.v b/src/verilog/Test.v
new file mode 100644
index 0000000..7a31865
--- /dev/null
+++ b/src/verilog/Test.v
@@ -0,0 +1,73 @@
+From coqup Require Import Verilog Veriloggen Coquplib Value.
+From compcert Require Import AST Errors Maps Op Integers.
+From compcert Require RTL.
+From Coq Require Import FSets.FMapPositive.
+Import ListNotations.
+Import HexNotationValue.
+Local Open Scope word_scope.
+
+Definition test_module : module :=
+  let mods := [
+      Valways (Vposedge 3%positive) (Vseq (Vnonblock (Vvar 6%positive) (Vlit (ZToValue 32 5)))
+                                          (Vnonblock (Vvar 7%positive)
+                                                     (Vvar 6%positive)))
+      ] in
+  mkmodule (1%positive, 1%nat)
+           (2%positive, 1%nat)
+           (3%positive, 1%nat)
+           (4%positive, 1%nat)
+           (5%positive, 32%nat)
+           (6%positive, 32%nat)
+           nil
+           mods.
+
+Definition test_input : RTL.function :=
+  let sig := mksignature nil Tvoid cc_default in
+  let params := nil in
+  let stacksize := 0 in
+  let entrypoint := 3%positive in
+  let code := PTree.set 1%positive (RTL.Ireturn (Some 1%positive))
+               (PTree.set 3%positive (RTL.Iop (Ointconst (Int.repr 5)) nil 1%positive 1%positive)
+                          (PTree.empty RTL.instruction)) in
+  RTL.mkfunction sig params stacksize code entrypoint.
+
+Definition test_input_program : RTL.program :=
+  mkprogram [(1%positive, Gfun (Internal test_input))] nil 1%positive.
+
+Compute transf_program test_input_program.
+
+Definition test_output_module : module :=
+  {| mod_start := (4%positive, 1%nat);
+     mod_reset := (5%positive, 1%nat);
+     mod_clk := (6%positive, 1%nat);
+     mod_finish := (2%positive, 1%nat);
+     mod_return := (3%positive, 32%nat);
+     mod_state := (7%positive, 32%nat);
+     mod_args := [];
+     mod_body :=
+       [Valways_ff (Vposedge 6%positive)
+                   (Vcond (Vbinop Veq (Vinputvar 5%positive) (1'h"1"))
+                          (Vnonblock (Vvar 7%positive) (32'h"3"))
+                          (Vcase (Vvar 7%positive)
+                                 [(Vlit (32'h"1"), Vnonblock (Vvar 7%positive) (32'h"1"));
+                                 (Vlit (32'h"3"), Vnonblock (Vvar 7%positive) (32'h"1"))]
+                                 (Some Vskip)));
+       Valways_ff (Vposedge 6%positive)
+                  (Vcase (Vvar 7%positive)
+                         [(Vlit (32'h"1"), Vseq (Vblock (Vvar 2%positive) (Vlit (1'h"1")))
+                                                (Vblock (Vvar 3%positive) (Vvar 1%positive)));
+                         (Vlit (32'h"3"), Vblock (Vvar 1%positive) (Vlit (32'h"5")))]
+                         (Some Vskip));
+       Vdecl 1%positive 32; Vdecl 7%positive 32] |}.
+
+Lemma valid_test_output :
+  transf_program test_input_program = OK test_output_module.
+Proof. trivial. Qed.
+
+Lemma manual_simulation :
+  forall f,
+  step (State test_output_module empty_assoclist
+              (initial_fextclk test_output_module)
+              1%nat 1%positive)
+       (State test_output_module test_output_module (add_assoclist 7 (32'h"3") empty_assoclist)
+              2%nat 3%positive).