From cc782e965945176a8572b25c9d518eff79de8528 Mon Sep 17 00:00:00 2001 From: Amelia Dobis Date: Tue, 2 Jul 2024 13:23:18 -0700 Subject: [PATCH] [LTL] Fold disable into assert intrinsic (#4236) --- core/src/main/scala/chisel3/Aggregate.scala | 18 ++++----- src/main/scala/chisel3/ltl/LTL.scala | 7 ++-- .../chisel3/util/circt/LTLIntrinsics.scala | 26 +++++++------ src/test/scala/chiselTests/LTLSpec.scala | 33 +++++----------- .../circtTests/stage/ChiselStageSpec.scala | 38 +++++++++---------- 5 files changed, 52 insertions(+), 70 deletions(-) diff --git a/core/src/main/scala/chisel3/Aggregate.scala b/core/src/main/scala/chisel3/Aggregate.scala index beb02fa75c3..904b027c1df 100644 --- a/core/src/main/scala/chisel3/Aggregate.scala +++ b/core/src/main/scala/chisel3/Aggregate.scala @@ -242,10 +242,8 @@ sealed class Vec[T <: Data] private[chisel3] (gen: => T, val length: Int) extend val resolvedDirection = SpecifiedDirection.fromParent(parentDirection, specifiedDirection) sample_element.bind(SampleElementBinding(this), resolvedDirection) - // Share same object for binding of all children. - val childBinding = ChildBinding(this) for (child <- elementsIterator) { // assume that all children are the same - child.bind(childBinding, resolvedDirection) + child.bind(ChildBinding(this), resolvedDirection) } // Since all children are the same, we can just use the sample_element rather than all children @@ -1072,20 +1070,18 @@ abstract class Record extends Aggregate { checkForAndReportDuplicates() - // Share same object for binding of all children. - val childBinding = ChildBinding(this) + // This check is for making sure that elements always returns the + // same object, which will not be the case if the user makes it a + // def inside the Record. Checking elementsIterator against itself + // is not useful for this check because it's a lazy val which will + // always return the same thing. for (((_, child), sameChild) <- this.elements.iterator.zip(this.elementsIterator)) { - // This check is for making sure that elements always returns the - // same object, which will not be the case if the user makes it a - // def inside the Record. Checking elementsIterator against itself - // is not useful for this check because it's a lazy val which will - // always return the same thing. if (child != sameChild) { throwException( s"${this.className} does not return the same objects when calling .elements multiple times. Did you make it a def by mistake?" ) } - child.bind(childBinding, resolvedDirection) + child.bind(ChildBinding(this), resolvedDirection) // Update the flipped tracker based on the flipped-ness of this specific child element _containsAFlipped |= child.containsAFlipped diff --git a/src/main/scala/chisel3/ltl/LTL.scala b/src/main/scala/chisel3/ltl/LTL.scala index 1193578634f..b11f62cadff 100644 --- a/src/main/scala/chisel3/ltl/LTL.scala +++ b/src/main/scala/chisel3/ltl/LTL.scala @@ -426,9 +426,8 @@ sealed abstract class AssertPropertyLike { )( implicit sourceInfo: SourceInfo ): Unit = { - val disabled = disable.fold(prop)(prop.disable(_)) - val clocked = clock.fold(disabled)(disabled.clock(_)) - createIntrinsic(label)(sourceInfo)(clocked.inner) + val clocked = clock.fold(prop)(prop.clock(_)) + createIntrinsic(label)(sourceInfo)(clocked.inner, disable.map(!_.value)) } /** Assert, assume, or cover that a boolean predicate holds. @@ -486,7 +485,7 @@ sealed abstract class AssertPropertyLike { apply(Sequence.BoolSequence(cond), Some(clock), Some(disable), Some(label)) } - protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo): (Bool) => Unit + protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo): (Bool, Option[Bool]) => Unit } /** Assert that a property holds. diff --git a/src/main/scala/chisel3/util/circt/LTLIntrinsics.scala b/src/main/scala/chisel3/util/circt/LTLIntrinsics.scala index 3c7b3964a36..30341f60272 100644 --- a/src/main/scala/chisel3/util/circt/LTLIntrinsics.scala +++ b/src/main/scala/chisel3/util/circt/LTLIntrinsics.scala @@ -145,29 +145,33 @@ private[chisel3] object LTLDisableIntrinsic { /** Base class for assert, assume, and cover intrinsics. */ private[chisel3] object VerifAssertLikeIntrinsic { - def apply(intrinsicName: String, label: Option[String])(prop: Bool)(implicit sourceInfo: SourceInfo): Unit = { + def apply( + intrinsicName: String, + label: Option[String] + )(prop: Bool, + enable: Option[Bool] + )( + implicit sourceInfo: SourceInfo + ): Unit = { val name = f"circt_verif_$intrinsicName" - if (label.isEmpty) - Intrinsic(name)(prop) - else - Intrinsic(name, "label" -> label.get)(prop) + Intrinsic(name, (label.map("label" -> StringParam(_)).toSeq): _*)((Seq(prop) ++ enable.toSeq): _*) } } /** A wrapper intrinsic for the CIRCT `verif.assert` operation. */ private[chisel3] object VerifAssertIntrinsic { - def apply(label: Option[String] = None)(prop: Bool)(implicit sourceInfo: SourceInfo) = - VerifAssertLikeIntrinsic("assert", label)(prop) + def apply(label: Option[String] = None)(prop: Bool, enable: Option[Bool])(implicit sourceInfo: SourceInfo) = + VerifAssertLikeIntrinsic("assert", label)(prop, enable) } /** A wrapper intrinsic for the CIRCT `verif.assume` operation. */ private[chisel3] object VerifAssumeIntrinsic { - def apply(label: Option[String] = None)(prop: Bool)(implicit sourceInfo: SourceInfo) = - VerifAssertLikeIntrinsic("assume", label)(prop) + def apply(label: Option[String] = None)(prop: Bool, enable: Option[Bool])(implicit sourceInfo: SourceInfo) = + VerifAssertLikeIntrinsic("assume", label)(prop, enable) } /** A wrapper intrinsic for the CIRCT `verif.cover` operation. */ private[chisel3] object VerifCoverIntrinsic { - def apply(label: Option[String] = None)(prop: Bool)(implicit sourceInfo: SourceInfo) = - VerifAssertLikeIntrinsic("cover", label)(prop) + def apply(label: Option[String] = None)(prop: Bool, enable: Option[Bool])(implicit sourceInfo: SourceInfo) = + VerifAssertLikeIntrinsic("cover", label)(prop, enable) } diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala index 42e008aed47..df08fd2db82 100644 --- a/src/test/scala/chiselTests/LTLSpec.scala +++ b/src/test/scala/chiselTests/LTLSpec.scala @@ -227,20 +227,6 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { ChiselStage.emitSystemVerilog(new EventuallyMod) } - class DisableMod extends RawModule { - val a, b = IO(Input(Bool())) - implicit val info = SourceLine("Foo.scala", 1, 2) - val p0: Property = a.disable(b.asDisable) - } - it should "support property disable operation" in { - val chirrtl = ChiselStage.emitCHIRRTL(new DisableMod) - val sourceLoc = "@[Foo.scala 1:2]" - chirrtl should include(f"intrinsic(circt_ltl_disable : UInt<1>, a, b) $sourceLoc") - } - it should "compile property disable operation" in { - ChiselStage.emitSystemVerilog(new DisableMod) - } - class BasicVerifMod extends RawModule { val a = IO(Input(Bool())) implicit val info = SourceLine("Foo.scala", 1, 2) @@ -276,9 +262,9 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { val sourceLoc = "@[Foo.scala 1:2]" chirrtl should include("node has_been_reset = intrinsic(circt_has_been_reset : UInt<1>, clock, reset)") chirrtl should include("node disable = eq(has_been_reset, UInt<1>(0h0))") - chirrtl should include(f"node disable_1 = intrinsic(circt_ltl_disable : UInt<1>, a, disable) $sourceLoc") - chirrtl should include(f"node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, disable_1, clock) $sourceLoc") - chirrtl should include(f"intrinsic(circt_verif_$op, clock_1) $sourceLoc") + chirrtl should include(f"node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, a, clock) $sourceLoc") + chirrtl should include(f"node _T = eq(disable, UInt<1>(0h0)) $sourceLoc") + chirrtl should include(f"intrinsic(circt_verif_$op, clock_1, _T) $sourceLoc") } } @@ -306,19 +292,18 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners { AssertProperty(a, disable = Some(b.asDisable)) AssertProperty(a, clock = Some(c), disable = Some(b.asDisable)) }) - // with clock; emitted as `assert(clock(a, c))` chirrtl should include("node clock = intrinsic(circt_ltl_clock : UInt<1>, a, c)") chirrtl should include("intrinsic(circt_verif_assert, clock)") - // with disable; emitted as `assert(disable(a, b))` - chirrtl should include("node disable = intrinsic(circt_ltl_disable : UInt<1>, a, b)") - chirrtl should include("intrinsic(circt_verif_assert, disable)") + // with disable; emitted as `assert(a, disable)` + chirrtl should include("node _T = eq(b, UInt<1>(0h0))") + chirrtl should include("intrinsic(circt_verif_assert, a, _T)") // with clock and disable; emitted as `assert(clock(disable(a, b), c))` - chirrtl should include("node disable_1 = intrinsic(circt_ltl_disable : UInt<1>, a, b)") - chirrtl should include("node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, disable_1, c)") - chirrtl should include("intrinsic(circt_verif_assert, clock_1)") + chirrtl should include("node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, a, c)") + chirrtl should include("node _T_1 = eq(b, UInt<1>(0h0))") + chirrtl should include("intrinsic(circt_verif_assert, clock_1, _T_1)") } class SequenceConvMod extends RawModule { diff --git a/src/test/scala/circtTests/stage/ChiselStageSpec.scala b/src/test/scala/circtTests/stage/ChiselStageSpec.scala index eb937f5126f..9e60b442dab 100644 --- a/src/test/scala/circtTests/stage/ChiselStageSpec.scala +++ b/src/test/scala/circtTests/stage/ChiselStageSpec.scala @@ -1164,29 +1164,27 @@ class ChiselStageSpec extends AnyFunSpec with Matchers with chiselTests.Utils { |2 input 1 reset |3 sort bitvec 32 |4 state 3 count - |5 constd 1 0 - |6 state 1 hbr - |7 init 1 6 5 + |5 state 1 hbr + |6 constd 1 0 + |7 init 1 5 6 |8 constd 3 43 |9 constd 3 1 |10 constd 3 42 - |11 constd 1 -1 - |12 constd 3 0 - |13 eq 1 4 10 - |14 add 3 4 9 - |15 ite 3 13 12 14 - |16 ult 1 4 8 - |17 constd 1 -1 - |18 or 1 2 6 - |19 xor 1 2 17 - |20 and 1 6 19 - |21 xor 1 20 11 - |22 or 1 21 16 - |23 not 1 22 - |24 bad 23 - |25 ite 3 2 12 15 - |26 next 3 4 25 - |28 next 1 6 27""".stripMargin) + |11 constd 3 0 + |12 eq 1 4 10 + |13 add 3 4 9 + |14 ite 3 12 11 13 + |15 ult 1 4 8 + |16 constd 1 -1 + |17 or 1 2 5 + |18 xor 1 2 16 + |19 and 1 5 18 + |20 implies 1 19 15 + |21 not 1 20 + |22 bad 21 + |23 ite 3 2 11 14 + |24 next 3 4 23 + |25 next 1 5 17""".stripMargin) } it("""should error if give a "--target-directory" option""") {