aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-11-02 19:38:07 +0000
committerYann Herklotz <git@yannherklotz.com>2020-11-02 19:38:07 +0000
commit2456ba0e08f91538feeb1403beb7de142a054ebe (patch)
tree9aacbf50afd904cff55ff813d3c29cfd86ba24a5 /driver
parent7e77b4ba70aceea384d4c485002c46875fc19695 (diff)
downloadvericert-2456ba0e08f91538feeb1403beb7de142a054ebe.tar.gz
vericert-2456ba0e08f91538feeb1403beb7de142a054ebe.zip
Add optimisations to output
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