Add compilation flag for superblock scheduling

8 files changed, 18 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 690536f..4e44eeb 100644
--- a/Makefile
+++ b/Makefile
@@ -45,7 +45,7 @@ install:
 	install -d $(PREFIX)/bin
 	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
 	install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.
-	install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert
+	install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert-kvx
 
 proof: Makefile.coq
 	$(MAKE) -f Makefile.coq
diff --git a/benchmarks/polybench-syn/common.mk b/benchmarks/polybench-syn/common.mk
index 8e67294..fde097d 100644
--- a/benchmarks/polybench-syn/common.mk
+++ b/benchmarks/polybench-syn/common.mk
@@ -1,11 +1,11 @@
-VERICERT ?= vericert
+VERICERT ?= vericert-kvx
 VERICERT_OPTS ?= -DSYNTHESIS -fschedule -fif-conv
 
 IVERILOG ?= iverilog
 IVERILOG_OPTS ?=
 
 VERILATOR ?= verilator
-VERILATOR_OPTS ?= -Wno-fatal --top main --exe /home/ymherklotz/projects/vericert/scripts/verilator_main.cpp
+VERILATOR_OPTS ?= -Wno-fatal --top main --exe $(HOME)/projects/vericert-kvx/scripts/verilator_main.cpp
 
 TARGETS ?=
 
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index e89ff86..1dd225a 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -253,7 +253,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
 
 HLS Optimisations:
   -fschedule      Schedule the resulting hardware [off].
-  -fif-conversion If-conversion optimisation [off].
+  -fif-conv       If-conversion optimisation [off].
 |} ^
  target_help ^
  toolchain_help ^
@@ -443,6 +443,7 @@ let cmdline_actions =
   @ f_opt "sse" option_ffpu (* backward compatibility *)
   @ f_opt "schedule" option_hls_schedule
   @ f_opt "if-conv" option_fif_conv
+  @ f_opt "superblock" option_fsuperblock
   @ f_opt "ram" option_fram
   @ [
 (* Catch options that are not handled *)
diff --git a/lib/CompCert b/lib/CompCert
-Subproject 5987aafe3bf6b6382f0a90c9209a7c79be1cab3
+Subproject 9c72ffe762dc2f90109d5991f74ee0ee4e9a8ec
diff --git a/src/Compiler.v b/src/Compiler.v
index 636346c..504246e 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -198,6 +198,12 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 0)
   @@@ transf_backend.
 
+Definition transf_superblock p :=
+  OK p
+     @@@ (time "RTLpath generation" RTLpathLivegen.transf_program)
+     @@@ (time "Prepass scheduling" RTLpathScheduler.transf_program)
+     @@ (time "Projection to RTL" RTLpath.transf_program).
+
 (* This is an unverified version of transf_hls with some experimental additions such as scheduling
 that aren't completed yet. *)
 Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
@@ -221,7 +227,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 6)
   @@@ time "Unused globals" Unusedglob.transf_program
-   @@ print (print_RTL 7)
+  @@ print (print_RTL 7)
+  @@@ partial_if HLSOpts.optim_superblock transf_superblock
+  @@ print (print_RTL 8)
   @@@ RTLBlockgen.transl_program
    @@ print (print_RTLBlock 0)
    @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
diff --git a/src/HLSOpts.v b/src/HLSOpts.v
index efa7ed0..b9e942e 100644
--- a/src/HLSOpts.v
+++ b/src/HLSOpts.v
@@ -17,5 +17,6 @@
  *)
 
 Parameter optim_if_conversion: unit -> bool.
+Parameter optim_superblock: unit -> bool.
 
 Parameter optim_ram: unit -> bool.
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 0402d49..05996c2 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -9,4 +9,5 @@ let option_drtlpar = ref false
 let option_drtlparfu = ref false
 let option_hls_schedule = ref false
 let option_fif_conv = ref false
+let option_fsuperblock = ref false
 let option_fram = ref true
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 044a086..6e9405f 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -199,6 +199,8 @@ Extract Constant Abstr.cf_instr_eq => "(fun _ _ -> true)".
 
 Extract Constant HLSOpts.optim_if_conversion =>
   "fun _ -> !VericertClflags.option_fif_conv".
+Extract Constant HLSOpts.optim_superblock =>
+  "fun _ -> !VericertClflags.option_fsuperblock".
 Extract Constant HLSOpts.optim_ram =>
   "fun _ -> !VericertClflags.option_fram".