From 2c5f867a347637cf1b651da7d041d9670493f540 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Fri, 30 Apr 2021 16:07:43 +0100 Subject: Fix map_externctrl double-incrementing freshreg --- src/hls/HTLgen.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index aa1064b..5400e25 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -163,10 +163,9 @@ Next Obligation. constructor; simpl; auto with htlh. Qed. Program Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := do r <- create_reg None (controlsignal_sz ctrl); - fun s => let r := s.(st_freshreg) in - OK r (mkstate + fun s => OK r (mkstate s.(st_st) - (Pos.succ r) + (st_freshreg s) (st_freshstate s) (st_scldecls s) (st_arrdecls s) -- cgit