projects
/
soc.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Allow the formal engine to perform a same-cycle result in the ALU
[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 bf6d2615b8142c15561cc63ca946ce718547e227..96b61a2b6a0375d37347a5ba19d675900ef97a40 100644
(file)
--- a/
src/soc/experiment/formal/proof_compalu_multi.py
+++ b/
src/soc/experiment/formal/proof_compalu_multi.py
@@
-153,7
+153,7
@@
class CompALUMultiTestCase(FHDLTestCase):
m.d.sync += cnt.eq(cnt + do_masked_read[i])
cnt_masked_read.append(cnt)
# If the ALU is idle, do not assert valid
m.d.sync += cnt.eq(cnt + do_masked_read[i])
cnt_masked_read.append(cnt)
# If the ALU is idle, do not assert valid
- with m.If(
cnt_alu_read == cnt
_alu_write):
+ with m.If(
(cnt_alu_read == cnt_alu_write) & ~do
_alu_write):
m.d.comb += Assume(~alu.n.o_valid)
# Keep ALU valid high, until read
last_alu_valid = Signal()
m.d.comb += Assume(~alu.n.o_valid)
# Keep ALU valid high, until read
last_alu_valid = Signal()