aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/VericertDriver.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 7dfde28..0c02aeb 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -92,7 +92,10 @@ let compile_c_file sourcename ifile ofile =
close_out oc
end else begin
let verilog =
- let translation = if !option_hls_schedule then Vericert.Compiler0.transf_hls_temp else Vericert.Compiler0.transf_hls in
+ let translation = if !option_hls_schedule
+ then Vericert.Compiler0.transf_hls_temp
+ else Vericert.Compiler0.transf_hls_opt
+ in
match translation csyntax with
| Vericert.Errors.OK v ->
v