diff options
| author | Kevin Laeufer | 2020-11-09 19:57:08 -0800 |
|---|---|---|
| committer | GitHub | 2020-11-10 03:57:08 +0000 |
| commit | 4c6993bf87dd6419e42387148c2b1d899e47fe73 (patch) | |
| tree | 92e8399177a11039da2449e75fddfb944cc9981f /src/main | |
| parent | 92af63c599fc480f6480ee22f23763f54881085f (diff) | |
Fix SMT Memory Bug (#1942)
* smt: add test for write port collision
* smt: add missing call to insertDummyAssignsForMemoryOutputs
* smt: fix typo in write port code
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala index 2c10dbcc..8bc51689 100644 --- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala +++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala @@ -421,7 +421,7 @@ private class MemoryEncoding(makeRandom: (String, Int) => BVExpr) extends LazyLo val bothWrite = and(doWrite, w.doWrite) val sameAddress = BVEqual(addr, w.addr) if (bothWrite == True) { sameAddress } - else { and(doWrite, sameAddress) } + else { and(bothWrite, sameAddress) } } def writeTo(array: ArrayExpr): ArrayExpr = { val doUpdate = if (memory.fullAddressRange) doWrite else and(doWrite, memory.isValidAddress(addr)) @@ -567,6 +567,8 @@ private class ModuleScanner(makeRandom: (String, Int) => BVExpr) extends LazyLog if (op == ir.Formal.Cover) { logger.warn(s"WARN: Cover statement was ignored: ${s.serialize}") } else { + insertDummyAssignsForMemoryOutputs(pred) + insertDummyAssignsForMemoryOutputs(en) val name = namespace.newName(msgToName(op.toString, msg.string)) val predicate = onExpression(pred, name + "_predicate") val enabled = onExpression(en, name + "_enabled") |