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/Compiler.v | |
| parent | 27714f85233e52978caebd67b550bde51e693d48 (diff) | |
| download | vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.tar.gz vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.zip | |
Rewrite a lot fixing scheduling of Gible
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index dc3b1c7..a0b3f24 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -62,8 +62,7 @@ Require vericert.hls.Veriloggenproof. Require vericert.hls.HTLgen. Require vericert.hls.GibleSeq. Require vericert.hls.GibleSeqgen. -Require vericert.hls.RTLPargen. -Require vericert.hls.RTLParFUgen. +Require vericert.hls.GiblePargen. Require vericert.hls.HTLPargen. (*Require vericert.hls.Pipeline.*) Require vericert.hls.IfConversion. @@ -84,9 +83,8 @@ intermediate steps in the compilation, such as ``print_RTL``, ``print_HTL`` and Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: Z -> HTL.program -> unit. -Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. -Parameter print_RTLPar: Z -> RTLPar.program -> unit. -Parameter print_RTLParFU: Z -> RTLParFU.program -> unit. +Parameter print_GibleSeq: Z -> GibleSeq.GibleSeq.program -> unit. +Parameter print_GiblePar: Z -> GiblePar.GiblePar.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -260,14 +258,12 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_RTL 6) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) - @@@ RTLBlockgen.transl_program - @@ print (print_RTLBlock 0) + @@@ GibleSeqgen.transl_program + @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program - @@ print (print_RTLBlock 1) - @@@ RTLPargen.transl_program - @@ print (print_RTLPar 0) - @@@ RTLParFUgen.transl_program - @@ print (print_RTLParFU 0) + @@ print (print_GibleSeq 1) + @@@ GiblePargen.transl_program + @@ print (print_GiblePar 0) @@@ HTLPargen.transl_program @@ print (print_HTL 0) @@ Veriloggen.transl_program. |