diff options
| author | Kevin Laeufer | 2022-01-17 15:29:14 -0800 |
|---|---|---|
| committer | GitHub | 2022-01-17 23:29:14 +0000 |
| commit | 5569c72c1b6246efd203e00f7af6041567575eec (patch) | |
| tree | 4b3bad805868c96e0e61cb8eee7dbb58eddff2c3 /src/main | |
| parent | afde9c7d6acd0937f5b8df548143ad0083ea8e08 (diff) | |
[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
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/random/UndefinedMemoryBehaviorPass.scala | 4 |
1 files changed, 2 insertions, 2 deletions
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 |