verification: guard statements with module reset

chipsalliance · Apr 29, 2021 · ef13ffe · ef13ffe
1 parent 992a0a6
commit ef13ffe
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 11 deletions.
diff --git a/core/src/main/scala/chisel3/experimental/verification/package.scala b/core/src/main/scala/chisel3/experimental/verification/package.scala
@@ -2,7 +2,7 @@
 
 package chisel3.experimental
 
-import chisel3.{Bool, CompileOptions}
+import chisel3.{Bool, CompileOptions, Module, when}
 import chisel3.internal.Builder
 import chisel3.internal.Builder.pushCommand
 import chisel3.internal.firrtl.{Formal, Verification}
@@ -13,19 +13,21 @@ package object verification {
     def apply(predicate: Bool, msg: String = "")(
       implicit sourceInfo: SourceInfo,
       compileOptions: CompileOptions): Unit = {
-      val clock = Builder.forcedClock
-      pushCommand(Verification(Formal.Assert, sourceInfo, clock.ref,
-        predicate.ref, msg))
+      when (!Module.reset.asBool) {
+        val clock = Builder.forcedClock
+        pushCommand(Verification(Formal.Assert, sourceInfo, clock.ref, predicate.ref, msg))
+      }
     }
   }
 
   object assume {
     def apply(predicate: Bool, msg: String = "")(
       implicit sourceInfo: SourceInfo,
       compileOptions: CompileOptions): Unit = {
-      val clock = Builder.forcedClock
-      pushCommand(Verification(Formal.Assume, sourceInfo, clock.ref,
-        predicate.ref, msg))
+      when (!Module.reset.asBool) {
+        val clock = Builder.forcedClock
+        pushCommand(Verification(Formal.Assume, sourceInfo, clock.ref, predicate.ref, msg))
+      }
     }
   }
 
@@ -34,8 +36,9 @@ package object verification {
       implicit sourceInfo: SourceInfo,
       compileOptions: CompileOptions): Unit = {
       val clock = Builder.forcedClock
-      pushCommand(Verification(Formal.Cover, sourceInfo, clock.ref,
-        predicate.ref, msg))
+      when (!Module.reset.asBool) {
+        pushCommand(Verification(Formal.Cover, sourceInfo, clock.ref, predicate.ref, msg))
+      }
     }
   }
 }
diff --git a/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala b/src/test/scala/chiselTests/experimental/verification/VerificationSpec.scala
@@ -30,8 +30,15 @@ class VerificationSpec extends ChiselPropSpec {
   property("basic equality check should work") {
     val fir = ChiselStage.emitChirrtl(new VerificationModule)
     val lines = fir.split("\n").map(_.trim)
+
+    // reset guard around the verification statement
+    assertContains(lines, "when _T_2 : @[VerificationSpec.scala 16:15]")
     assertContains(lines, "cover(clock, _T, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 16:15]")
-    assertContains(lines, "assume(clock, _T_2, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]")
-    assertContains(lines, "assert(clock, _T_3, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]")
+
+    assertContains(lines, "when _T_6 : @[VerificationSpec.scala 18:18]")
+    assertContains(lines, "assume(clock, _T_4, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 18:18]")
+
+    assertContains(lines, "when _T_9 : @[VerificationSpec.scala 19:18]")
+    assertContains(lines, "assert(clock, _T_7, UInt<1>(\"h1\"), \"\") @[VerificationSpec.scala 19:18]")
   }
 }