From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 27 May 2020 14:00:57 +0000 (-0400)
Subject: Fix bug in alu main stage proof
X-Git-Tag: div_pipeline~799
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d2259bb2d8585516c887438084032e842533b327;p=soc.git

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 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