From b2dca514919e07400925fbccc93521ffd7650f55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 2 Nov 2020 16:41:51 -0800 Subject: [PATCH 1/3] smt: add test for write port collision --- .../experimental/smt/end2end/MemorySpec.scala | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala b/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala index e38195e2a4..9de4da6f55 100644 --- a/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala +++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala @@ -110,4 +110,65 @@ class MemorySpec extends EndToEndSMTBaseSpec { annos = Seq(MemoryArrayInitAnnotation(m(4), Seq(1, 2, 2, 3))) ) } + + def collisionTest(assumption: String) = s""" + |circuit CollisionTest: + | module CollisionTest: + | input c : Clock + | input preset: AsyncReset + | input addr : UInt<8> + | input data : UInt<32> + | input aEn : UInt<1> + | input bEn : UInt<1> + | + | reg cycle: UInt<8>, c with: (reset => (preset, UInt(0))) + | cycle <= add(cycle, UInt(1)) + | node pastValid = geq(cycle, UInt(1)) + | + | reg prevAddr: UInt<8>, c + | prevAddr <= addr + | reg prevData: UInt<32>, c + | prevData <= data + | reg prevEn: UInt<1>, c + | prevEn <= or(aEn, bEn) + | + | mem m: + | data-type => UInt<32> + | depth => 32 + | reader => r + | writer => a, b + | read-latency => 0 + | write-latency => 1 + | read-under-write => undefined + | + | ; the readport is used to verify the written value + | m.r.clk <= c + | m.r.en <= UInt(1) + | m.r.addr <= prevAddr + | + | ; both read ports write to the same address and the same data + | m.a.clk <= c + | m.a.en <= aEn + | m.a.addr <= addr + | m.a.data <= data + | m.a.mask <= UInt(1) + | m.b.clk <= c + | m.b.en <= bEn + | m.b.addr <= addr + | m.b.data <= data + | m.b.mask <= UInt(1) + | + | ; we assume that writes are mutually exclusive + | ; => no collision should occur + | assume(c, $assumption, UInt(1), "") + | + | ; we check that we always read the last written value + | assert(c, eq(m.r.data, prevData), and(pastValid, prevEn), "") + |""".stripMargin + "memory with two write ports" should "not have collisions when enables are mutually exclusive" taggedAs (RequiresZ3) in { + test(collisionTest("not(and(aEn, bEn))"), MCSuccess, kmax = 4) + } + "memory with two write ports" should "can have collisions when enables are unconstrained" taggedAs (RequiresZ3) in { + test(collisionTest("UInt(1)"), MCFail(1), kmax = 1) + } } From d40d2063ab7be7bbe90c51b95d73e810a99e1958 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 9 Nov 2020 11:39:39 -0800 Subject: [PATCH 2/3] smt: add missing call to insertDummyAssignsForMemoryOutputs --- .../backends/experimental/smt/FirrtlToTransitionSystem.scala | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala index 2c10dbcc1b..6d9c000478 100644 --- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala +++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala @@ -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") From c55c90786c8831124cee5a959015b64fddd10588 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 9 Nov 2020 11:41:24 -0800 Subject: [PATCH 3/3] smt: fix typo in write port code --- .../backends/experimental/smt/FirrtlToTransitionSystem.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala index 6d9c000478..8bc5168944 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))