From 7d637e256d09e46c5b45c9ac3b6258e43c279f2a Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Wed, 11 Nov 2020 12:12:45 -0800
Subject: smt: add support for write-first memories (#1948)

---
 .../experimental/smt/end2end/MemorySpec.scala      | 26 +++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

(limited to 'src/test')

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 9de4da6f..e489db7d 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
@@ -45,7 +45,7 @@ class MemorySpec extends EndToEndSMTBaseSpec {
        |    ${cmds.mkString("\n    ")}
        |""".stripMargin
 
-  "Registered test memory" should "return written data after two cycles" taggedAs (RequiresZ3) in {
+  "Registered read-first memory" should "return written data after two cycles" taggedAs (RequiresZ3) in {
     val cmds =
       """node past_past_valid = geq(cycle, UInt(2))
         |reg past_in: UInt<8>, clock
@@ -61,6 +61,30 @@ class MemorySpec extends EndToEndSMTBaseSpec {
     test(registeredTestMem("Mem00", cmds, "old"), MCSuccess, kmax = 3)
   }
 
+  "Registered read-first memory" should "not return written data after one cycle" taggedAs (RequiresZ3) in {
+    val cmds =
+      """
+        |reg past_in: UInt<8>, clock
+        |past_in <= in
+        |
+        |assume(clock, eq(read_addr, write_addr), UInt(1), "read_addr = write_addr")
+        |assert(clock, eq(out, past_in), past_valid, "out = past(in)")
+        |""".stripMargin
+    test(registeredTestMem("Mem00", cmds, "old"), MCFail(1), kmax = 3)
+  }
+
+  "Registered write-first memory" should "return written data after one cycle" taggedAs (RequiresZ3) in {
+    val cmds =
+      """
+        |reg past_in: UInt<8>, clock
+        |past_in <= in
+        |
+        |assume(clock, eq(read_addr, write_addr), UInt(1), "read_addr = write_addr")
+        |assert(clock, eq(out, past_in), past_valid, "out = past(in)")
+        |""".stripMargin
+    test(registeredTestMem("Mem00", cmds, "new"), MCSuccess, kmax = 3)
+  }
+
   private def readOnlyMem(pred: String, num: Int) =
     s"""circuit Mem0$num:
        |  module Mem0$num:
-- 
cgit v1.2.3