X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Fexperiment%2Fformal%2Fproof_compalu_multi.py;h=8f75b7b070f8ae783cf14d9ceaa6ad7fb50ad0ea;hb=5fe221fda62b538a9f49784e28bd9e7b69923b8d;hp=d81f35e12151518a77a2bf5358016acef9c7952c;hpb=e3654a3502e0770d7af2fb168ef016a6a398b233;p=soc.git

diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py
index d81f35e1..8f75b7b0 100644
--- a/src/soc/experiment/formal/proof_compalu_multi.py
+++ b/src/soc/experiment/formal/proof_compalu_multi.py
@@ -35,7 +35,7 @@ https://bugs.libre-soc.org/show_bug.cgi?id=197
 import unittest
 
 from nmigen import Signal, Module
-from nmigen.hdl.ast import Cover
+from nmigen.hdl.ast import Cover, Const
 from nmutil.formaltest import FHDLTestCase
 from nmutil.singlepipe import ControlBase
 
@@ -141,7 +141,13 @@ class CompALUMultiTestCase(FHDLTestCase):
         cnt_masked_read = []
         for i in range(dut.n_src):
             cnt = Signal(4, name="cnt_masked_read_%d" % i)
-            m.d.sync += cnt.eq(cnt + (do_issue & dut.rdmaskn[i]))
+            if i == 0:
+                extra = dut.oper_i.zero_a
+            elif i == 1:
+                extra = dut.oper_i.imm_data.ok
+            else:
+                extra = Const(0, 1)
+            m.d.sync += cnt.eq(cnt + (do_issue & (dut.rdmaskn[i] | extra)))
             cnt_masked_read.append(cnt)
 
         # Ask the formal engine to give an example