Fix bug in alu main stage proof

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 4ef8ef978f0d812cb37828e47c67310599599031..90854c1d8eace4c310dbadab13ed9451cf09879c 100644 (file)
--- 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