From 4c6993bf87dd6419e42387148c2b1d899e47fe73 Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Mon, 9 Nov 2020 19:57:08 -0800
Subject: 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>---
 .../firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala   | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/main')

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")
-- 
cgit v1.2.3