diff options
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") |