| Age | Commit message (Collapse) | Author |
|---|
|
This fixes an off by one error, where 3 was erroneously
accepted as in-bounds for a memory of depth=3
|
|
This finally removes all randomization code from the transition
system conversion and into a separate pass using DefRandom nodes.
|
|
* SMT: memory port inout fields cannot be used as RHS expressions
* smt: add end2end check for read enable modelling
|
|
With this PR the smt backend now supports memories
with more than two write ports and the conservative
memory modelling can be selectively turned off with
a new annotation.
|
