diff options
Diffstat (limited to 'src/extraction/Extraction.v')
| -rw-r--r-- | src/extraction/Extraction.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 9b82e1b..395ec47 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -24,9 +24,10 @@ From vericert Require RTLPar RTLBlockInstr HTLgen - Pipeline + (*Pipeline*) HLSOpts Predicate + Bourdoncle . From Coq Require DecidableClass. @@ -182,10 +183,13 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false". 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 Pipeline.pipeline => "pipelining.pipeline".*) Extract Constant RTLBlockgen.partition => "Partition.partition". Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +(* Loop normalization *) +Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". + (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -195,9 +199,9 @@ Separate Extraction vericert.Compiler.transf_hls_temp RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr - Pipeline.pipeline Predicate.sat_pred_simple Verilog.stmnt_to_list + Bourdoncle.bourdoncle Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state |