projects / soc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6828f2a) | patch
Formal proof of the phased write dual port memory wrapper
authorCesar Strauss <cestrauss@gmail.com>
Sun, 3 Apr 2022 18:24:16 +0000 (15:24 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Sun, 3 Apr 2022 18:27:51 +0000 (15:27 -0300)
commit9764dfc9c5d0fc8dff70c73cc4475d1087b155aa
tree31975312f30ebfeda31fa6a90b771260787a8dc7tree
parent6828f2a2930ffd8f3ba4a6aee75315972d856a56commit | diff
Formal proof of the phased write dual port memory wrapper

Similar to the proof of the 1RW memory block, but read and writes are
done on dedicated ports.
For now, only transparent regfile is tested.
To complete the formal verification, an induction proof will follow.
src/soc/regfile/sram_wrapper.py diff | blob | history