From b91f6db17ee30efd2068efbeecbf1d2b4c3850ea Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 9 Dec 2021 20:06:34 +0000 Subject: Add bourdoncle to build --- src/extraction/Extraction.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'src/extraction') 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 -- cgit