From 1c8e0373d735ac88740f96c5da1d929ce3f7b688 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sat, 5 Jun 2021 23:17:33 +0100 Subject: Move HTL renaming pass to own file --- src/Compiler.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Compiler.v') 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. -- cgit