diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-05 23:17:33 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:38:45 +0100 |
| commit | 1c8e0373d735ac88740f96c5da1d929ce3f7b688 (patch) | |
| tree | 60c170715bdc960778f58502f56dcb28775d3e13 /src/Compiler.v | |
| parent | 34a0415ad0c65602ba097c37e23ced9cb3cf390e (diff) | |
| download | vericert-1c8e0373d735ac88740f96c5da1d929ce3f7b688.tar.gz vericert-1c8e0373d735ac88740f96c5da1d929ce3f7b688.zip | |
Move HTL renaming pass to own file
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index b5b33e7..38a9d0e 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.Renaming. Require vericert.hls.HTLgen. Require vericert.hls.RTLBlock. Require vericert.hls.RTLBlockgen. @@ -191,7 +192,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print (print_HTL 1) - @@@ HTLgen.renumber_program + @@@ Renaming.transf_program @@ print (print_HTL 2) @@@ Veriloggen.transl_program. |