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 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/main')

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