diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 10:04:21 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 10:04:21 +0000 |
| commit | 8a0bd7b74939b65a89b81352b238d1d8252fb278 (patch) | |
| tree | bd6a099b74e2035da32fe963c688c907f9c46722 /src/extraction | |
| parent | fd52cc1edbe192e3a4b6e6780be8761d5702664b (diff) | |
| download | vericert-8a0bd7b74939b65a89b81352b238d1d8252fb278.tar.gz vericert-8a0bd7b74939b65a89b81352b238d1d8252fb278.zip | |
Add extraction and loop pipelining stage
Diffstat (limited to 'src/extraction')
| -rw-r--r-- | src/extraction/Extraction.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index e8cfe50..7736bfa 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -22,7 +22,8 @@ From vericert Require RTLBlockgen RTLBlock HTLSchedulegen - HTLgen. + HTLgen + Pipeline. From Coq Require DecidableClass. @@ -169,6 +170,7 @@ 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 => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". Extract Constant HTLSchedulegen.transl_module => "Schedule.transl_module". @@ -179,9 +181,9 @@ Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls vericert.Compiler.transf_hls_temp - vericert.Compiler.transf_hls_opt RTLBlockgen.transl_program RTLBlock.successors_instr HTLgen.tbl_to_case_expr + Pipeline.pipeline Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state |