projects
/
soc.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Count zero_a and imm_data.ok as masked read transactions
[soc.git]
/
src
/
soc
/
experiment
/
formal
/
proof_compalu_multi.py
diff --git
a/src/soc/experiment/formal/proof_compalu_multi.py
b/src/soc/experiment/formal/proof_compalu_multi.py
index d81f35e12151518a77a2bf5358016acef9c7952c..8f75b7b070f8ae783cf14d9ceaa6ad7fb50ad0ea 100644
(file)
--- 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
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
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)
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
cnt_masked_read.append(cnt)
# Ask the formal engine to give an example