From 91e9202e6317ab3edd22562d659255d63a3fe65d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 20 Oct 2020 18:44:59 +0100
Subject: Finish implementing scheduling and add top level export

---
 driver/VericertDriver.ml    |  2 +-
 src/Compiler.v              | 10 +++++++---
 src/extraction/Extraction.v |  4 +++-
 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
-- 
cgit