projects / soc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0d9b75a) | patch
Check invariant for instruction operands
authorCesar Strauss <cestrauss@gmail.com>
Wed, 12 Oct 2022 13:32:49 +0000 (10:32 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Wed, 12 Oct 2022 13:38:58 +0000 (10:38 -0300)
commit099825f7d53fb64adb30e363fd359eda3d1f14cd
tree4a47ae521d6ba85a1f2cf26c3f51c4509b6b9f96tree
parent0d9b75ad1ae14b0f645e5a1bde343c1db85274a7commit | diff
Check invariant for instruction operands

For every instruction issued, at any point in time, each operand
was either:
1) Already read
2) Not read yet, but the read is pending (rel_o high)
3) Masked
src/soc/experiment/formal/proof_compalu_multi.py diff | blob | history