diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-10-20 18:44:59 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-10-20 18:44:59 +0100 |
| commit | 91e9202e6317ab3edd22562d659255d63a3fe65d (patch) | |
| tree | 40101a29bfc14f5770ea8e367571c2cec7bc8275 | |
| parent | 3144c39f4533f0936f3df0537bf470461565f5e9 (diff) | |
| download | vericert-kvx-91e9202e6317ab3edd22562d659255d63a3fe65d.tar.gz vericert-kvx-91e9202e6317ab3edd22562d659255d63a3fe65d.zip | |
Finish implementing scheduling and add top level export
| -rw-r--r-- | driver/VericertDriver.ml | 2 | ||||
| -rw-r--r-- | src/Compiler.v | 10 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 4 | ||||
| -rw-r--r-- | src/hls/Partition.ml | 2 |
4 files changed, 12 insertions, 6 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 2b8d45f..0362456 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -98,7 +98,7 @@ let compile_c_file sourcename ifile ofile = let loc = file_loc sourcename in fatal_error loc "%a" print_error msg in let oc = open_out ofile in - Vericert.PrintRTLBlock.print_program oc verilog; + Vericert.PrintVerilog.print_program !option_debug_hls oc verilog; close_out oc end diff --git a/src/Compiler.v b/src/Compiler.v index ff8c523..cceb87d 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -53,7 +53,8 @@ From vericert Require Veriloggenproof HTLgen RTLBlock - RTLBlockgen. + RTLBlockgen + HTLSchedulegen. From compcert Require Import Smallstep. @@ -101,7 +102,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@ print (print_RTL 0) @@@ transf_backend. -Definition transf_hls_temp (p : Csyntax.program) : res RTLBlock.program := +Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -111,7 +112,10 @@ Definition transf_hls_temp (p : Csyntax.program) : res RTLBlock.program := @@@ RTLgen.transl_program @@ Renumber.transf_program @@ print (print_RTL 0) - @@@ RTLBlockgen.transl_program. + @@@ RTLBlockgen.transl_program + @@@ HTLSchedulegen.transl_program + @@ print print_HTL + @@ Veriloggen.transl_program. Local Open Scope linking_scope. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 6fc8545..f7131b0 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -21,7 +21,8 @@ From vericert Require Value Compiler RTLBlockgen - RTLBlock. + RTLBlock + HTLSchedulegen. From Coq Require DecidableClass. @@ -168,6 +169,7 @@ Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant RTLBlockgen.partition => "Partition.partition". +Extract Constant HTLSchedulegen.transl_module => "Schedule.transl_module". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index d8e7ff7..224cdc9 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -117,7 +117,7 @@ let function_from_RTL f = fn_stacksize = f.RTL.fn_stacksize; fn_params = f.RTL.fn_params; fn_entrypoint = f.RTL.fn_entrypoint; - fn_code = Schedule.schedule f.RTL.fn_entrypoint c + fn_code = c } let partition = function_from_RTL |