From 91e9202e6317ab3edd22562d659255d63a3fe65d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 20 Oct 2020 18:44:59 +0100 Subject: Finish implementing scheduling and add top level export --- src/Compiler.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'src/Compiler.v') 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. -- cgit