projects / soc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7df58b3) | patch
Finish the SRAM formal proof by implementing induction
authorCesar Strauss <cestrauss@gmail.com>
Sun, 27 Mar 2022 17:23:39 +0000 (14:23 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Sun, 27 Mar 2022 17:32:37 +0000 (14:32 -0300)
commitec40b7ea2b43a9874db3aa1400545ab469844779
treeeeebf9e19c6745c82df254fb82c2fa5ed6a86d9dtree
parent7df58b30dcefe51c547db4102db41a58e5124922commit | diff
Finish the SRAM formal proof by implementing induction

Add a combinatorial (no delay) debug read port to the SRAM model,
for turning an unreacheable state (memory and holding register differ)
into an illegal state.
Just two clock cycles are needed for a working proof.
src/soc/regfile/sram_wrapper.py diff | blob | history