diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 01:05:32 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 01:05:32 +0100 |
| commit | 0a44da6a7037d9eb270386eeef4f929177c4ec0d (patch) | |
| tree | ac08c768bbdedda7d791972ee0e2c4db1fb5ac14 /src/extraction | |
| parent | 27714f85233e52978caebd67b550bde51e693d48 (diff) | |
| download | vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.tar.gz vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.zip | |
Rewrite a lot fixing scheduling of Gible
Diffstat (limited to 'src/extraction')
| -rw-r--r-- | src/extraction/Extraction.v | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 395ec47..88bb3e8 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -19,10 +19,10 @@ From vericert Require Verilog Compiler - RTLBlockgen - RTLBlock - RTLPar - RTLBlockInstr + GibleSeqgen + GibleSeq + GiblePar + Gible HTLgen (*Pipeline*) HLSOpts @@ -145,11 +145,9 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". -Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". -Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". +Extract Constant Compiler.print_GibleSeq => "PrintGibleSeq.print_if". +Extract Constant Compiler.print_GiblePar => "PrintGiblePar.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". -Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". -Extract Constant Compiler.print_RTLParFU => "PrintRTLParFU.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". @@ -184,8 +182,8 @@ Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". (*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*) -Extract Constant RTLBlockgen.partition => "Partition.partition". -Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +Extract Constant GibleSeqgen.partition => "Partition.partition". +Extract Constant GiblePargen.schedule => "Schedule.schedule_fn". (* Loop normalization *) Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". @@ -197,7 +195,7 @@ Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls vericert.Compiler.transf_hls_temp - RTLBlockgen.transl_program RTLBlockInstr.successors_instr + GibleSeqgen.transl_program Gible.successors_instr HTLgen.tbl_to_case_expr Predicate.sat_pred_simple Verilog.stmnt_to_list |