From 0b118f8dca9068e0075e72f4d0c24cf707df44c7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 3 May 2020 17:13:56 +0100 Subject: Add code to debug execution of HLS --- debug/CoqupTest.ml | 59 +++++++++++++++++++++++++++++++++++++++++++ debug/dune | 5 ++++ src/verilog/Test.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 137 insertions(+) create mode 100644 debug/CoqupTest.ml create mode 100644 debug/dune create mode 100644 src/verilog/Test.v 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). -- cgit