From 5569c72c1b6246efd203e00f7af6041567575eec Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Mon, 17 Jan 2022 15:29:14 -0800
Subject: [smt] correct comparison for out-of-bounds memory access check
 (#2463)

This fixes an off by one error, where 3 was erroneously
accepted as in-bounds for a memory of depth=3---
 .../experimental/smt/random/UndefinedMemoryBehaviorPass.scala       | 4 ++--
 .../experimental/smt/random/UndefinedMemoryBehaviorSpec.scala       | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/main/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorPass.scala b/src/main/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorPass.scala
index 5fd0e680..96582778 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorPass.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorPass.scala
@@ -414,8 +414,8 @@ private class InstrumentMems(
 
   private def isInBounds(depth: BigInt, addr: Expression): Expression = {
     val width = getWidth(addr)
-    // depth >= addr
-    DoPrim(PrimOps.Geq, List(UIntLiteral(depth, width), addr), List(), BoolType)
+    // depth > addr (e.g. if the depth is 3, then the address must be in {0, 1, 2})
+    DoPrim(PrimOps.Gt, List(UIntLiteral(depth, width), addr), List(), BoolType)
   }
 
   private def isPow2(v: BigInt): Boolean = ((v - 1) & v) == 0
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 f8f889ac..3cc4f831 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorSpec.scala
@@ -91,7 +91,7 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
 
     assert(
       result.contains(
-        """assert(m_a_clk, geq(UInt<5>("h1e"), m_a_addr), UInt<1>("h1"), "out of bounds read")"""
+        """assert(m_a_clk, gt(UInt<5>("h1e"), m_a_addr), UInt<1>("h1"), "out of bounds read")"""
       )
     )
   }
@@ -102,7 +102,7 @@ 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(gt(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"))
@@ -137,7 +137,7 @@ class UndefinedMemoryBehaviorSpec extends LeanTransformSpec(Seq(Dependency(Undef
     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(gt(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)"))
-- 
cgit v1.2.3