aboutsummaryrefslogtreecommitdiffstats
path: root/driver/VericertDriver.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-22 19:26:01 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-22 19:26:01 +0100
commit2ff1316847b9d338a792f67b7b9f6364d4b65551 (patch)
tree6aaf069a05f889d6f3fe012332a5e74dd8707429 /driver/VericertDriver.ml
parentc114bd7a269824623f2dbb41322d95d5056fca02 (diff)
parent8386bed39f413bb461c19debbad92e85f927c4b5 (diff)
downloadvericert-kvx-2ff1316847b9d338a792f67b7b9f6364d4b65551.tar.gz
vericert-kvx-2ff1316847b9d338a792f67b7b9f6364d4b65551.zip
Merge remote-tracking branch 'origin/develop' into develop
Diffstat (limited to 'driver/VericertDriver.ml')
-rw-r--r--driver/VericertDriver.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 0706d79..1ea580f 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -65,7 +65,6 @@ let compile_c_file sourcename ifile ofile =
set_dest Vericert.PrintClight.destination option_dclight ".light.c";
set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
- set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -93,7 +92,7 @@ let compile_c_file sourcename ifile ofile =
end else begin
let verilog =
let translation = if !option_hls_schedule
- then Vericert.Compiler0.transf_hls_temp
+ then Vericert.Compiler0.transf_hls
else Vericert.Compiler0.transf_hls
in
match translation csyntax with