projects / soc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 36f8a92) | patch
Add formal verification of the single port memory block
authorCesar Strauss <cestrauss@gmail.com>
Sat, 26 Mar 2022 21:09:12 +0000 (18:09 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Sat, 26 Mar 2022 21:36:04 +0000 (18:36 -0300)
commit7df58b30dcefe51c547db4102db41a58e5124922
tree841148c868a6ffc5823bd9c9c256267fa73dc61btree
parent36f8a92eb6e900f69a375d793602b9353c32a540commit | diff
Add formal verification of the single port memory block

We test a single, random memory location.
If any memory location, chosen at random, passes, then the whole memory
is correct.
Note that an induction proof is still missing, since it requires
additional assertions to avoid illegal states.
src/soc/regfile/sram_wrapper.py diff | blob | history