diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:39:04 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:39:04 +0100 |
| commit | 77c5c01146fa9e2fa09779c1da642b8f5469dff5 (patch) | |
| tree | 30d98d7302451a0423635ec807f7c97026d48382 /src/Compiler.v | |
| parent | 1c8e0373d735ac88740f96c5da1d929ce3f7b688 (diff) | |
| download | vericert-77c5c01146fa9e2fa09779c1da642b8f5469dff5.tar.gz vericert-77c5c01146fa9e2fa09779c1da642b8f5469dff5.zip | |
Make externctrl application its own HTL pass
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 38a9d0e..ea3720a 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -61,6 +61,7 @@ Require Import compcert.lib.Coqlib. Require vericert.hls.Verilog. Require vericert.hls.Veriloggen. Require vericert.hls.Veriloggenproof. +Require vericert.hls.ApplyExternctrl. Require vericert.hls.Renaming. Require vericert.hls.HTLgen. Require vericert.hls.RTLBlock. @@ -194,6 +195,8 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_HTL 1) @@@ Renaming.transf_program @@ print (print_HTL 2) + @@@ ApplyExternctrl.transf_program + @@ print (print_HTL 3) @@@ Veriloggen.transl_program. Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@ -297,7 +300,7 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T. + unfold transf_backend, time in T. rewrite ! compose_print_identity in T. destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. set (p8 := Renumber.transf_program p7) in *. set (p9 := total_if Compopts.optim_constprop Constprop.transf_program p8) in *. |