From 766ddcd80e7aaeccc83b5b604eabd04b2574187c Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Wed, 13 Nov 2024 09:19:34 -0800 Subject: [PATCH 1/4] move LTL to chisel3.core --- .../scala-2 => core/src/main/scala}/chisel3/ltl/LTL.scala | 4 ++-- .../src/main/scala}/chisel3/util/circt/LTLIntrinsics.scala | 0 2 files changed, 2 insertions(+), 2 deletions(-) rename {src/main/scala-2 => core/src/main/scala}/chisel3/ltl/LTL.scala (99%) rename {src/main/scala-2 => core/src/main/scala}/chisel3/util/circt/LTLIntrinsics.scala (100%) diff --git a/src/main/scala-2/chisel3/ltl/LTL.scala b/core/src/main/scala/chisel3/ltl/LTL.scala similarity index 99% rename from src/main/scala-2/chisel3/ltl/LTL.scala rename to core/src/main/scala/chisel3/ltl/LTL.scala index d2546d57c44..ef40dcc79e9 100644 --- a/src/main/scala-2/chisel3/ltl/LTL.scala +++ b/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 diff --git a/src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala b/core/src/main/scala/chisel3/util/circt/LTLIntrinsics.scala similarity index 100% rename from src/main/scala-2/chisel3/util/circt/LTLIntrinsics.scala rename to core/src/main/scala/chisel3/util/circt/LTLIntrinsics.scala From 98db4f1759ae84d11796edd4c4aba133217c583b Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Wed, 13 Nov 2024 09:32:45 -0800 Subject: [PATCH 2/4] add static warning and property for reset->disable migration --- .../chisel3/VerificationStatementMacros.scala | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala b/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala index d32764c0085..2a884a60525 100644 --- a/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala +++ b/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,17 @@ object VerifStmtMacrosCompat { (p.source.file.name, p.line): @nowarn // suppress, there's no clear replacement } + private[chisel3] def resetToDisableMigrationChecks(label: String)(implicit sourceInfo: SourceInfo) = { + 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 +130,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 +200,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 +245,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, "")) } From 68a47bc26da215297069ee4e002643daace5848f Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Wed, 8 Jan 2025 10:24:38 -0800 Subject: [PATCH 3/4] put checks behind an option --- .../chisel3/VerificationStatementMacros.scala | 19 ++++---- .../hierarchy/core/Definition.scala | 1 + .../main/scala/chisel3/internal/Builder.scala | 20 +++++---- .../chisel3/stage/ChiselAnnotations.scala | 14 ++++++ .../scala/chisel3/stage/ChiselOptions.scala | 45 ++++++++++--------- src/main/scala/chisel3/stage/package.scala | 9 ++-- .../chisel3/stage/phases/Elaborate.scala | 1 + 7 files changed, 67 insertions(+), 42 deletions(-) diff --git a/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala b/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala index 2a884a60525..46010aec3b4 100644 --- a/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala +++ b/core/src/main/scala-2/chisel3/VerificationStatementMacros.scala @@ -44,16 +44,17 @@ object VerifStmtMacrosCompat { (p.source.file.name, p.line): @nowarn // suppress, there's no clear replacement } - private[chisel3] def resetToDisableMigrationChecks(label: String)(implicit sourceInfo: SourceInfo) = { - 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") + 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 { diff --git a/core/src/main/scala/chisel3/experimental/hierarchy/core/Definition.scala b/core/src/main/scala/chisel3/experimental/hierarchy/core/Definition.scala index 7f584963877..e2664fd7364 100644 --- a/core/src/main/scala/chisel3/experimental/hierarchy/core/Definition.scala +++ b/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), diff --git a/core/src/main/scala/chisel3/internal/Builder.scala b/core/src/main/scala/chisel3/internal/Builder.scala index 0992b48efd5..3c11d676e70 100644 --- a/core/src/main/scala/chisel3/internal/Builder.scala +++ b/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 diff --git a/src/main/scala/chisel3/stage/ChiselAnnotations.scala b/src/main/scala/chisel3/stage/ChiselAnnotations.scala index 9593311a5b4..4bdb5906905 100644 --- a/src/main/scala/chisel3/stage/ChiselAnnotations.scala +++ b/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" + ) + ) +} diff --git a/src/main/scala/chisel3/stage/ChiselOptions.scala b/src/main/scala/chisel3/stage/ChiselOptions.scala index ebd78656fe5..20e4046c7fa 100644 --- a/src/main/scala/chisel3/stage/ChiselOptions.scala +++ b/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 ) } diff --git a/src/main/scala/chisel3/stage/package.scala b/src/main/scala/chisel3/stage/package.scala index 04045195392..72190a5ce2d 100644 --- a/src/main/scala/chisel3/stage/package.scala +++ b/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) } } diff --git a/src/main/scala/chisel3/stage/phases/Elaborate.scala b/src/main/scala/chisel3/stage/phases/Elaborate.scala index 6e9e1736eff..eddeb80671d 100644 --- a/src/main/scala/chisel3/stage/phases/Elaborate.scala +++ b/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, From b239f487f2d6a81ceb04a96a2ef40e338ffb07e6 Mon Sep 17 00:00:00 2001 From: Trevor McKay Date: Wed, 8 Jan 2025 11:50:26 -0800 Subject: [PATCH 4/4] add tests --- .../main/scala-2/chisel3/PrintfMacros.scala | 2 ++ src/main/scala/circt/stage/Shell.scala | 4 ++- .../scala/chiselTests/VerificationSpec.scala | 30 ++++++++++++++++++- 3 files changed, 34 insertions(+), 2 deletions(-) diff --git a/core/src/main/scala-2/chisel3/PrintfMacros.scala b/core/src/main/scala-2/chisel3/PrintfMacros.scala index 308a49494d9..91b14c9c30f 100644 --- a/core/src/main/scala-2/chisel3/PrintfMacros.scala +++ b/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 diff --git a/src/main/scala/circt/stage/Shell.scala b/src/main/scala/circt/stage/Shell.scala index 712323c728d..6ac0cac67ea 100644 --- a/src/main/scala/circt/stage/Shell.scala +++ b/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") diff --git a/src/test/scala/chiselTests/VerificationSpec.scala b/src/test/scala/chiselTests/VerificationSpec.scala index f5c4d885933..b9e76981e07 100644 --- a/src/test/scala/chiselTests/VerificationSpec.scala +++ b/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]]) + """ + ) + } }