Add warnings for upcoming migration to Disable for simulation constructs

core/src/main/scala-2/chisel3/PrintfMacros.scala

@@ -8,6 +8,7 @@ import chisel3.experimental.SourceInfo
 import chisel3.{layer, layers}
 import scala.language.experimental.macros
 import scala.reflect.macros.blackbox
+import chisel3.VerifStmtMacrosCompat.resetToDisableMigrationChecks
 
 object PrintfMacrosCompat {
   def _applyMacroWithInterpolatorCheck(
@@ -77,6 +78,7 @@ object PrintfMacrosCompat {
     Printable.checkScope(pable)
 
     layer.block(layers.Verification, skipIfAlreadyInBlock = true, skipIfLayersEnabled = true) {
+      resetToDisableMigrationChecks("printf")
       pushCommand(chisel3.internal.firrtl.ir.Printf(printfId, sourceInfo, clock.ref, pable))
     }
     printfId

core/src/main/scala-2/chisel3/VerificationStatementMacros.scala

@@ -10,6 +10,8 @@ import chisel3.layers
 import chisel3.util.circt.IfElseFatalIntrinsic
 import chisel3.internal.Builder.pushCommand
 import chisel3.internal._
+import chisel3.ltl._
+import chisel3.ltl.Sequence.BoolSequence
 
 import scala.language.experimental.macros
 import scala.reflect.macros.blackbox
@@ -42,6 +44,18 @@ object VerifStmtMacrosCompat {
     (p.source.file.name, p.line): @nowarn // suppress, there's no clear replacement
   }
 
+  private[chisel3] def resetToDisableMigrationChecks(label: String)(implicit sourceInfo: SourceInfo) =
+    if (Builder.emitVerifStatementDisableProperties) {
+      val disable = Module.disable.value
+      withDisable(Disable.Never) {
+        AssertProperty(
+          prop = ltl.Property.eventually(!disable),
+          label = Some(s"${label}_never_enabled")
+        )
+        CoverProperty(!disable, s"${label}_enabled")
+      }
+    }
+
   object assert {
 
     /** @group VerifPrintMacros */
@@ -117,6 +131,7 @@ object VerifStmtMacrosCompat {
     ): chisel3.assert.Assert = {
       block(layers.Verification.Assert, skipIfAlreadyInBlock = true, skipIfLayersEnabled = true) {
         val id = Builder.forcedUserModule // It should be safe since we push commands anyway.
+        resetToDisableMigrationChecks("assertion")
         IfElseFatalIntrinsic(id, format, "chisel3_builtin", clock, predicate, enable, format.unpackArgs: _*)(sourceInfo)
       }
       new chisel3.assert.Assert()
@@ -186,6 +201,7 @@ object VerifStmtMacrosCompat {
       val id = new chisel3.assume.Assume()
       block(layers.Verification.Assume, skipIfAlreadyInBlock = true, skipIfLayersEnabled = true) {
         message.foreach(Printable.checkScope(_))
+        resetToDisableMigrationChecks("assumption")
         when(!Module.reset.asBool) {
           val formattedMsg = formatFailureMessage("Assumption", line, cond, message)
           Builder.pushCommand(Verification(id, Formal.Assume, sourceInfo, Module.clock.ref, cond.ref, formattedMsg))
@@ -230,6 +246,7 @@ object VerifStmtMacrosCompat {
     ): chisel3.cover.Cover = {
       val id = new chisel3.cover.Cover()
       block(layers.Verification.Cover, skipIfAlreadyInBlock = true, skipIfLayersEnabled = true) {
+        resetToDisableMigrationChecks("cover")
         when(!Module.reset.asBool) {
           Builder.pushCommand(Verification(id, Formal.Cover, sourceInfo, Module.clock.ref, cond.ref, ""))
         }

core/src/main/scala/chisel3/experimental/hierarchy/core/Definition.scala

@@ -112,6 +112,7 @@ object Definition extends SourceInfoDoc {
         context.useLegacyWidth,
         context.includeUtilMetadata,
         context.useSRAMBlackbox,
+        context.emitVerifStatementDisableProperties,
         context.warningFilters,
         context.sourceRoots,
         Some(context.globalNamespace),

core/src/main/scala/chisel3/internal/Builder.scala

@@ -477,14 +477,15 @@ private[chisel3] class ChiselContext() {
 }
 
 private[chisel3] class DynamicContext(
-  val annotationSeq:       AnnotationSeq,
-  val throwOnFirstError:   Boolean,
-  val useLegacyWidth:      Boolean,
-  val includeUtilMetadata: Boolean,
-  val useSRAMBlackbox:     Boolean,
-  val warningFilters:      Seq[WarningFilter],
-  val sourceRoots:         Seq[File],
-  val defaultNamespace:    Option[Namespace],
+  val annotationSeq:                       AnnotationSeq,
+  val throwOnFirstError:                   Boolean,
+  val useLegacyWidth:                      Boolean,
+  val includeUtilMetadata:                 Boolean,
+  val useSRAMBlackbox:                     Boolean,
+  val emitVerifStatementDisableProperties: Boolean,
+  val warningFilters:                      Seq[WarningFilter],
+  val sourceRoots:                         Seq[File],
+  val defaultNamespace:                    Option[Namespace],
   // Definitions from other scopes in the same elaboration, use allDefinitions below
   val loggerOptions: LoggerOptions,
   val definitions:   ArrayBuffer[Definition[_]],
@@ -978,6 +979,9 @@ private[chisel3] object Builder extends LazyLogging {
 
   def useSRAMBlackbox: Boolean = dynamicContextVar.value.map(_.useSRAMBlackbox).getOrElse(false)
 
+  def emitVerifStatementDisableProperties: Boolean =
+    dynamicContextVar.value.map(_.emitVerifStatementDisableProperties).getOrElse(false)
+
   // Builds a RenameMap for all Views that do not correspond to a single Data
   // These Data give a fake ReferenceTarget for .toTarget and .toReferenceTarget that the returned
   // RenameMap can split into the constituent parts

src/main/scala-2/chisel3/ltl/LTL.scala → core/src/main/scala/chisel3/ltl/LTL.scala

@@ -6,7 +6,7 @@ import chisel3._
 import chisel3.layer.{block, Layer}
 import chisel3.util.circt._
 import chisel3.experimental.hierarchy.Instance
-import chisel3.experimental.SourceInfo
+import chisel3.experimental.{SourceInfo, UnlocatableSourceInfo}
 
 /** An opaque sequence returned by an intrinsic.
   *
@@ -410,7 +410,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
   def apply(
     prop:    => Property,
     clock:   Option[Clock] = Module.clockOption,
-    disable: Option[Disable] = Module.disableOption,
+    disable: Option[Disable] = Module.disableOption(UnlocatableSourceInfo),
     label:   Option[String] = None
   )(
     implicit sourceInfo: SourceInfo

src/main/scala/chisel3/stage/ChiselAnnotations.scala

@@ -518,3 +518,17 @@ case object UseSRAMBlackbox extends NoTargetAnnotation with ChiselOption with Ha
     )
   )
 }
+
+case object EmitVerifStatementDisableProperties
+    extends NoTargetAnnotation
+    with ChiselOption
+    with HasShellOptions
+    with Unserializable {
+  val options = Seq(
+    new ShellOption[Unit](
+      longOption = "emit-verif-statement-disable-properties",
+      toAnnotationSeq = _ => Seq(EmitVerifStatementDisableProperties),
+      helpText = "Emit properties to check that Disable for verification statements is eventually toggled"
+    )
+  )
+}

src/main/scala/chisel3/stage/ChiselOptions.scala

@@ -8,28 +8,30 @@ import chisel3.layer.Layer
 import java.io.File
 
 class ChiselOptions private[stage] (
-  val printFullStackTrace: Boolean = false,
-  val throwOnFirstError:   Boolean = false,
-  val outputFile:          Option[String] = None,
-  val chiselCircuit:       Option[Circuit] = None,
-  val sourceRoots:         Vector[File] = Vector.empty,
-  val warningFilters:      Vector[WarningFilter] = Vector.empty,
-  val useLegacyWidth:      Boolean = false,
-  val layerMap:            Map[Layer, Layer] = Map.empty,
-  val includeUtilMetadata: Boolean = false,
-  val useSRAMBlackbox:     Boolean = false) {
+  val printFullStackTrace:                 Boolean = false,
+  val throwOnFirstError:                   Boolean = false,
+  val outputFile:                          Option[String] = None,
+  val chiselCircuit:                       Option[Circuit] = None,
+  val sourceRoots:                         Vector[File] = Vector.empty,
+  val warningFilters:                      Vector[WarningFilter] = Vector.empty,
+  val useLegacyWidth:                      Boolean = false,
+  val layerMap:                            Map[Layer, Layer] = Map.empty,
+  val includeUtilMetadata:                 Boolean = false,
+  val useSRAMBlackbox:                     Boolean = false,
+  val emitVerifStatementDisableProperties: Boolean = false) {
 
   private[stage] def copy(
-    printFullStackTrace: Boolean = printFullStackTrace,
-    throwOnFirstError:   Boolean = throwOnFirstError,
-    outputFile:          Option[String] = outputFile,
-    chiselCircuit:       Option[Circuit] = chiselCircuit,
-    sourceRoots:         Vector[File] = sourceRoots,
-    warningFilters:      Vector[WarningFilter] = warningFilters,
-    useLegacyWidth:      Boolean = useLegacyWidth,
-    layerMap:            Map[Layer, Layer] = layerMap,
-    includeUtilMetadata: Boolean = includeUtilMetadata,
-    useSRAMBlackbox:     Boolean = useSRAMBlackbox
+    printFullStackTrace:                 Boolean = printFullStackTrace,
+    throwOnFirstError:                   Boolean = throwOnFirstError,
+    outputFile:                          Option[String] = outputFile,
+    chiselCircuit:                       Option[Circuit] = chiselCircuit,
+    sourceRoots:                         Vector[File] = sourceRoots,
+    warningFilters:                      Vector[WarningFilter] = warningFilters,
+    useLegacyWidth:                      Boolean = useLegacyWidth,
+    layerMap:                            Map[Layer, Layer] = layerMap,
+    includeUtilMetadata:                 Boolean = includeUtilMetadata,
+    useSRAMBlackbox:                     Boolean = useSRAMBlackbox,
+    emitVerifStatementDisableProperties: Boolean = emitVerifStatementDisableProperties
   ): ChiselOptions = {
 
     new ChiselOptions(
@@ -42,7 +44,8 @@ class ChiselOptions private[stage] (
       useLegacyWidth = useLegacyWidth,
       layerMap = layerMap,
       includeUtilMetadata = includeUtilMetadata,
-      useSRAMBlackbox = useSRAMBlackbox
+      useSRAMBlackbox = useSRAMBlackbox,
+      emitVerifStatementDisableProperties = emitVerifStatementDisableProperties
     )
 
   }

src/main/scala/chisel3/stage/package.scala

@@ -29,10 +29,11 @@ package object stage {
           case SourceRootAnnotation(s)       => c.copy(sourceRoots = c.sourceRoots :+ s)
           case a: WarningConfigurationAnnotation     => c.copy(warningFilters = c.warningFilters ++ a.filters)
           case a: WarningConfigurationFileAnnotation => c.copy(warningFilters = c.warningFilters ++ a.filters)
-          case UseLegacyWidthBehavior         => c.copy(useLegacyWidth = true)
-          case RemapLayer(oldLayer, newLayer) => c.copy(layerMap = c.layerMap + ((oldLayer, newLayer)))
-          case IncludeUtilMetadata            => c.copy(includeUtilMetadata = true)
-          case UseSRAMBlackbox                => c.copy(useSRAMBlackbox = true)
+          case UseLegacyWidthBehavior              => c.copy(useLegacyWidth = true)
+          case RemapLayer(oldLayer, newLayer)      => c.copy(layerMap = c.layerMap + ((oldLayer, newLayer)))
+          case IncludeUtilMetadata                 => c.copy(includeUtilMetadata = true)
+          case UseSRAMBlackbox                     => c.copy(useSRAMBlackbox = true)
+          case EmitVerifStatementDisableProperties => c.copy(emitVerifStatementDisableProperties = true)
         }
       }
 

src/main/scala/chisel3/stage/phases/Elaborate.scala

@@ -45,6 +45,7 @@ class Elaborate extends Phase {
             chiselOptions.useLegacyWidth,
             chiselOptions.includeUtilMetadata,
             chiselOptions.useSRAMBlackbox,
+            chiselOptions.emitVerifStatementDisableProperties,
             chiselOptions.warningFilters,
             chiselOptions.sourceRoots,
             None,

src/main/scala/circt/stage/Shell.scala

@@ -6,6 +6,7 @@ import chisel3.stage.{
   ChiselCircuitAnnotation,
   ChiselGeneratorAnnotation,
   CircuitSerializationAnnotation,
+  EmitVerifStatementDisableProperties,
   PrintFullStackTraceAnnotation,
   RemapLayer,
   SourceRootAnnotation,
@@ -44,7 +45,8 @@ trait CLI extends BareShell { this: BareShell =>
     WarningConfigurationFileAnnotation,
     SourceRootAnnotation,
     DumpFir,
-    RemapLayer
+    RemapLayer,
+    EmitVerifStatementDisableProperties
   ).foreach(_.addOptions(parser))
 
   parser.note("CIRCT (MLIR FIRRTL Compiler) options")

src/test/scala/chiselTests/VerificationSpec.scala

@@ -21,7 +21,7 @@ class SimpleTest extends Module {
   }
 }
 
-class VerificationSpec extends ChiselPropSpec with Matchers {
+class VerificationSpec extends ChiselPropSpec with FileCheck with Matchers {
 
   def assertContains(s: Seq[String], x: String): Unit = {
     val containsLine = s.map(_.contains(x)).reduce(_ || _)
@@ -74,4 +74,32 @@ class VerificationSpec extends ChiselPropSpec with Matchers {
     exactly(1, svLines) should include("assume(io_in != 8'h2)")
     exactly(1, svLines) should include("$error(\"Assumption failed")
   }
+
+  property("verification statements should check that Disable toggles") {
+    class DisableChecksTest extends Module {
+      val io = IO(new Bundle {
+        val in = Input(UInt(8.W))
+        val out = Output(UInt(8.W))
+      })
+      io.out := io.in
+      val assert = chisel3.assert(io.out === io.in)
+      printf(cf"io: ${io.in}")
+    }
+
+    val fir = ChiselStage.emitCHIRRTL(
+      new DisableChecksTest,
+      args = Array("--emit-verif-statement-disable-properties")
+    )
+    fileCheckString(fir)(
+      """
+      CHECK: node assert_disable =
+      CHECK: node [[NOT_DISABLE:[a-zA-Z0-9_]+]] = eq(assert_disable, UInt<1>(0h0))
+      CHECK: node assert_ltl_eventually = intrinsic(circt_ltl_eventually : UInt<1>, [[NOT_DISABLE]])
+
+      CHECK: node disable =
+      CHECK: node [[NOT_DISABLE_1:[a-zA-Z0-9_]+]] = eq(disable, UInt<1>(0h0))
+      CHECK: node ltl_eventually = intrinsic(circt_ltl_eventually : UInt<1>, [[NOT_DISABLE_1]])
+      """
+    )
+  }
 }