From d2259bb2d8585516c887438084032e842533b327 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 27 May 2020 10:00:57 -0400 Subject: [PATCH] Fix bug in alu main stage proof --- src/soc/fu/alu/formal/proof_main_stage.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py index 4ef8ef97..90854c1d 100644 --- a/src/soc/fu/alu/formal/proof_main_stage.py +++ b/src/soc/fu/alu/formal/proof_main_stage.py @@ -67,8 +67,9 @@ class Driver(Elaboratable): comb += a_signed.eq(a) comb += a_signed_32.eq(a[0:32]) - comb += Assume(a[32:64] == 0) - comb += Assume(b[32:64] == 0) + with m.If(rec.is_32bit): + comb += Assume(a[32:64] == 0) + comb += Assume(b[32:64] == 0) o_ok = Signal() comb += o_ok.eq(1) # will be set to zero if no op takes place -- 2.30.2