diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-10-19 18:21:00 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-19 18:21:00 +0100 |
| commit | 92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2 (patch) | |
| tree | 7e8d76015cb35828e371817dfdf1defc46fcfe89 /driver/VericertDriver.ml | |
| parent | afcb12b5e443da586459455dbc637fc04b9d0634 (diff) | |
| download | vericert-92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2.tar.gz vericert-92b6c68cdfd1e42ca1f9ebf70b7292e7c16570c2.zip | |
Finished most of the giblesubpar proof
Diffstat (limited to 'driver/VericertDriver.ml')
| -rw-r--r-- | driver/VericertDriver.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 5950e95..6cd8e1f 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -67,6 +67,7 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; set_dest Vericert.PrintGibleSeq.destination option_dgblseq ".gblseq"; set_dest Vericert.PrintGiblePar.destination option_dgblpar ".gblpar"; + set_dest Vericert.PrintGibleSubPar.destination option_dgblsubpar ".gblsubpar"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.PrintDHTL.destination option_ddhtl ".dhtl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; @@ -270,6 +271,7 @@ HLS Optimisations: -drtl Save RTL at various optimization points in <file>.rtl.<n> -dgblseq Save GibleSeq <file>.gblseq -dgblpar Save GiblePar <file>.gblpar + -dgblsubpar Save GibleSubPar <file>.gblsubpar -dhtl Save HTL before Verilog generation <file>.htl -dltl Save LTL after register allocation in <file>.ltl -dmach Save generated Mach code in <file>.mach @@ -412,6 +414,7 @@ let cmdline_actions = option_drtl := true; option_dgblseq := true; option_dgblpar := true; + option_dgblsubpar := true; option_dhtl := true; option_ddhtl := true; option_dltl := true; |