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 | |
| parent | fd52cc1edbe192e3a4b6e6780be8761d5702664b (diff) | |
| download | vericert-kvx-8a0bd7b74939b65a89b81352b238d1d8252fb278.tar.gz vericert-kvx-8a0bd7b74939b65a89b81352b238d1d8252fb278.zip | |
Add extraction and loop pipelining stage
| -rw-r--r-- | src/Compiler.v | 5 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 6 | ||||
| -rw-r--r-- | src/hls/Pipeline.v | 11 |
3 files changed, 19 insertions, 3 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 7df00d8..5895e1d 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -74,7 +74,8 @@ From vericert Require HTLgen RTLBlock RTLBlockgen - HTLSchedulegen. + HTLSchedulegen + Pipeline. From compcert Require Import Smallstep. @@ -240,6 +241,8 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_RTL 6) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) + @@ Pipeline.transf_program + @@ print (print_RTL 8) @@@ RTLBlockgen.transl_program @@ print print_RTLBlock @@@ HTLSchedulegen.transl_program 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 diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v new file mode 100644 index 0000000..ea0c32e --- /dev/null +++ b/src/hls/Pipeline.v @@ -0,0 +1,11 @@ +From compcert Require Import + Maps + AST + RTL. + +Parameter pipeline : function -> function. + +Definition transf_fundef := transf_fundef pipeline. + +Definition transf_program : program -> program := + transform_program transf_fundef. |