Add option to turn off if-conversion

7 files changed, 33 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index e50a543..763c892 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ COQMAKE := $(COQBIN)coq_makefile
 
 COQDOCFLAGS := --no-lib-name -l
 
-VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v)
+VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls, src/$(d)/*.v)
 
 PREFIX ?= .
 
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 6887b56..d2c301f 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -249,7 +249,8 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -fcommon       Put uninitialized globals in the common section [on].
 
 HLS Optimisations:
-  -fschedule     Schedule the resulting hardware [off].
+  -fschedule      Schedule the resulting hardware [off].
+  -fif-conversion If-conversion optimisation [off].
 |} ^
  target_help ^
  toolchain_help ^
@@ -434,6 +435,7 @@ let cmdline_actions =
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
   @ f_opt "schedule" option_hls_schedule
+  @ f_opt "if-conv" option_fif_conv
   @ [
 (* Catch options that are not handled *)
   Prefix "-", Self (fun s ->
diff --git a/src/Compiler.v b/src/Compiler.v
index 27cb80c..d99ce56 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -68,6 +68,7 @@ Require vericert.hls.RTLPargen.
 Require vericert.hls.HTLPargen.
 Require vericert.hls.Pipeline.
 Require vericert.hls.IfConversion.
+Require vericert.HLSOpts.
 
 Require Import vericert.hls.HTLgenproof.
 
@@ -235,7 +236,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 7)
   @@@ RTLBlockgen.transl_program
    @@ print (print_RTLBlock 1)
-   @@ IfConversion.transf_program
+   @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
    @@ print (print_RTLBlock 2)
   @@@ RTLPargen.transl_program
   @@@ HTLPargen.transl_program
diff --git a/src/HLSOpts.v b/src/HLSOpts.v
new file mode 100644
index 0000000..173300d
--- /dev/null
+++ b/src/HLSOpts.v
@@ -0,0 +1,19 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Parameter optim_if_conversion: unit -> bool.
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 26b4053..534962b 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -6,3 +6,4 @@ let option_initial = ref false
 let option_dhtl = ref false
 let option_drtlblock = ref false
 let option_hls_schedule = ref false
+let option_fif_conv = ref false
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index a4d0bde..8aec96e 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -24,7 +24,8 @@ From vericert Require
      RTLPar
      RTLBlockInstr
      HTLgen
-     Pipeline.
+     Pipeline
+     HLSOpts.
 
 From Coq Require DecidableClass.
 
@@ -131,6 +132,9 @@ Extract Constant Compopts.thumb =>
 Extract Constant Compopts.debug =>
   "fun _ -> !Clflags.option_g".
 
+Extract Constant HLSOpts.optim_if_conversion =>
+  "fun _ -> !VericertClflags.option_fif_conv".
+
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 16103f8..4461d85 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -812,7 +812,7 @@ let rec all_successors dfg v =
 let order_instr dfg =
   DFG.fold_vertex (fun v li ->
       if DFG.in_degree dfg v = 0
-      then (printf "v: %s\n" (print_instr (snd v)); (List.map snd (v :: all_successors dfg v)) :: li)
+      then (List.map snd (v :: all_successors dfg v)) :: li
       else li
     ) dfg []
 
@@ -856,7 +856,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
   fprintf graph "%a\n" GDot.output_graph cgraph;
   close_out graph;
   let schedule' = solve_constraints cgraph in
-  IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';
+  (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
   (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
   transf_rtlpar c c' schedule'