[LTL] Fold disable into assert intrinsic (#4236)

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

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.

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)
 }

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 {

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""") {