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 /src/Compiler.v | |
| parent | 3144c39f4533f0936f3df0537bf470461565f5e9 (diff) | |
| download | vericert-91e9202e6317ab3edd22562d659255d63a3fe65d.tar.gz vericert-91e9202e6317ab3edd22562d659255d63a3fe65d.zip | |
Finish implementing scheduling and add top level export
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 10 |
1 files changed, 7 insertions, 3 deletions
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. |