SMT: memory port inout fields cannot be used as RHS expressions (#2105)

* SMT: memory port inout fields cannot be used as RHS expressions

* smt: add end2end check for read enable modelling

2 files changed, 59 insertions, 17 deletions

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 e489db7d..2a0276e1 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/end2end/MemorySpec.scala
@@ -195,4 +195,46 @@ class MemorySpec extends EndToEndSMTBaseSpec {
   "memory with two write ports" should "can have collisions when enables are unconstrained" taggedAs (RequiresZ3) in {
     test(collisionTest("UInt(1)"), MCFail(1), kmax = 1)
   }
+
+  private def readEnableSrc(pred: String, num: Int) =
+    s"""
+       |circuit ReadEnableTest$num:
+       |  module ReadEnableTest$num:
+       |    input c : Clock
+       |    input preset: AsyncReset
+       |
+       |    reg first: UInt<1>, c with: (reset => (preset, UInt(1)))
+       |    first <= UInt(0)
+       |
+       |    reg even: UInt<1>, c with: (reset => (preset, UInt(0)))
+       |    node odd = not(even)
+       |    even <= not(even)
+       |
+       |    mem m:
+       |      data-type => UInt<8>
+       |      depth => 4
+       |      reader => r
+       |      read-latency => 1
+       |      write-latency => 1
+       |      read-under-write => undefined
+       |
+       |    m.r.clk <= c
+       |    m.r.addr <= UInt(0)
+       |    ; the read port is enabled in even cycles
+       |    m.r.en <= even
+       |
+       |    assert(c, $pred, not(first), "")
+       |""".stripMargin
+
+  "a memory with read enable" should "supply valid data one cycle after en=1" in {
+    val init = Seq(MemoryScalarInitAnnotation(CircuitTarget(s"ReadEnableTest1").module(s"ReadEnableTest1").ref("m"), 0))
+    // the read port is enabled on even cycles, so on odd cycles we should reliably get zeros
+    test(readEnableSrc("or(not(odd), eq(m.r.data, UInt(0)))", 1), MCSuccess, kmax = 3, annos = init)
+  }
+
+  "a memory with read enable" should "supply invalid data one cycle after en=0" in {
+    val init = Seq(MemoryScalarInitAnnotation(CircuitTarget(s"ReadEnableTest2").module(s"ReadEnableTest2").ref("m"), 0))
+    // the read port is disabled on odd cycles, so on even cycles we should *NOT* reliably get zeros
+    test(readEnableSrc("or(not(even), eq(m.r.data, UInt(0)))", 2), MCFail(1), kmax = 1, annos = init)
+  }
 }
diff --git a/src/test/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorSpec.scala
index c6f89b93..f8f889ac 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorSpec.scala
@@ -13,10 +13,10 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     val result = circuit.serialize.split('\n').map(_.trim)
 
     // a random value should be declared for the data written on a write-write conflict
-    assert(result.contains("rand m_a_wwc_data : UInt<32>, m.a.clk when m_a_b_wwc"))
+    assert(result.contains("rand m_a_wwc_data : UInt<32>, m_a_clk when m_a_b_wwc"))
 
     // a write-write conflict occurs when both ports are enabled and the addresses match
-    assert(result.contains("m_a_b_wwc <= and(and(m_a_en, m_b_en), eq(m.a.addr, m.b.addr))"))
+    assert(result.contains("m_a_b_wwc <= and(and(m_a_en, m_b_en), eq(m_a_addr, m_b_addr))"))
 
     // the data of read port a depends on whether there is a write-write conflict
     assert(result.contains("m.a.data <= mux(m_a_b_wwc, m_a_wwc_data, m_a_data)"))
@@ -35,14 +35,14 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     assert(result.contains("node m_a_wwc_active = or(m_a_b_wwc, m_a_c_wwc)"))
 
     // a random value should be declared for the data written on a write-write conflict
-    assert(result.contains("rand m_a_wwc_data : UInt<32>, m.a.clk when m_a_wwc_active"))
-    assert(result.contains("rand m_b_wwc_data : UInt<32>, m.b.clk when m_b_c_wwc"))
+    assert(result.contains("rand m_a_wwc_data : UInt<32>, m_a_clk when m_a_wwc_active"))
+    assert(result.contains("rand m_b_wwc_data : UInt<32>, m_b_clk when m_b_c_wwc"))
 
     // a write-write conflict occurs when both ports are enabled and the addresses match
     Seq(("a", "b"), ("a", "c"), ("b", "c")).foreach {
       case (w1, w2) =>
         assert(
-          result.contains(s"m_${w1}_${w2}_wwc <= and(and(m_${w1}_en, m_${w2}_en), eq(m.${w1}.addr, m.${w2}.addr))")
+          result.contains(s"m_${w1}_${w2}_wwc <= and(and(m_${w1}_en, m_${w2}_en), eq(m_${w1}_addr, m_${w2}_addr))")
         )
     }
 
@@ -67,7 +67,7 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     val result = circuit.serialize.split('\n').map(_.trim)
 
     // we should not compute the conflict between a and c since it is impossible
-    assert(!result.contains("node m_a_c_wwc = and(and(m_a_en, m_c_en), eq(m.a.addr, m.c.addr))"))
+    assert(!result.contains("node m_a_c_wwc = and(and(m_a_en, m_c_en), eq(m_a_addr, m_c_addr))"))
 
     // the enable of port b depends on whether there is a conflict with a
     assert(result.contains("m.b.en <= and(m_b_en, not(m_a_b_wwc))"))
@@ -91,7 +91,7 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
 
     assert(
       result.contains(
-        """assert(m.a.clk, or(not(and(m.a.en, m.a.mask)), geq(UInt<5>("h1e"), m.a.addr)), UInt<1>("h1"), "out of bounds read")"""
+        """assert(m_a_clk, geq(UInt<5>("h1e"), m_a_addr), UInt<1>("h1"), "out of bounds read")"""
       )
     )
   }
@@ -102,10 +102,10 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     val result = circuit.serialize.split('\n').map(_.trim)
 
     // an out of bounds read happens if the depth is not greater or equal to the address
-    assert(result.contains("node m_r_oob = not(geq(UInt<5>(\"h1e\"), m.r.addr))"))
+    assert(result.contains("node m_r_oob = not(geq(UInt<5>(\"h1e\"), m_r_addr))"))
 
     // the source of randomness needs to be triggered when there is an out of bounds read
-    assert(result.contains("rand m_r_rand_data : UInt<32>, m.r.clk when m_r_oob"))
+    assert(result.contains("rand m_r_rand_data : UInt<32>, m_r_clk when m_r_oob"))
 
     // the data is random when there is an oob
     assert(result.contains("m_r_data <= mux(m_r_oob, m_r_rand_data, m.r.data)"))
@@ -118,10 +118,10 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     val result = circuit.serialize.split('\n').map(_.trim)
 
     // the memory is disabled when it is not enabled
-    assert(result.contains("node m_r_disabled = not(m.r.en)"))
+    assert(result.contains("node m_r_disabled = not(m_r_en)"))
 
     // the source of randomness needs to be triggered when there is an read while the port is disabled
-    assert(result.contains("rand m_r_rand_data : UInt<32>, m.r.clk when m_r_disabled"))
+    assert(result.contains("rand m_r_rand_data : UInt<32>, m_r_clk when m_r_disabled"))
 
     // the data is random when there is an un-enabled read
     assert(result.contains("m_r_data <= mux(m_r_disabled, m_r_rand_data, m.r.data)"))
@@ -134,16 +134,16 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     val result = circuit.serialize.split('\n').map(_.trim)
 
     // the memory is disabled when it is not enabled
-    assert(result.contains("node m_r_disabled = not(m.r.en)"))
+    assert(result.contains("node m_r_disabled = not(m_r_en)"))
 
     // an out of bounds read happens if the depth is not greater or equal to the address and the memory is enabled
-    assert(result.contains("node m_r_oob = and(m.r.en, not(geq(UInt<5>(\"h1e\"), m.r.addr)))"))
+    assert(result.contains("node m_r_oob = and(m_r_en, not(geq(UInt<5>(\"h1e\"), m_r_addr)))"))
 
     // the two possible issues are combined into a single signal
     assert(result.contains("node m_r_do_rand = or(m_r_disabled, m_r_oob)"))
 
     // the source of randomness needs to be triggered when either issue occurs
-    assert(result.contains("rand m_r_rand_data : UInt<32>, m.r.clk when m_r_do_rand"))
+    assert(result.contains("rand m_r_rand_data : UInt<32>, m_r_clk when m_r_do_rand"))
 
     // the data is random when either issue occurs
     assert(result.contains("m_r_data <= mux(m_r_do_rand, m_r_rand_data, m.r.data)"))
@@ -159,7 +159,7 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     assert(result.contains("m_r_do_rand_r1 <= m_r_do_rand"))
 
     // the source of randomness needs to be triggered by the pipeline register
-    assert(result.contains("rand m_r_rand_data : UInt<32>, m.r.clk when m_r_do_rand_r1"))
+    assert(result.contains("rand m_r_rand_data : UInt<32>, m_r_clk when m_r_do_rand_r1"))
 
     // the data is random when the pipeline register is 1
     assert(result.contains("m_r_data <= mux(m_r_do_rand_r1, m_r_rand_data, m.r.data)"))
@@ -171,13 +171,13 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     val result = circuit.serialize.split('\n').map(_.trim)
 
     // detect read/write conflicts
-    assert(result.contains("m_r_a_rwc <= and(and(m.r.en, and(m.a.en, m.a.mask)), eq(m.r.addr, m.a.addr))"))
+    assert(result.contains("m_r_a_rwc <= eq(m_r_addr, m_a_addr)"))
 
     // delay the signal
     assert(result.contains("m_r_do_rand_r1 <= m_r_rwc"))
 
     // randomize the data
-    assert(result.contains("rand m_r_rand_data : UInt<32>, m.r.clk when m_r_do_rand_r1"))
+    assert(result.contains("rand m_r_rand_data : UInt<32>, m_r_clk when m_r_do_rand_r1"))
     assert(result.contains("m_r_data <= mux(m_r_do_rand_r1, m_r_rand_data, m.r.data)"))
   }
 }