projects
/
soc.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(from:
7df58b3
)
Add formal verification of the single port memory block
author
Cesar Strauss
<cestrauss@gmail.com>
Sat, 26 Mar 2022 21:09:12 +0000
(18:09 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sat, 26 Mar 2022 21:36:04 +0000
(18:36 -0300)
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.
No differences found