From fdedfc0e56b93316f2d4f019d70d12e746d9bd57 Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Wed, 28 Jan 2026 20:59:15 -0800
Subject: [PATCH 1/9] first go

---
 src/main/scala-2/chisel3/ltl/LTLIntf.scala | 215 +++++++++++++++++++++
 src/main/scala-3/chisel3/ltl/LTLIntf.scala | 212 ++++++++++++++++++++
 src/main/scala/chisel3/ltl/LTL.scala       | 163 +++++++++-------
 3 files changed, 520 insertions(+), 70 deletions(-)
 create mode 100644 src/main/scala-2/chisel3/ltl/LTLIntf.scala
 create mode 100644 src/main/scala-3/chisel3/ltl/LTLIntf.scala

diff --git a/src/main/scala-2/chisel3/ltl/LTLIntf.scala b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
new file mode 100644
index 00000000000..c92ae88d01f
--- /dev/null
+++ b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
@@ -0,0 +1,215 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package chisel3.ltl
+
+import chisel3._
+import chisel3.experimental.SourceInfo
+
+private[chisel3] trait SequenceIntf { self: Sequence =>
+
+  /** See `Sequence.delay`. */
+  def delay(delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = _delayImpl(delay)
+
+  /** See `Sequence.delayRange`. */
+  def delayRange(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = _delayRangeImpl(min, max)
+
+  /** See `Sequence.delayAtLeast`. */
+  def delayAtLeast(delay: Int)(implicit sourceInfo: SourceInfo): Sequence = _delayAtLeastImpl(delay)
+
+  /** See `Sequence.concat`. */
+  def concat(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _concatImpl(other)
+
+  /** See `Sequence.repeat`. */
+  def repeat(n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = _repeatImpl(n)
+
+  /** See `Sequence.repeatRange`. */
+  def repeatRange(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = _repeatRangeImpl(min, max)
+
+  /** See `Sequence.repeatAtLeast`. */
+  def repeatAtLeast(n: Int)(implicit sourceInfo: SourceInfo): Sequence = _repeatAtLeastImpl(n)
+
+  /** See `Sequence.gotoRepeat`. */
+  def gotoRepeat(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = _gotoRepeatImpl(min, max)
+
+  /** See `Sequence.nonConsecutiveRepeat`. */
+  def nonConsecutiveRepeat(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    _nonConsecutiveRepeatImpl(min, max)
+
+  /** See `Sequence.and`. */
+  def and(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _andSeqImpl(other)
+
+  /** See `Sequence.or`. */
+  def or(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _orSeqImpl(other)
+
+  /** See `Sequence.intersect`. */
+  def intersect(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _intersectSeqImpl(other)
+
+  /** See `Sequence.until`. */
+  def until(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _untilSeqImpl(other)
+
+  /** See `Sequence.clock`. */
+  override def clock(clock: Clock)(implicit sourceInfo: SourceInfo): Sequence = _clockImpl(clock)
+
+  /** See `Property.implication`. */
+  def implication(prop: Property)(implicit sourceInfo: SourceInfo): Property = _implicationImpl(prop)
+
+  /** See `Property.implication`. */
+  def implicationNonOverlapping(prop: Property)(implicit sourceInfo: SourceInfo): Property =
+    _implicationNonOverlappingImpl(prop)
+
+  // Convenience operators.
+
+  /** Equivalent to `|->` in SVA. */
+  def |->(prop: Property)(implicit sourceInfo: SourceInfo): Property = _impl_|->(prop)
+
+  /** Equivalent to `|=>` in SVA. */
+  def |=>(prop: Property)(implicit sourceInfo: SourceInfo): Property = _impl_|=>(prop)
+
+  /** Equivalent to `a ##1 b` in SVA. */
+  def ###(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _impl_###(other)
+
+  /** Equivalent to `a ##[*] b` in SVA. */
+  def ##*(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _impl_##*(other)
+
+  /** Equivalent to `a ##[+] b` in SVA. */
+  def ##+(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _impl_##+(other)
+}
+
+private[chisel3] trait PropertyIntf { self: Property =>
+
+  /** See `Property.not`. */
+  def not(implicit sourceInfo: SourceInfo): Property = _notImpl
+
+  /** See `Property.eventually`. */
+  def eventually(implicit sourceInfo: SourceInfo): Property = _eventuallyImpl
+
+  /** See `Property.and`. */
+  def and(other: Property)(implicit sourceInfo: SourceInfo): Property = _andPropImpl(other)
+
+  /** See `Property.or`. */
+  def or(other: Property)(implicit sourceInfo: SourceInfo): Property = _orPropImpl(other)
+
+  /** See `Property.intersect`. */
+  def intersect(other: Property)(implicit sourceInfo: SourceInfo): Property = _intersectPropImpl(other)
+
+  /** See `Property.until`. */
+  def until(other: Property)(implicit sourceInfo: SourceInfo): Property = _untilPropImpl(other)
+
+  /** See `Property.clock`. */
+  def clock(clock: Clock)(implicit sourceInfo: SourceInfo): Property = _clockImpl(clock)
+}
+
+private[chisel3] trait Sequence$Intf { self: Sequence.type =>
+
+  /** Delay a sequence by a fixed number of cycles. */
+  def delay(seq: Sequence, delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = _delay(seq, delay)
+
+  /** Delay a sequence by a bounded range of cycles. */
+  def delayRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    _delayRange(seq, min, max)
+
+  /** Delay a sequence by an unbounded range of cycles. */
+  def delayAtLeast(seq: Sequence, delay: Int)(implicit sourceInfo: SourceInfo): Sequence = _delayAtLeast(seq, delay)
+
+  /** Concatenate multiple sequences. */
+  def concat(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = _concat(arg0, argN: _*)
+
+  /** Repeat a sequence a fixed number of consecutive times. */
+  def repeat(seq: Sequence, n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = _repeat(seq, n)
+
+  /** Repeat a sequence by a bounded range of consecutive times. */
+  def repeatRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    _repeatRange(seq, min, max)
+
+  /** Repeat a sequence by an unbounded range of consecutive times. */
+  def repeatAtLeast(seq: Sequence, n: Int)(implicit sourceInfo: SourceInfo): Sequence = _repeatAtLeast(seq, n)
+
+  /** GoTo-style repitition of a sequence. */
+  def gotoRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    _gotoRepeat(seq, min, max)
+
+  /** Repeat a sequence a fixed number of non-consecutive times. */
+  def nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    _nonConsecutiveRepeat(seq, min, max)
+
+  /** Form the conjunction of two sequences. */
+  def and(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = _and(arg0, argN: _*)
+
+  /** Form the disjunction of two sequences. */
+  def or(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = _or(arg0, argN: _*)
+
+  /** Form the intersection of two sequences. */
+  def intersect(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence =
+    _intersect(arg0, argN: _*)
+
+  /** Check that a sequence holds until another sequence holds. */
+  def until(arg0: Sequence, arg1: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _until(arg0, arg1)
+
+  /** Specify a clock relative to which all cycle delays are specified. */
+  def clock(seq: Sequence, clock: Clock)(implicit sourceInfo: SourceInfo): Sequence = _clock(seq, clock)
+
+  /** Convenience constructor for sequences. */
+  def apply(atoms: SequenceAtom*)(implicit sourceInfo: SourceInfo): Sequence = _apply(atoms: _*)
+}
+
+private[chisel3] trait Property$Intf { self: Property.type =>
+
+  /** Negate a property. */
+  def not(prop: Property)(implicit sourceInfo: SourceInfo): Property = _not(prop)
+
+  /** Precondition the checking of a property on a sequence. */
+  def implication(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property = _implication(seq, prop)
+
+  /** Non-overlapping variant of implication. */
+  def implicationNonOverlapping(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property =
+    _implicationNonOverlapping(seq, prop)
+
+  /** Indicate that a property will eventually hold. */
+  def eventually(prop: Property)(implicit sourceInfo: SourceInfo): Property = _eventually(prop)
+
+  /** Form the conjunction of two properties. */
+  def and(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = _and(arg0, argN: _*)
+
+  /** Form the disjunction of two properties. */
+  def or(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = _or(arg0, argN: _*)
+
+  /** Form the intersection of two properties. */
+  def intersect(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = _intersect(arg0, argN: _*)
+
+  /** Check that a property holds until another property holds. */
+  def until(arg0: Property, arg1: Property)(implicit sourceInfo: SourceInfo): Property = _until(arg0, arg1)
+
+  /** Specify a clock relative to which all cycle delays are specified. */
+  def clock(prop: Property, clock: Clock)(implicit sourceInfo: SourceInfo): Property = _clock(prop, clock)
+}
+
+private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
+
+  def apply(
+    prop:    => Property,
+    clock:   Option[Clock] = Module.clockOption,
+    disable: Option[Disable] = Module.disableOption,
+    label:   Option[String] = None
+  )(
+    implicit sourceInfo: SourceInfo
+  ): Unit = _applyImpl(prop, clock, disable, label)
+
+  def apply(cond: Bool)(implicit sourceInfo: SourceInfo): Unit = _applyCondImpl(cond)
+
+  def apply(cond: Bool, label: String)(implicit sourceInfo: SourceInfo): Unit = _applyCondLabelImpl(cond, label)
+
+  def apply(
+    cond:    Bool,
+    clock:   Clock,
+    disable: Disable,
+    label:   String
+  )(
+    implicit sourceInfo: SourceInfo
+  ): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
+}
+
+private[chisel3] trait AssertProperty$Intf extends AssertPropertyLikeIntf { self: AssertProperty.type => }
+private[chisel3] trait AssumeProperty$Intf extends AssertPropertyLikeIntf { self: AssumeProperty.type => }
+private[chisel3] trait CoverProperty$Intf extends AssertPropertyLikeIntf { self: CoverProperty.type => }
+private[chisel3] trait RequireProperty$Intf extends AssertPropertyLikeIntf { self: RequireProperty.type => }
+private[chisel3] trait EnsureProperty$Intf extends AssertPropertyLikeIntf { self: EnsureProperty.type => }
diff --git a/src/main/scala-3/chisel3/ltl/LTLIntf.scala b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
new file mode 100644
index 00000000000..2923c0d62c7
--- /dev/null
+++ b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
@@ -0,0 +1,212 @@
+// SPDX-License-Identifier: Apache-2.0
+
+package chisel3.ltl
+
+import chisel3._
+import chisel3.experimental.SourceInfo
+
+private[chisel3] trait SequenceIntf { self: Sequence =>
+
+  /** See `Sequence.delay`. */
+  def delay(delay: Int = 1)(using SourceInfo): Sequence = _delayImpl(delay)
+
+  /** See `Sequence.delayRange`. */
+  def delayRange(min: Int, max: Int)(using SourceInfo): Sequence = _delayRangeImpl(min, max)
+
+  /** See `Sequence.delayAtLeast`. */
+  def delayAtLeast(delay: Int)(using SourceInfo): Sequence = _delayAtLeastImpl(delay)
+
+  /** See `Sequence.concat`. */
+  def concat(other: Sequence)(using SourceInfo): Sequence = _concatImpl(other)
+
+  /** See `Sequence.repeat`. */
+  def repeat(n: Int = 1)(using SourceInfo): Sequence = _repeatImpl(n)
+
+  /** See `Sequence.repeatRange`. */
+  def repeatRange(min: Int, max: Int)(using SourceInfo): Sequence = _repeatRangeImpl(min, max)
+
+  /** See `Sequence.repeatAtLeast`. */
+  def repeatAtLeast(n: Int)(using SourceInfo): Sequence = _repeatAtLeastImpl(n)
+
+  /** See `Sequence.gotoRepeat`. */
+  def gotoRepeat(min: Int, max: Int)(using SourceInfo): Sequence = _gotoRepeatImpl(min, max)
+
+  /** See `Sequence.nonConsecutiveRepeat`. */
+  def nonConsecutiveRepeat(min: Int, max: Int)(using SourceInfo): Sequence =
+    _nonConsecutiveRepeatImpl(min, max)
+
+  /** See `Sequence.and`. */
+  def and(other: Sequence)(using SourceInfo): Sequence = _andSeqImpl(other)
+
+  /** See `Sequence.or`. */
+  def or(other: Sequence)(using SourceInfo): Sequence = _orSeqImpl(other)
+
+  /** See `Sequence.intersect`. */
+  def intersect(other: Sequence)(using SourceInfo): Sequence = _intersectSeqImpl(other)
+
+  /** See `Sequence.until`. */
+  def until(other: Sequence)(using SourceInfo): Sequence = _untilSeqImpl(other)
+
+  /** See `Sequence.clock`. */
+  override def clock(clock: Clock)(using SourceInfo): Sequence = _clockImpl(clock)
+
+  /** See `Property.implication`. */
+  def implication(prop: Property)(using SourceInfo): Property = _implicationImpl(prop)
+
+  /** See `Property.implication`. */
+  def implicationNonOverlapping(prop: Property)(using SourceInfo): Property =
+    _implicationNonOverlappingImpl(prop)
+
+  // Convenience operators.
+
+  /** Equivalent to `|->` in SVA. */
+  def |->(prop: Property)(using SourceInfo): Property = _impl_|->(prop)
+
+  /** Equivalent to `|=>` in SVA. */
+  def |=>(prop: Property)(using SourceInfo): Property = _impl_|=>(prop)
+
+  /** Equivalent to `a ##1 b` in SVA. */
+  def ###(other: Sequence)(using SourceInfo): Sequence = _impl_###(other)
+
+  /** Equivalent to `a ##[*] b` in SVA. */
+  def ##*(other: Sequence)(using SourceInfo): Sequence = _impl_##*(other)
+
+  /** Equivalent to `a ##[+] b` in SVA. */
+  def ##+(other: Sequence)(using SourceInfo): Sequence = _impl_##+(other)
+}
+
+private[chisel3] trait PropertyIntf { self: Property =>
+
+  /** See `Property.not`. */
+  def not(using SourceInfo): Property = _notImpl
+
+  /** See `Property.eventually`. */
+  def eventually(using SourceInfo): Property = _eventuallyImpl
+
+  /** See `Property.and`. */
+  def and(other: Property)(using SourceInfo): Property = _andPropImpl(other)
+
+  /** See `Property.or`. */
+  def or(other: Property)(using SourceInfo): Property = _orPropImpl(other)
+
+  /** See `Property.intersect`. */
+  def intersect(other: Property)(using SourceInfo): Property = _intersectPropImpl(other)
+
+  /** See `Property.until`. */
+  def until(other: Property)(using SourceInfo): Property = _untilPropImpl(other)
+
+  /** See `Property.clock`. */
+  def clock(clock: Clock)(using SourceInfo): Property = _clockImpl(clock)
+}
+
+private[chisel3] trait Sequence$Intf { self: Sequence.type =>
+
+  /** Delay a sequence by a fixed number of cycles. */
+  def delay(seq: Sequence, delay: Int = 1)(using SourceInfo): Sequence = _delay(seq, delay)
+
+  /** Delay a sequence by a bounded range of cycles. */
+  def delayRange(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
+    _delayRange(seq, min, max)
+
+  /** Delay a sequence by an unbounded range of cycles. */
+  def delayAtLeast(seq: Sequence, delay: Int)(using SourceInfo): Sequence = _delayAtLeast(seq, delay)
+
+  /** Concatenate multiple sequences. */
+  def concat(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _concat(arg0, argN: _*)
+
+  /** Repeat a sequence a fixed number of consecutive times. */
+  def repeat(seq: Sequence, n: Int = 1)(using SourceInfo): Sequence = _repeat(seq, n)
+
+  /** Repeat a sequence by a bounded range of consecutive times. */
+  def repeatRange(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
+    _repeatRange(seq, min, max)
+
+  /** Repeat a sequence by an unbounded range of consecutive times. */
+  def repeatAtLeast(seq: Sequence, n: Int)(using SourceInfo): Sequence = _repeatAtLeast(seq, n)
+
+  /** GoTo-style repitition of a sequence. */
+  def gotoRepeat(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
+    _gotoRepeat(seq, min, max)
+
+  /** Repeat a sequence a fixed number of non-consecutive times. */
+  def nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
+    _nonConsecutiveRepeat(seq, min, max)
+
+  /** Form the conjunction of two sequences. */
+  def and(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _and(arg0, argN: _*)
+
+  /** Form the disjunction of two sequences. */
+  def or(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _or(arg0, argN: _*)
+
+  /** Form the intersection of two sequences. */
+  def intersect(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence =
+    _intersect(arg0, argN: _*)
+
+  /** Check that a sequence holds until another sequence holds. */
+  def until(arg0: Sequence, arg1: Sequence)(using SourceInfo): Sequence = _until(arg0, arg1)
+
+  /** Specify a clock relative to which all cycle delays are specified. */
+  def clock(seq: Sequence, clock: Clock)(using SourceInfo): Sequence = _clock(seq, clock)
+
+  /** Convenience constructor for sequences. */
+  def apply(atoms: SequenceAtom*)(using SourceInfo): Sequence = _apply(atoms: _*)
+}
+
+private[chisel3] trait Property$Intf { self: Property.type =>
+
+  /** Negate a property. */
+  def not(prop: Property)(using SourceInfo): Property = _not(prop)
+
+  /** Precondition the checking of a property on a sequence. */
+  def implication(seq: Sequence, prop: Property)(using SourceInfo): Property = _implication(seq, prop)
+
+  /** Non-overlapping variant of implication. */
+  def implicationNonOverlapping(seq: Sequence, prop: Property)(using SourceInfo): Property =
+    _implicationNonOverlapping(seq, prop)
+
+  /** Indicate that a property will eventually hold. */
+  def eventually(prop: Property)(using SourceInfo): Property = _eventually(prop)
+
+  /** Form the conjunction of two properties. */
+  def and(arg0: Property, argN: Property*)(using SourceInfo): Property = _and(arg0, argN: _*)
+
+  /** Form the disjunction of two properties. */
+  def or(arg0: Property, argN: Property*)(using SourceInfo): Property = _or(arg0, argN: _*)
+
+  /** Form the intersection of two properties. */
+  def intersect(arg0: Property, argN: Property*)(using SourceInfo): Property = _intersect(arg0, argN: _*)
+
+  /** Check that a property holds until another property holds. */
+  def until(arg0: Property, arg1: Property)(using SourceInfo): Property = _until(arg0, arg1)
+
+  /** Specify a clock relative to which all cycle delays are specified. */
+  def clock(prop: Property, clock: Clock)(using SourceInfo): Property = _clock(prop, clock)
+}
+
+private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
+
+  def apply(
+    prop:    => Property,
+    clock:   Option[Clock] = Module.clockOption,
+    disable: Option[Disable] = Module.disableOption,
+    label:   Option[String] = None
+  )(using SourceInfo): Unit = _applyImpl(prop, clock, disable, label)
+
+  def apply(cond: Bool)(using SourceInfo): Unit = _applyCondImpl(cond)
+
+  def apply(cond: Bool, label: String)(using SourceInfo): Unit = _applyCondLabelImpl(cond, label)
+
+  def apply(
+    cond:    Bool,
+    clock:   Clock,
+    disable: Disable,
+    label:   String
+  )(using SourceInfo): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
+}
+
+private[chisel3] trait AssertProperty$Intf extends AssertPropertyLikeIntf { self: AssertProperty.type => }
+private[chisel3] trait AssumeProperty$Intf extends AssertPropertyLikeIntf { self: AssumeProperty.type => }
+private[chisel3] trait CoverProperty$Intf extends AssertPropertyLikeIntf { self: CoverProperty.type => }
+private[chisel3] trait RequireProperty$Intf extends AssertPropertyLikeIntf { self: RequireProperty.type => }
+private[chisel3] trait EnsureProperty$Intf extends AssertPropertyLikeIntf { self: EnsureProperty.type => }
+
diff --git a/src/main/scala/chisel3/ltl/LTL.scala b/src/main/scala/chisel3/ltl/LTL.scala
index a663ae4d2ee..7f5717e9abb 100644
--- a/src/main/scala/chisel3/ltl/LTL.scala
+++ b/src/main/scala/chisel3/ltl/LTL.scala
@@ -46,74 +46,85 @@ object Delay {
 }
 
 /** A Linear Temporal Logic (LTL) sequence. */
-sealed trait Sequence extends Property {
+sealed trait Sequence extends Property with SequenceIntf {
 
   /** See `Sequence.delay`. */
-  def delay(delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = Sequence.delay(this, delay)
+  protected def _delayImpl(delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = Sequence._delay(this, delay)
 
   /** See `Sequence.delayRange`. */
-  def delayRange(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence.delayRange(this, min, max)
+  protected def _delayRangeImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._delayRange(this, min, max)
 
   /** See `Sequence.delayAtLeast`. */
-  def delayAtLeast(delay: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence.delayAtLeast(this, delay)
+  protected def _delayAtLeastImpl(delay: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._delayAtLeast(this, delay)
 
   /** See `Sequence.concat`. */
-  def concat(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence.concat(this, other)
+  protected def _concatImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence._concat(this, other)
 
   /** See `Sequence.repeat`. */
-  def repeat(n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = Sequence.repeat(this, n)
+  protected def _repeatImpl(n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = Sequence._repeat(this, n)
 
   /** See `Sequence.repeatRange`. */
-  def repeatRange(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence.repeatRange(this, min, max)
+  protected def _repeatRangeImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._repeatRange(this, min, max)
 
   /** See `Sequence.repeatAtLeast`. */
-  def repeatAtLeast(n: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence.repeatAtLeast(this, n)
+  protected def _repeatAtLeastImpl(n: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence._repeatAtLeast(this, n)
 
   /** See `Sequence.gotoRepeat`. */
-  def gotoRepeat(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence.gotoRepeat(this, min, max)
+  protected def _gotoRepeatImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._gotoRepeat(this, min, max)
 
   /** See `Sequence.nonConsecutiveRepeat`. */
-  def nonConsecutiveRepeat(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
-    Sequence.nonConsecutiveRepeat(this, min, max)
+  protected def _nonConsecutiveRepeatImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._nonConsecutiveRepeat(this, min, max)
 
   /** See `Sequence.and`. */
-  def and(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence.and(this, other)
+  protected def _andSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence._and(this, other)
 
   /** See `Sequence.or`. */
-  def or(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence.or(this, other)
+  protected def _orSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence._or(this, other)
 
   /** See `Sequence.intersect`. */
-  def intersect(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence.intersect(this, other)
+  protected def _intersectSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._intersect(this, other)
 
   /** See `Sequence.until`. */
-  def until(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence.until(this, other)
+  protected def _untilSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._until(this, other)
 
   /** See `Sequence.clock`. */
-  override def clock(clock: Clock)(implicit sourceInfo: SourceInfo): Sequence = Sequence.clock(this, clock)
+  override protected def _clockImpl(clock: Clock)(implicit sourceInfo: SourceInfo): Sequence =
+    Sequence._clock(this, clock)
 
   /** See `Property.implication`. */
-  def implication(prop: Property)(implicit sourceInfo: SourceInfo): Property = Property.implication(this, prop)
+  protected def _implicationImpl(prop: Property)(implicit sourceInfo: SourceInfo): Property =
+    Property.implication(this, prop)
 
   /** See `Property.implication`. */
-  def implicationNonOverlapping(prop: Property)(implicit sourceInfo: SourceInfo): Property =
+  protected def _implicationNonOverlappingImpl(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     Property.implicationNonOverlapping(this, prop)
 
   // Convenience operators.
 
   /** Equivalent to `|->` in SVA. */
-  def |->(prop: Property)(implicit sourceInfo: SourceInfo): Property = this.implication(prop)
+  protected def _impl_|->(prop: Property)(implicit sourceInfo: SourceInfo): Property = this.implication(prop)
 
   /** Equivalent to `|=>` in SVA. */
-  def |=>(prop: Property)(implicit sourceInfo: SourceInfo): Property = this.implicationNonOverlapping(prop)
+  protected def _impl_|=>(prop: Property)(implicit sourceInfo: SourceInfo): Property =
+    this.implicationNonOverlapping(prop)
 
   /** Equivalent to `a ##1 b` in SVA. */
-  def ###(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = this.concat(other.delay())
+  protected def _impl_###(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = this.concat(other.delay())
 
   /** Equivalent to `a ##[*] b` in SVA. */
-  def ##*(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = this.concat(other.delayAtLeast(0))
+  protected def _impl_##*(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
+    this.concat(other.delayAtLeast(0))
 
   /** Equivalent to `a ##[+] b` in SVA. */
-  def ##+(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = this.concat(other.delayAtLeast(1))
+  protected def _impl_##+(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
+    this.concat(other.delayAtLeast(1))
 }
 
 /** Prefix-style utilities to work with sequences.
@@ -121,7 +132,7 @@ sealed trait Sequence extends Property {
   * This object exposes the primary API to create and compose sequences from
   * booleans and shorter sequences.
   */
-object Sequence {
+object Sequence extends Sequence$Intf {
 
   /** Implicitly wraps a `Bool` and allows it to be used as a sequence or
     * property. Use via `import chisel3.ltl.Sequence.BoolSequence`.
@@ -131,13 +142,13 @@ object Sequence {
   /** Delay a sequence by a fixed number of cycles. Equivalent to `##delay` in
     * SVA.
     */
-  def delay(seq: Sequence, delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence =
+  protected def _delay(seq: Sequence, delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLDelayIntrinsic(delay, Some(0))(seq.inner))
 
   /** Delay a sequence by a bounded range of cycles. Equivalent to `##[min:max]`
     * in SVA.
     */
-  def delayRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _delayRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(min <= max)
     OpaqueSequence(LTLDelayIntrinsic(min, Some(max - min))(seq.inner))
   }
@@ -145,13 +156,13 @@ object Sequence {
   /** Delay a sequence by an unbounded range of cycles. Equivalent to
     * `##[delay:$]` in SVA.
     */
-  def delayAtLeast(seq: Sequence, delay: Int)(implicit sourceInfo: SourceInfo): Sequence =
+  protected def _delayAtLeast(seq: Sequence, delay: Int)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLDelayIntrinsic(delay, None)(seq.inner))
 
   /** Concatenate multiple sequences. Equivalent to
     * `arg0 ##0 arg1 ##0 ... ##0 argN` in SVA.
     */
-  def concat(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _concat(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueSequence(LTLConcatIntrinsic(lhs.inner, rhs.inner))
@@ -162,7 +173,7 @@ object Sequence {
   /** Repeat a sequence a fixed number of consecutive times. Equivalent to `s[n]` in
     * SVA.
     */
-  def repeat(seq: Sequence, n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _repeat(seq: Sequence, n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 < n)
     OpaqueSequence(LTLRepeatIntrinsic(n, Some(0))(seq.inner))
   }
@@ -170,7 +181,7 @@ object Sequence {
   /** Repeat a sequence by a bounded range of consecutive times. Equivalent to `s[min:max]`
     * in SVA.
     */
-  def repeatRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _repeatRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(min <= max)
     OpaqueSequence(LTLRepeatIntrinsic(min, Some(max - min))(seq.inner))
   }
@@ -178,7 +189,7 @@ object Sequence {
   /** Repeat a sequence by an unbounded range of consecutive times. Equivalent to
     * `s[n:$]` in SVA.
     */
-  def repeatAtLeast(seq: Sequence, n: Int)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _repeatAtLeast(seq: Sequence, n: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 < n)
     OpaqueSequence(LTLRepeatIntrinsic(n, None)(seq.inner))
   }
@@ -188,7 +199,7 @@ object Sequence {
     * a !b b b !b !b b c represents a matching observation of `gotoRepeat(b, 1, 3)`,
     * but a !b b b !b !b b !b c does not. Equivalent to `s[->min:max]` in SVA.
     */
-  def gotoRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _gotoRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 <= min && min <= max)
     OpaqueSequence(LTLGoToRepeatIntrinsic(min, max - min)(seq.inner))
   }
@@ -198,7 +209,7 @@ object Sequence {
     * both a !b b b !b !b b c and a !b b b !b !b b !b c represent matching
     * observations of `nonConsecutiveRepeat(b, 1, 3)`. Equivalent to `s[=min:max]` in SVA.
     */
-  def nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 <= min && min <= max)
     OpaqueSequence(LTLNonConsecutiveRepeatIntrinsic(min, max - min)(seq.inner))
   }
@@ -206,7 +217,7 @@ object Sequence {
   /** Form the conjunction of two sequences. Equivalent to
     * `arg0 and arg1 and ... and argN` in SVA.
     */
-  def and(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _and(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueSequence(LTLAndIntrinsic(lhs.inner, rhs.inner))
@@ -217,7 +228,7 @@ object Sequence {
   /** Form the disjunction of two sequences. Equivalent to
     * `arg0 or arg1 or ... or argN` in SVA.
     */
-  def or(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _or(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueSequence(LTLOrIntrinsic(lhs.inner, rhs.inner))
@@ -229,7 +240,7 @@ object Sequence {
     * times of both sequences must be identical. Equivalent to
     * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
     */
-  def intersect(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _intersect(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueSequence(LTLIntersectIntrinsic(lhs.inner, rhs.inner))
@@ -241,13 +252,13 @@ object Sequence {
     * This operator is weak: the property will hold even if input always
     * holds and condition never holds.
     */
-  def until(arg0: Sequence, arg1: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
+  protected def _until(arg0: Sequence, arg1: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLUntilIntrinsic(arg0.inner, arg1.inner))
 
   /** Specify a `clock` relative to which all cycle delays within `seq` are
     * specified. Equivalent to `@(posedge clock) seq` in SVA.
     */
-  def clock(seq: Sequence, clock: Clock)(implicit sourceInfo: SourceInfo): Sequence =
+  protected def _clock(seq: Sequence, clock: Clock)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLClockIntrinsic(seq.inner, clock))
 
   /** Convenience constructor for sequences. Allows for the following syntax:
@@ -256,17 +267,17 @@ object Sequence {
     *
     * See `SequenceAtom` for more details.
     */
-  def apply(atoms: SequenceAtom*)(implicit sourceInfo: SourceInfo): Sequence = {
+  protected def _apply(atoms: SequenceAtom*)(implicit sourceInfo: SourceInfo): Sequence = {
     require(atoms.nonEmpty)
     def needDelayTail = {
       require(
         atoms.tail.nonEmpty,
         "`Delay` operator in `Sequence(...)` must be followed by an item to be delayed"
       )
-      Sequence(atoms.tail: _*)
+      apply(atoms.tail: _*)
     }
     atoms.head match {
-      case seq: Sequence if atoms.tail.nonEmpty => seq.concat(Sequence(atoms.tail: _*))
+      case seq: Sequence if atoms.tail.nonEmpty => seq.concat(apply(atoms.tail: _*))
       case seq: Sequence                        => seq
       case DelayAtom(min, None)      => needDelayTail.delayAtLeast(min)
       case DelayAtom(min, Some(max)) => needDelayTail.delayRange(min, max)
@@ -275,7 +286,7 @@ object Sequence {
 }
 
 /** A Linear Temporal Logic (LTL) property. */
-sealed trait Property {
+sealed trait Property extends PropertyIntf {
 
   /** The underlying `Bool` that is returned and accepted by the LTL
     * intrinsics.
@@ -283,25 +294,27 @@ sealed trait Property {
   private[ltl] def inner: Bool
 
   /** See `Property.not`. */
-  def not(implicit sourceInfo: SourceInfo): Property = Property.not(this)
+  protected def _notImpl(implicit sourceInfo: SourceInfo): Property = Property._not(this)
 
   /** See `Property.eventually`. */
-  def eventually(implicit sourceInfo: SourceInfo): Property = Property.eventually(this)
+  protected def _eventuallyImpl(implicit sourceInfo: SourceInfo): Property = Property._eventually(this)
 
   /** See `Property.and`. */
-  def and(other: Property)(implicit sourceInfo: SourceInfo): Property = Property.and(this, other)
+  protected def _andPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property = Property._and(this, other)
 
   /** See `Property.or`. */
-  def or(other: Property)(implicit sourceInfo: SourceInfo): Property = Property.or(this, other)
+  protected def _orPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property = Property._or(this, other)
 
   /** See `Property.intersect`. */
-  def intersect(other: Property)(implicit sourceInfo: SourceInfo): Property = Property.intersect(this, other)
+  protected def _intersectPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property =
+    Property._intersect(this, other)
 
   /** See `Property.until`. */
-  def until(other: Property)(implicit sourceInfo: SourceInfo): Property = Property.until(this, other)
+  protected def _untilPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property =
+    Property._until(this, other)
 
   /** See `Property.clock`. */
-  def clock(clock: Clock)(implicit sourceInfo: SourceInfo): Property = Property.clock(this, clock)
+  protected def _clockImpl(clock: Clock)(implicit sourceInfo: SourceInfo): Property = Property._clock(this, clock)
 }
 
 /** Prefix-style utilities to work with properties.
@@ -309,25 +322,25 @@ sealed trait Property {
   * This object exposes the primary API to create and compose properties from
   * booleans, sequences, and other properties.
   */
-object Property {
+object Property extends Property$Intf {
 
   /** Negate a property. Equivalent to `not prop` in SVA. */
-  def not(prop: Property)(implicit sourceInfo: SourceInfo): Property =
+  protected def _not(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLNotIntrinsic(prop.inner))
 
   /** Precondition the checking of a property (the consequent) on a sequence
     * (the antecedent). Equivalent to the overlapping implication `seq |-> prop`
     * in SVA.
     */
-  def implication(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property =
+  protected def _implication(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLImplicationIntrinsic(seq.inner, prop.inner))
 
   /** Non-overlapping variant of `Property.implication`. Equivalent to
     * `seq ##1 true |-> prop` and `seq |=> prop` in SVA.
     */
-  def implicationNonOverlapping(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property = {
+  protected def _implicationNonOverlapping(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property = {
     import Sequence.BoolSequence
-    Property.implication(seq.concat(true.B.delay(1)), prop)
+    implication(seq.concat(true.B.delay(1)), prop)
   }
 
   /** Indicate that a property will eventually hold at a future point in time.
@@ -337,13 +350,13 @@ object Property {
     *
     * Equivalent to `s_eventually prop` in SVA.
     */
-  def eventually(prop: Property)(implicit sourceInfo: SourceInfo): Property =
+  protected def _eventually(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLEventuallyIntrinsic(prop.inner))
 
   /** Form the conjunction of two properties. Equivalent to
     * `arg0 and arg1 and ... and argN` in SVA.
     */
-  def and(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
+  protected def _and(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueProperty(LTLAndIntrinsic(lhs.inner, rhs.inner))
@@ -354,7 +367,7 @@ object Property {
   /** Form the disjunction of two properties. Equivalent to
     * `arg0 or arg1 or ... or argN` in SVA.
     */
-  def or(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
+  protected def _or(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueProperty(LTLOrIntrinsic(lhs.inner, rhs.inner))
@@ -366,7 +379,7 @@ object Property {
     * times of both sequences must be identical. Equivalent to
     * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
     */
-  def intersect(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
+  protected def _intersect(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
     var lhs = arg0
     for (rhs <- argN) {
       lhs = OpaqueProperty(LTLIntersectIntrinsic(lhs.inner, rhs.inner))
@@ -378,20 +391,20 @@ object Property {
     * This operator is weak: the property will hold even if input always
     * holds and condition never holds.
     */
-  def until(arg0: Property, arg1: Property)(implicit sourceInfo: SourceInfo): Property =
+  protected def _until(arg0: Property, arg1: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLUntilIntrinsic(arg0.inner, arg1.inner))
 
   /** Specify a `clock` relative to which all cycle delays within `prop` are
     * specified. Equivalent to `@(posedge clock) prop` in SVA.
     */
-  def clock(prop: Property, clock: Clock)(implicit sourceInfo: SourceInfo): Property =
+  protected def _clock(prop: Property, clock: Clock)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLClockIntrinsic(prop.inner, clock))
 }
 
 /** The base class for the `AssertProperty`, `AssumeProperty`, and
   * `CoverProperty` verification constructs.
   */
-sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
+sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertPropertyLikeIntf {
 
   /** Assert, assume, or cover that a property holds.
     *
@@ -406,7 +419,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     *   cover construct in the output language. In SystemVerilog, this is
     *   emitted as `label: assert(...)`.
     */
-  def apply(
+  protected def _applyImpl(
     prop:    => Property,
     clock:   Option[Clock] = Module.clockOption,
     disable: Option[Disable] = Module.disableOption,
@@ -424,7 +437,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     * This will generate a boolean property that is clocked using the implicit clock
     * and disabled in the case where the design has not yet been reset.
     */
-  def apply(
+  protected def _applyCondImpl(
     cond: Bool
   )(
     implicit sourceInfo: SourceInfo
@@ -440,7 +453,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     * This will generate a boolean property that is clocked using the implicit clock
     * and disabled in the case where the design has not yet been reset.
     */
-  def apply(
+  protected def _applyCondLabelImpl(
     cond:  Bool,
     label: String
   )(
@@ -463,7 +476,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     * This will generate a boolean property that is clocked using the implicit clock
     * and disabled in the case where the design has not yet been reset.
     */
-  def apply(
+  protected def _applyCondClockDisableLabelImpl(
     cond:    Bool,
     clock:   Clock,
     disable: Disable,
@@ -482,7 +495,9 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
   * Use like `AssertProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object AssertProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assert) {
+object AssertProperty
+    extends AssertPropertyLike(defaultLayer = layers.Verification.Assert)
+    with AssertProperty$Intf {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifAssertIntrinsic(label)
 }
 
@@ -491,7 +506,9 @@ object AssertProperty extends AssertPropertyLike(defaultLayer = layers.Verificat
   * Use like `AssumeProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object AssumeProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assume) {
+object AssumeProperty
+    extends AssertPropertyLike(defaultLayer = layers.Verification.Assume)
+    with AssumeProperty$Intf {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifAssumeIntrinsic(label)
 }
 
@@ -500,7 +517,9 @@ object AssumeProperty extends AssertPropertyLike(defaultLayer = layers.Verificat
   * Use like `CoverProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object CoverProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Cover) {
+object CoverProperty
+    extends AssertPropertyLike(defaultLayer = layers.Verification.Cover)
+    with CoverProperty$Intf {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifCoverIntrinsic(label)
 }
 
@@ -517,7 +536,9 @@ object CoverProperty extends AssertPropertyLike(defaultLayer = layers.Verificati
   * Use like `RequireProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object RequireProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assume) {
+object RequireProperty
+    extends AssertPropertyLike(defaultLayer = layers.Verification.Assume)
+    with RequireProperty$Intf {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifRequireIntrinsic(label)
 }
 
@@ -534,6 +555,8 @@ object RequireProperty extends AssertPropertyLike(defaultLayer = layers.Verifica
   * Use like `EnsureProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object EnsureProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assert) {
+object EnsureProperty
+    extends AssertPropertyLike(defaultLayer = layers.Verification.Assert)
+    with EnsureProperty$Intf {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifEnsureIntrinsic(label)
 }

From 0420ba088ebf2c479985ed772f1de04dae7c333a Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Wed, 28 Jan 2026 21:00:32 -0800
Subject: [PATCH 2/9] Remove unneeded interfaces

---
 src/main/scala-2/chisel3/ltl/LTLIntf.scala |  8 +-------
 src/main/scala-3/chisel3/ltl/LTLIntf.scala |  9 +--------
 src/main/scala/chisel3/ltl/LTL.scala       | 20 +++++---------------
 3 files changed, 7 insertions(+), 30 deletions(-)

diff --git a/src/main/scala-2/chisel3/ltl/LTLIntf.scala b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
index c92ae88d01f..51e05b19c1b 100644
--- a/src/main/scala-2/chisel3/ltl/LTLIntf.scala
+++ b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
@@ -206,10 +206,4 @@ private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
   )(
     implicit sourceInfo: SourceInfo
   ): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
-}
-
-private[chisel3] trait AssertProperty$Intf extends AssertPropertyLikeIntf { self: AssertProperty.type => }
-private[chisel3] trait AssumeProperty$Intf extends AssertPropertyLikeIntf { self: AssumeProperty.type => }
-private[chisel3] trait CoverProperty$Intf extends AssertPropertyLikeIntf { self: CoverProperty.type => }
-private[chisel3] trait RequireProperty$Intf extends AssertPropertyLikeIntf { self: RequireProperty.type => }
-private[chisel3] trait EnsureProperty$Intf extends AssertPropertyLikeIntf { self: EnsureProperty.type => }
+}
\ No newline at end of file
diff --git a/src/main/scala-3/chisel3/ltl/LTLIntf.scala b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
index 2923c0d62c7..1e5b1e258cf 100644
--- a/src/main/scala-3/chisel3/ltl/LTLIntf.scala
+++ b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
@@ -202,11 +202,4 @@ private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
     disable: Disable,
     label:   String
   )(using SourceInfo): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
-}
-
-private[chisel3] trait AssertProperty$Intf extends AssertPropertyLikeIntf { self: AssertProperty.type => }
-private[chisel3] trait AssumeProperty$Intf extends AssertPropertyLikeIntf { self: AssumeProperty.type => }
-private[chisel3] trait CoverProperty$Intf extends AssertPropertyLikeIntf { self: CoverProperty.type => }
-private[chisel3] trait RequireProperty$Intf extends AssertPropertyLikeIntf { self: RequireProperty.type => }
-private[chisel3] trait EnsureProperty$Intf extends AssertPropertyLikeIntf { self: EnsureProperty.type => }
-
+}
\ No newline at end of file
diff --git a/src/main/scala/chisel3/ltl/LTL.scala b/src/main/scala/chisel3/ltl/LTL.scala
index 7f5717e9abb..a0f23f520d8 100644
--- a/src/main/scala/chisel3/ltl/LTL.scala
+++ b/src/main/scala/chisel3/ltl/LTL.scala
@@ -495,9 +495,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertProp
   * Use like `AssertProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object AssertProperty
-    extends AssertPropertyLike(defaultLayer = layers.Verification.Assert)
-    with AssertProperty$Intf {
+object AssertProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assert) {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifAssertIntrinsic(label)
 }
 
@@ -506,9 +504,7 @@ object AssertProperty
   * Use like `AssumeProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object AssumeProperty
-    extends AssertPropertyLike(defaultLayer = layers.Verification.Assume)
-    with AssumeProperty$Intf {
+object AssumeProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assume) {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifAssumeIntrinsic(label)
 }
 
@@ -517,9 +513,7 @@ object AssumeProperty
   * Use like `CoverProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object CoverProperty
-    extends AssertPropertyLike(defaultLayer = layers.Verification.Cover)
-    with CoverProperty$Intf {
+object CoverProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Cover) {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifCoverIntrinsic(label)
 }
 
@@ -536,9 +530,7 @@ object CoverProperty
   * Use like `RequireProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object RequireProperty
-    extends AssertPropertyLike(defaultLayer = layers.Verification.Assume)
-    with RequireProperty$Intf {
+object RequireProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assume) {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifRequireIntrinsic(label)
 }
 
@@ -555,8 +547,6 @@ object RequireProperty
   * Use like `EnsureProperty(p)`. See `AssertPropertyLike.apply` for optional
   * clock, disable_iff, and label parameters.
   */
-object EnsureProperty
-    extends AssertPropertyLike(defaultLayer = layers.Verification.Assert)
-    with EnsureProperty$Intf {
+object EnsureProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assert) {
   protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifEnsureIntrinsic(label)
 }

From 75a83e6fb09b7da81054f77985e9d96a4b460059 Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Wed, 28 Jan 2026 21:31:27 -0800
Subject: [PATCH 3/9] Copy ScalaDoc

---
 src/main/scala-2/chisel3/ltl/LTLIntf.scala | 150 ++++++++++++++++----
 src/main/scala-3/chisel3/ltl/LTLIntf.scala | 150 ++++++++++++++++----
 src/main/scala/chisel3/ltl/LTL.scala       | 157 ---------------------
 3 files changed, 252 insertions(+), 205 deletions(-)

diff --git a/src/main/scala-2/chisel3/ltl/LTLIntf.scala b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
index 51e05b19c1b..2d67d8759f6 100644
--- a/src/main/scala-2/chisel3/ltl/LTLIntf.scala
+++ b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
@@ -101,90 +101,165 @@ private[chisel3] trait PropertyIntf { self: Property =>
 
 private[chisel3] trait Sequence$Intf { self: Sequence.type =>
 
-  /** Delay a sequence by a fixed number of cycles. */
+  /** Delay a sequence by a fixed number of cycles. Equivalent to `##delay` in
+    * SVA.
+    */
   def delay(seq: Sequence, delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = _delay(seq, delay)
 
-  /** Delay a sequence by a bounded range of cycles. */
+  /** Delay a sequence by a bounded range of cycles. Equivalent to `##[min:max]`
+    * in SVA.
+    */
   def delayRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     _delayRange(seq, min, max)
 
-  /** Delay a sequence by an unbounded range of cycles. */
+  /** Delay a sequence by an unbounded range of cycles. Equivalent to
+    * `##[delay:$]` in SVA.
+    */
   def delayAtLeast(seq: Sequence, delay: Int)(implicit sourceInfo: SourceInfo): Sequence = _delayAtLeast(seq, delay)
 
-  /** Concatenate multiple sequences. */
+  /** Concatenate multiple sequences. Equivalent to
+    * `arg0 ##0 arg1 ##0 ... ##0 argN` in SVA.
+    */
   def concat(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = _concat(arg0, argN: _*)
 
-  /** Repeat a sequence a fixed number of consecutive times. */
+  /** Repeat a sequence a fixed number of consecutive times. Equivalent to `s[n]` in
+    * SVA.
+    */
   def repeat(seq: Sequence, n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = _repeat(seq, n)
 
-  /** Repeat a sequence by a bounded range of consecutive times. */
+  /** Repeat a sequence by a bounded range of consecutive times. Equivalent to `s[min:max]`
+    * in SVA.
+    */
   def repeatRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     _repeatRange(seq, min, max)
 
-  /** Repeat a sequence by an unbounded range of consecutive times. */
+  /** Repeat a sequence by an unbounded range of consecutive times. Equivalent to
+    * `s[n:$]` in SVA.
+    */
   def repeatAtLeast(seq: Sequence, n: Int)(implicit sourceInfo: SourceInfo): Sequence = _repeatAtLeast(seq, n)
 
-  /** GoTo-style repitition of a sequence. */
+  /** GoTo-style repitition of a sequence a fixed number of non-consecutive times,
+    * where the final evaluation of the sequence must hold, e.g.
+    * a !b b b !b !b b c represents a matching observation of `gotoRepeat(b, 1, 3)`,
+    * but a !b b b !b !b b !b c does not. Equivalent to `s[->min:max]` in SVA.
+    */
   def gotoRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     _gotoRepeat(seq, min, max)
 
-  /** Repeat a sequence a fixed number of non-consecutive times. */
+  /** Repeat a sequence a fixed number of non-consecutive times,
+    * where the final evaluation of the sequence does not have to hold, e.g.
+    * both a !b b b !b !b b c and a !b b b !b !b b !b c represent matching
+    * observations of `nonConsecutiveRepeat(b, 1, 3)`. Equivalent to `s[=min:max]` in SVA.
+    */
   def nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     _nonConsecutiveRepeat(seq, min, max)
 
-  /** Form the conjunction of two sequences. */
+  /** Form the conjunction of two sequences. Equivalent to
+    * `arg0 and arg1 and ... and argN` in SVA.
+    */
   def and(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = _and(arg0, argN: _*)
 
-  /** Form the disjunction of two sequences. */
+  /** Form the disjunction of two sequences. Equivalent to
+    * `arg0 or arg1 or ... or argN` in SVA.
+    */
   def or(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = _or(arg0, argN: _*)
 
-  /** Form the intersection of two sequences. */
+  /** Form the conjunction of two sequences, where the start and end
+    * times of both sequences must be identical. Equivalent to
+    * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
+    */
   def intersect(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence =
     _intersect(arg0, argN: _*)
 
-  /** Check that a sequence holds until another sequence holds. */
+  /** Check that a sequence holds untile another sequence holds.
+    * This operator is weak: the property will hold even if input always
+    * holds and condition never holds.
+    */
   def until(arg0: Sequence, arg1: Sequence)(implicit sourceInfo: SourceInfo): Sequence = _until(arg0, arg1)
 
-  /** Specify a clock relative to which all cycle delays are specified. */
+  /** Specify a `clock` relative to which all cycle delays within `seq` are
+    * specified. Equivalent to `@(posedge clock) seq` in SVA.
+    */
   def clock(seq: Sequence, clock: Clock)(implicit sourceInfo: SourceInfo): Sequence = _clock(seq, clock)
 
-  /** Convenience constructor for sequences. */
+  /** Convenience constructor for sequences. Allows for the following syntax:
+    *
+    * `Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e)`
+    *
+    * See `SequenceAtom` for more details.
+    */
   def apply(atoms: SequenceAtom*)(implicit sourceInfo: SourceInfo): Sequence = _apply(atoms: _*)
 }
 
 private[chisel3] trait Property$Intf { self: Property.type =>
 
-  /** Negate a property. */
+  /** Negate a property. Equivalent to `not prop` in SVA. */
   def not(prop: Property)(implicit sourceInfo: SourceInfo): Property = _not(prop)
 
-  /** Precondition the checking of a property on a sequence. */
+  /** Precondition the checking of a property (the consequent) on a sequence
+    * (the antecedent). Equivalent to the overlapping implication `seq |-> prop`
+    * in SVA.
+    */
   def implication(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property = _implication(seq, prop)
 
-  /** Non-overlapping variant of implication. */
+  /** Non-overlapping variant of `Property.implication`. Equivalent to
+    * `seq ##1 true |-> prop` and `seq |=> prop` in SVA.
+    */
   def implicationNonOverlapping(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property =
     _implicationNonOverlapping(seq, prop)
 
-  /** Indicate that a property will eventually hold. */
+  /** Indicate that a property will eventually hold at a future point in time.
+    * This is a *strong* eventually, so the property has to hold within a finite
+    * number of cycles. The property does not trivially hold by waiting an
+    * infinite number of cycles.
+    *
+    * Equivalent to `s_eventually prop` in SVA.
+    */
   def eventually(prop: Property)(implicit sourceInfo: SourceInfo): Property = _eventually(prop)
 
-  /** Form the conjunction of two properties. */
+  /** Form the conjunction of two properties. Equivalent to
+    * `arg0 and arg1 and ... and argN` in SVA.
+    */
   def and(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = _and(arg0, argN: _*)
 
-  /** Form the disjunction of two properties. */
+  /** Form the disjunction of two properties. Equivalent to
+    * `arg0 or arg1 or ... or argN` in SVA.
+    */
   def or(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = _or(arg0, argN: _*)
 
-  /** Form the intersection of two properties. */
+  /** Form the conjunction of two properties, where the start and end
+    * times of both sequences must be identical. Equivalent to
+    * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
+    */
   def intersect(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = _intersect(arg0, argN: _*)
 
-  /** Check that a property holds until another property holds. */
+  /** Check that a property holds untile another property holds.
+    * This operator is weak: the property will hold even if input always
+    * holds and condition never holds.
+    */
   def until(arg0: Property, arg1: Property)(implicit sourceInfo: SourceInfo): Property = _until(arg0, arg1)
 
-  /** Specify a clock relative to which all cycle delays are specified. */
+  /** Specify a `clock` relative to which all cycle delays within `prop` are
+    * specified. Equivalent to `@(posedge clock) prop` in SVA.
+    */
   def clock(prop: Property, clock: Clock)(implicit sourceInfo: SourceInfo): Property = _clock(prop, clock)
 }
 
 private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
 
+  /** Assert, assume, or cover that a property holds.
+    *
+    * @param prop: parameter can be a `Property`, `Sequence`, or simple `Bool`.
+    * @param clock [optional]: specifies a clock with respect to which all cycle
+    *   delays in the property are expressed. This is a shorthand for
+    *   `prop.clock(clock)`.
+    * @param disable [optional]: specifies a condition under which the evaluation
+    *   of the property is disabled. This is a shorthand for
+    *   `prop.disable(disable)`.
+    * @param label [optional]: is used to assign a name to the assert, assume, or
+    *   cover construct in the output language. In SystemVerilog, this is
+    *   emitted as `label: assert(...)`.
+    */
   def apply(
     prop:    => Property,
     clock:   Option[Clock] = Module.clockOption,
@@ -194,10 +269,37 @@ private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
     implicit sourceInfo: SourceInfo
   ): Unit = _applyImpl(prop, clock, disable, label)
 
+  /** Assert, assume, or cover that a boolean predicate holds.
+    * @param cond: a boolean predicate that should be checked.
+    * This will generate a boolean property that is clocked using the implicit clock
+    * and disabled in the case where the design has not yet been reset.
+    */
   def apply(cond: Bool)(implicit sourceInfo: SourceInfo): Unit = _applyCondImpl(cond)
 
+  /** Assert, assume, or cover that a boolean predicate holds.
+    * @param cond: a boolean predicate that should be checked.
+    * @param label: is used to assign a name to the assert, assume, or
+    *   cover construct in the output language. In SystemVerilog, this is
+    *   emitted as `label: assert(...)`.
+    * This will generate a boolean property that is clocked using the implicit clock
+    * and disabled in the case where the design has not yet been reset.
+    */
   def apply(cond: Bool, label: String)(implicit sourceInfo: SourceInfo): Unit = _applyCondLabelImpl(cond, label)
 
+  /** Assert, assume, or cover that a boolean predicate holds.
+    * @param cond: a boolean predicate that should be checked.
+    * @param clock: specifies a clock with respect to which all cycle
+    *   delays in the property are expressed. This is a shorthand for
+    *   `prop.clock(clock)`.
+    * @param disable: specifies a condition under which the evaluation
+    *   of the property is disabled. This is a shorthand for
+    *   `prop.disable(disable)`.
+    * @param label: is used to assign a name to the assert, assume, or
+    *   cover construct in the output language. In SystemVerilog, this is
+    *   emitted as `label: assert(...)`.
+    * This will generate a boolean property that is clocked using the implicit clock
+    * and disabled in the case where the design has not yet been reset.
+    */
   def apply(
     cond:    Bool,
     clock:   Clock,
diff --git a/src/main/scala-3/chisel3/ltl/LTLIntf.scala b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
index 1e5b1e258cf..d0b7bef6d3a 100644
--- a/src/main/scala-3/chisel3/ltl/LTLIntf.scala
+++ b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
@@ -101,90 +101,165 @@ private[chisel3] trait PropertyIntf { self: Property =>
 
 private[chisel3] trait Sequence$Intf { self: Sequence.type =>
 
-  /** Delay a sequence by a fixed number of cycles. */
+  /** Delay a sequence by a fixed number of cycles. Equivalent to `##delay` in
+    * SVA.
+    */
   def delay(seq: Sequence, delay: Int = 1)(using SourceInfo): Sequence = _delay(seq, delay)
 
-  /** Delay a sequence by a bounded range of cycles. */
+  /** Delay a sequence by a bounded range of cycles. Equivalent to `##[min:max]`
+    * in SVA.
+    */
   def delayRange(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
     _delayRange(seq, min, max)
 
-  /** Delay a sequence by an unbounded range of cycles. */
+  /** Delay a sequence by an unbounded range of cycles. Equivalent to
+    * `##[delay:$]` in SVA.
+    */
   def delayAtLeast(seq: Sequence, delay: Int)(using SourceInfo): Sequence = _delayAtLeast(seq, delay)
 
-  /** Concatenate multiple sequences. */
+  /** Concatenate multiple sequences. Equivalent to
+    * `arg0 ##0 arg1 ##0 ... ##0 argN` in SVA.
+    */
   def concat(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _concat(arg0, argN: _*)
 
-  /** Repeat a sequence a fixed number of consecutive times. */
+  /** Repeat a sequence a fixed number of consecutive times. Equivalent to `s[n]` in
+    * SVA.
+    */
   def repeat(seq: Sequence, n: Int = 1)(using SourceInfo): Sequence = _repeat(seq, n)
 
-  /** Repeat a sequence by a bounded range of consecutive times. */
+  /** Repeat a sequence by a bounded range of consecutive times. Equivalent to `s[min:max]`
+    * in SVA.
+    */
   def repeatRange(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
     _repeatRange(seq, min, max)
 
-  /** Repeat a sequence by an unbounded range of consecutive times. */
+  /** Repeat a sequence by an unbounded range of consecutive times. Equivalent to
+    * `s[n:$]` in SVA.
+    */
   def repeatAtLeast(seq: Sequence, n: Int)(using SourceInfo): Sequence = _repeatAtLeast(seq, n)
 
-  /** GoTo-style repitition of a sequence. */
+  /** GoTo-style repitition of a sequence a fixed number of non-consecutive times,
+    * where the final evaluation of the sequence must hold, e.g.
+    * a !b b b !b !b b c represents a matching observation of `gotoRepeat(b, 1, 3)`,
+    * but a !b b b !b !b b !b c does not. Equivalent to `s[->min:max]` in SVA.
+    */
   def gotoRepeat(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
     _gotoRepeat(seq, min, max)
 
-  /** Repeat a sequence a fixed number of non-consecutive times. */
+  /** Repeat a sequence a fixed number of non-consecutive times,
+    * where the final evaluation of the sequence does not have to hold, e.g.
+    * both a !b b b !b !b b c and a !b b b !b !b b !b c represent matching
+    * observations of `nonConsecutiveRepeat(b, 1, 3)`. Equivalent to `s[=min:max]` in SVA.
+    */
   def nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(using SourceInfo): Sequence =
     _nonConsecutiveRepeat(seq, min, max)
 
-  /** Form the conjunction of two sequences. */
+  /** Form the conjunction of two sequences. Equivalent to
+    * `arg0 and arg1 and ... and argN` in SVA.
+    */
   def and(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _and(arg0, argN: _*)
 
-  /** Form the disjunction of two sequences. */
+  /** Form the disjunction of two sequences. Equivalent to
+    * `arg0 or arg1 or ... or argN` in SVA.
+    */
   def or(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _or(arg0, argN: _*)
 
-  /** Form the intersection of two sequences. */
+  /** Form the conjunction of two sequences, where the start and end
+    * times of both sequences must be identical. Equivalent to
+    * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
+    */
   def intersect(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence =
     _intersect(arg0, argN: _*)
 
-  /** Check that a sequence holds until another sequence holds. */
+  /** Check that a sequence holds untile another sequence holds.
+    * This operator is weak: the property will hold even if input always
+    * holds and condition never holds.
+    */
   def until(arg0: Sequence, arg1: Sequence)(using SourceInfo): Sequence = _until(arg0, arg1)
 
-  /** Specify a clock relative to which all cycle delays are specified. */
+  /** Specify a `clock` relative to which all cycle delays within `seq` are
+    * specified. Equivalent to `@(posedge clock) seq` in SVA.
+    */
   def clock(seq: Sequence, clock: Clock)(using SourceInfo): Sequence = _clock(seq, clock)
 
-  /** Convenience constructor for sequences. */
+  /** Convenience constructor for sequences. Allows for the following syntax:
+    *
+    * `Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e)`
+    *
+    * See `SequenceAtom` for more details.
+    */
   def apply(atoms: SequenceAtom*)(using SourceInfo): Sequence = _apply(atoms: _*)
 }
 
 private[chisel3] trait Property$Intf { self: Property.type =>
 
-  /** Negate a property. */
+  /** Negate a property. Equivalent to `not prop` in SVA. */
   def not(prop: Property)(using SourceInfo): Property = _not(prop)
 
-  /** Precondition the checking of a property on a sequence. */
+  /** Precondition the checking of a property (the consequent) on a sequence
+    * (the antecedent). Equivalent to the overlapping implication `seq |-> prop`
+    * in SVA.
+    */
   def implication(seq: Sequence, prop: Property)(using SourceInfo): Property = _implication(seq, prop)
 
-  /** Non-overlapping variant of implication. */
+  /** Non-overlapping variant of `Property.implication`. Equivalent to
+    * `seq ##1 true |-> prop` and `seq |=> prop` in SVA.
+    */
   def implicationNonOverlapping(seq: Sequence, prop: Property)(using SourceInfo): Property =
     _implicationNonOverlapping(seq, prop)
 
-  /** Indicate that a property will eventually hold. */
+  /** Indicate that a property will eventually hold at a future point in time.
+    * This is a *strong* eventually, so the property has to hold within a finite
+    * number of cycles. The property does not trivially hold by waiting an
+    * infinite number of cycles.
+    *
+    * Equivalent to `s_eventually prop` in SVA.
+    */
   def eventually(prop: Property)(using SourceInfo): Property = _eventually(prop)
 
-  /** Form the conjunction of two properties. */
+  /** Form the conjunction of two properties. Equivalent to
+    * `arg0 and arg1 and ... and argN` in SVA.
+    */
   def and(arg0: Property, argN: Property*)(using SourceInfo): Property = _and(arg0, argN: _*)
 
-  /** Form the disjunction of two properties. */
+  /** Form the disjunction of two properties. Equivalent to
+    * `arg0 or arg1 or ... or argN` in SVA.
+    */
   def or(arg0: Property, argN: Property*)(using SourceInfo): Property = _or(arg0, argN: _*)
 
-  /** Form the intersection of two properties. */
+  /** Form the conjunction of two properties, where the start and end
+    * times of both sequences must be identical. Equivalent to
+    * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
+    */
   def intersect(arg0: Property, argN: Property*)(using SourceInfo): Property = _intersect(arg0, argN: _*)
 
-  /** Check that a property holds until another property holds. */
+  /** Check that a property holds untile another property holds.
+    * This operator is weak: the property will hold even if input always
+    * holds and condition never holds.
+    */
   def until(arg0: Property, arg1: Property)(using SourceInfo): Property = _until(arg0, arg1)
 
-  /** Specify a clock relative to which all cycle delays are specified. */
+  /** Specify a `clock` relative to which all cycle delays within `prop` are
+    * specified. Equivalent to `@(posedge clock) prop` in SVA.
+    */
   def clock(prop: Property, clock: Clock)(using SourceInfo): Property = _clock(prop, clock)
 }
 
 private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
 
+  /** Assert, assume, or cover that a property holds.
+    *
+    * @param prop: parameter can be a `Property`, `Sequence`, or simple `Bool`.
+    * @param clock [optional]: specifies a clock with respect to which all cycle
+    *   delays in the property are expressed. This is a shorthand for
+    *   `prop.clock(clock)`.
+    * @param disable [optional]: specifies a condition under which the evaluation
+    *   of the property is disabled. This is a shorthand for
+    *   `prop.disable(disable)`.
+    * @param label [optional]: is used to assign a name to the assert, assume, or
+    *   cover construct in the output language. In SystemVerilog, this is
+    *   emitted as `label: assert(...)`.
+    */
   def apply(
     prop:    => Property,
     clock:   Option[Clock] = Module.clockOption,
@@ -192,10 +267,37 @@ private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
     label:   Option[String] = None
   )(using SourceInfo): Unit = _applyImpl(prop, clock, disable, label)
 
+  /** Assert, assume, or cover that a boolean predicate holds.
+    * @param cond: a boolean predicate that should be checked.
+    * This will generate a boolean property that is clocked using the implicit clock
+    * and disabled in the case where the design has not yet been reset.
+    */
   def apply(cond: Bool)(using SourceInfo): Unit = _applyCondImpl(cond)
 
+  /** Assert, assume, or cover that a boolean predicate holds.
+    * @param cond: a boolean predicate that should be checked.
+    * @param label: is used to assign a name to the assert, assume, or
+    *   cover construct in the output language. In SystemVerilog, this is
+    *   emitted as `label: assert(...)`.
+    * This will generate a boolean property that is clocked using the implicit clock
+    * and disabled in the case where the design has not yet been reset.
+    */
   def apply(cond: Bool, label: String)(using SourceInfo): Unit = _applyCondLabelImpl(cond, label)
 
+  /** Assert, assume, or cover that a boolean predicate holds.
+    * @param cond: a boolean predicate that should be checked.
+    * @param clock: specifies a clock with respect to which all cycle
+    *   delays in the property are expressed. This is a shorthand for
+    *   `prop.clock(clock)`.
+    * @param disable: specifies a condition under which the evaluation
+    *   of the property is disabled. This is a shorthand for
+    *   `prop.disable(disable)`.
+    * @param label: is used to assign a name to the assert, assume, or
+    *   cover construct in the output language. In SystemVerilog, this is
+    *   emitted as `label: assert(...)`.
+    * This will generate a boolean property that is clocked using the implicit clock
+    * and disabled in the case where the design has not yet been reset.
+    */
   def apply(
     cond:    Bool,
     clock:   Clock,
diff --git a/src/main/scala/chisel3/ltl/LTL.scala b/src/main/scala/chisel3/ltl/LTL.scala
index a0f23f520d8..bd65d1ab413 100644
--- a/src/main/scala/chisel3/ltl/LTL.scala
+++ b/src/main/scala/chisel3/ltl/LTL.scala
@@ -48,81 +48,60 @@ object Delay {
 /** A Linear Temporal Logic (LTL) sequence. */
 sealed trait Sequence extends Property with SequenceIntf {
 
-  /** See `Sequence.delay`. */
   protected def _delayImpl(delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = Sequence._delay(this, delay)
 
-  /** See `Sequence.delayRange`. */
   protected def _delayRangeImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._delayRange(this, min, max)
 
-  /** See `Sequence.delayAtLeast`. */
   protected def _delayAtLeastImpl(delay: Int)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._delayAtLeast(this, delay)
 
-  /** See `Sequence.concat`. */
   protected def _concatImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence._concat(this, other)
 
-  /** See `Sequence.repeat`. */
   protected def _repeatImpl(n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = Sequence._repeat(this, n)
 
-  /** See `Sequence.repeatRange`. */
   protected def _repeatRangeImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._repeatRange(this, min, max)
 
-  /** See `Sequence.repeatAtLeast`. */
   protected def _repeatAtLeastImpl(n: Int)(implicit sourceInfo: SourceInfo): Sequence = Sequence._repeatAtLeast(this, n)
 
-  /** See `Sequence.gotoRepeat`. */
   protected def _gotoRepeatImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._gotoRepeat(this, min, max)
 
-  /** See `Sequence.nonConsecutiveRepeat`. */
   protected def _nonConsecutiveRepeatImpl(min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._nonConsecutiveRepeat(this, min, max)
 
-  /** See `Sequence.and`. */
   protected def _andSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence._and(this, other)
 
-  /** See `Sequence.or`. */
   protected def _orSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = Sequence._or(this, other)
 
-  /** See `Sequence.intersect`. */
   protected def _intersectSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._intersect(this, other)
 
-  /** See `Sequence.until`. */
   protected def _untilSeqImpl(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._until(this, other)
 
-  /** See `Sequence.clock`. */
   override protected def _clockImpl(clock: Clock)(implicit sourceInfo: SourceInfo): Sequence =
     Sequence._clock(this, clock)
 
-  /** See `Property.implication`. */
   protected def _implicationImpl(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     Property.implication(this, prop)
 
-  /** See `Property.implication`. */
   protected def _implicationNonOverlappingImpl(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     Property.implicationNonOverlapping(this, prop)
 
   // Convenience operators.
 
-  /** Equivalent to `|->` in SVA. */
   protected def _impl_|->(prop: Property)(implicit sourceInfo: SourceInfo): Property = this.implication(prop)
 
-  /** Equivalent to `|=>` in SVA. */
   protected def _impl_|=>(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     this.implicationNonOverlapping(prop)
 
-  /** Equivalent to `a ##1 b` in SVA. */
   protected def _impl_###(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence = this.concat(other.delay())
 
-  /** Equivalent to `a ##[*] b` in SVA. */
   protected def _impl_##*(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
     this.concat(other.delayAtLeast(0))
 
-  /** Equivalent to `a ##[+] b` in SVA. */
   protected def _impl_##+(other: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
     this.concat(other.delayAtLeast(1))
 }
@@ -134,34 +113,19 @@ sealed trait Sequence extends Property with SequenceIntf {
   */
 object Sequence extends Sequence$Intf {
 
-  /** Implicitly wraps a `Bool` and allows it to be used as a sequence or
-    * property. Use via `import chisel3.ltl.Sequence.BoolSequence`.
-    */
   implicit class BoolSequence(val inner: Bool) extends Sequence with SequenceAtom
 
-  /** Delay a sequence by a fixed number of cycles. Equivalent to `##delay` in
-    * SVA.
-    */
   protected def _delay(seq: Sequence, delay: Int = 1)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLDelayIntrinsic(delay, Some(0))(seq.inner))
 
-  /** Delay a sequence by a bounded range of cycles. Equivalent to `##[min:max]`
-    * in SVA.
-    */
   protected def _delayRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(min <= max)
     OpaqueSequence(LTLDelayIntrinsic(min, Some(max - min))(seq.inner))
   }
 
-  /** Delay a sequence by an unbounded range of cycles. Equivalent to
-    * `##[delay:$]` in SVA.
-    */
   protected def _delayAtLeast(seq: Sequence, delay: Int)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLDelayIntrinsic(delay, None)(seq.inner))
 
-  /** Concatenate multiple sequences. Equivalent to
-    * `arg0 ##0 arg1 ##0 ... ##0 argN` in SVA.
-    */
   protected def _concat(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -170,53 +134,31 @@ object Sequence extends Sequence$Intf {
     lhs
   }
 
-  /** Repeat a sequence a fixed number of consecutive times. Equivalent to `s[n]` in
-    * SVA.
-    */
   protected def _repeat(seq: Sequence, n: Int = 1)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 < n)
     OpaqueSequence(LTLRepeatIntrinsic(n, Some(0))(seq.inner))
   }
 
-  /** Repeat a sequence by a bounded range of consecutive times. Equivalent to `s[min:max]`
-    * in SVA.
-    */
   protected def _repeatRange(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(min <= max)
     OpaqueSequence(LTLRepeatIntrinsic(min, Some(max - min))(seq.inner))
   }
 
-  /** Repeat a sequence by an unbounded range of consecutive times. Equivalent to
-    * `s[n:$]` in SVA.
-    */
   protected def _repeatAtLeast(seq: Sequence, n: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 < n)
     OpaqueSequence(LTLRepeatIntrinsic(n, None)(seq.inner))
   }
 
-  /** GoTo-style repitition of a sequence a fixed number of non-consecutive times,
-    * where the final evaluation of the sequence must hold, e.g.
-    * a !b b b !b !b b c represents a matching observation of `gotoRepeat(b, 1, 3)`,
-    * but a !b b b !b !b b !b c does not. Equivalent to `s[->min:max]` in SVA.
-    */
   protected def _gotoRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 <= min && min <= max)
     OpaqueSequence(LTLGoToRepeatIntrinsic(min, max - min)(seq.inner))
   }
 
-  /** Repeat a sequence a fixed number of non-consecutive times,
-    * where the final evaluation of the sequence does not have to hold, e.g.
-    * both a !b b b !b !b b c and a !b b b !b !b b !b c represent matching
-    * observations of `nonConsecutiveRepeat(b, 1, 3)`. Equivalent to `s[=min:max]` in SVA.
-    */
   protected def _nonConsecutiveRepeat(seq: Sequence, min: Int, max: Int)(implicit sourceInfo: SourceInfo): Sequence = {
     require(0 <= min && min <= max)
     OpaqueSequence(LTLNonConsecutiveRepeatIntrinsic(min, max - min)(seq.inner))
   }
 
-  /** Form the conjunction of two sequences. Equivalent to
-    * `arg0 and arg1 and ... and argN` in SVA.
-    */
   protected def _and(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -225,9 +167,6 @@ object Sequence extends Sequence$Intf {
     lhs
   }
 
-  /** Form the disjunction of two sequences. Equivalent to
-    * `arg0 or arg1 or ... or argN` in SVA.
-    */
   protected def _or(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -236,10 +175,6 @@ object Sequence extends Sequence$Intf {
     lhs
   }
 
-  /** Form the conjunction of two sequences, where the start and end
-    * times of both sequences must be identical. Equivalent to
-    * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
-    */
   protected def _intersect(arg0: Sequence, argN: Sequence*)(implicit sourceInfo: SourceInfo): Sequence = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -248,25 +183,12 @@ object Sequence extends Sequence$Intf {
     lhs
   }
 
-  /** Check that a sequence holds untile another sequence holds.
-    * This operator is weak: the property will hold even if input always
-    * holds and condition never holds.
-    */
   protected def _until(arg0: Sequence, arg1: Sequence)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLUntilIntrinsic(arg0.inner, arg1.inner))
 
-  /** Specify a `clock` relative to which all cycle delays within `seq` are
-    * specified. Equivalent to `@(posedge clock) seq` in SVA.
-    */
   protected def _clock(seq: Sequence, clock: Clock)(implicit sourceInfo: SourceInfo): Sequence =
     OpaqueSequence(LTLClockIntrinsic(seq.inner, clock))
 
-  /** Convenience constructor for sequences. Allows for the following syntax:
-    *
-    * `Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e)`
-    *
-    * See `SequenceAtom` for more details.
-    */
   protected def _apply(atoms: SequenceAtom*)(implicit sourceInfo: SourceInfo): Sequence = {
     require(atoms.nonEmpty)
     def needDelayTail = {
@@ -293,27 +215,20 @@ sealed trait Property extends PropertyIntf {
     */
   private[ltl] def inner: Bool
 
-  /** See `Property.not`. */
   protected def _notImpl(implicit sourceInfo: SourceInfo): Property = Property._not(this)
 
-  /** See `Property.eventually`. */
   protected def _eventuallyImpl(implicit sourceInfo: SourceInfo): Property = Property._eventually(this)
 
-  /** See `Property.and`. */
   protected def _andPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property = Property._and(this, other)
 
-  /** See `Property.or`. */
   protected def _orPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property = Property._or(this, other)
 
-  /** See `Property.intersect`. */
   protected def _intersectPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property =
     Property._intersect(this, other)
 
-  /** See `Property.until`. */
   protected def _untilPropImpl(other: Property)(implicit sourceInfo: SourceInfo): Property =
     Property._until(this, other)
 
-  /** See `Property.clock`. */
   protected def _clockImpl(clock: Clock)(implicit sourceInfo: SourceInfo): Property = Property._clock(this, clock)
 }
 
@@ -324,38 +239,20 @@ sealed trait Property extends PropertyIntf {
   */
 object Property extends Property$Intf {
 
-  /** Negate a property. Equivalent to `not prop` in SVA. */
   protected def _not(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLNotIntrinsic(prop.inner))
 
-  /** Precondition the checking of a property (the consequent) on a sequence
-    * (the antecedent). Equivalent to the overlapping implication `seq |-> prop`
-    * in SVA.
-    */
   protected def _implication(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLImplicationIntrinsic(seq.inner, prop.inner))
 
-  /** Non-overlapping variant of `Property.implication`. Equivalent to
-    * `seq ##1 true |-> prop` and `seq |=> prop` in SVA.
-    */
   protected def _implicationNonOverlapping(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property = {
     import Sequence.BoolSequence
     implication(seq.concat(true.B.delay(1)), prop)
   }
 
-  /** Indicate that a property will eventually hold at a future point in time.
-    * This is a *strong* eventually, so the property has to hold within a finite
-    * number of cycles. The property does not trivially hold by waiting an
-    * infinite number of cycles.
-    *
-    * Equivalent to `s_eventually prop` in SVA.
-    */
   protected def _eventually(prop: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLEventuallyIntrinsic(prop.inner))
 
-  /** Form the conjunction of two properties. Equivalent to
-    * `arg0 and arg1 and ... and argN` in SVA.
-    */
   protected def _and(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -364,9 +261,6 @@ object Property extends Property$Intf {
     lhs
   }
 
-  /** Form the disjunction of two properties. Equivalent to
-    * `arg0 or arg1 or ... or argN` in SVA.
-    */
   protected def _or(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -375,10 +269,6 @@ object Property extends Property$Intf {
     lhs
   }
 
-  /** Form the conjunction of two properties, where the start and end
-    * times of both sequences must be identical. Equivalent to
-    * `arg0 intersect arg1 intersect ... intersect argN` in SVA.
-    */
   protected def _intersect(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property = {
     var lhs = arg0
     for (rhs <- argN) {
@@ -387,16 +277,9 @@ object Property extends Property$Intf {
     lhs
   }
 
-  /** Check that a property holds untile another property holds.
-    * This operator is weak: the property will hold even if input always
-    * holds and condition never holds.
-    */
   protected def _until(arg0: Property, arg1: Property)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLUntilIntrinsic(arg0.inner, arg1.inner))
 
-  /** Specify a `clock` relative to which all cycle delays within `prop` are
-    * specified. Equivalent to `@(posedge clock) prop` in SVA.
-    */
   protected def _clock(prop: Property, clock: Clock)(implicit sourceInfo: SourceInfo): Property =
     OpaqueProperty(LTLClockIntrinsic(prop.inner, clock))
 }
@@ -406,19 +289,6 @@ object Property extends Property$Intf {
   */
 sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertPropertyLikeIntf {
 
-  /** Assert, assume, or cover that a property holds.
-    *
-    * @param prop: parameter can be a `Property`, `Sequence`, or simple `Bool`.
-    * @param clock [optional]: specifies a clock with respect to which all cycle
-    *   delays in the property are expressed. This is a shorthand for
-    *   `prop.clock(clock)`.
-    * @param disable [optional]: specifies a condition under which the evaluation
-    *   of the property is disabled. This is a shorthand for
-    *   `prop.disable(disable)`.
-    * @param label [optional]: is used to assign a name to the assert, assume, or
-    *   cover construct in the output language. In SystemVerilog, this is
-    *   emitted as `label: assert(...)`.
-    */
   protected def _applyImpl(
     prop:    => Property,
     clock:   Option[Clock] = Module.clockOption,
@@ -432,11 +302,6 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertProp
     createIntrinsic(label)(sourceInfo)(clocked.inner, disable.map(!_.value))
   }
 
-  /** Assert, assume, or cover that a boolean predicate holds.
-    * @param cond: a boolean predicate that should be checked.
-    * This will generate a boolean property that is clocked using the implicit clock
-    * and disabled in the case where the design has not yet been reset.
-    */
   protected def _applyCondImpl(
     cond: Bool
   )(
@@ -445,14 +310,6 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertProp
     apply(Sequence.BoolSequence(cond))
   }
 
-  /** Assert, assume, or cover that a boolean predicate holds.
-    * @param cond: a boolean predicate that should be checked.
-    * @param label: is used to assign a name to the assert, assume, or
-    *   cover construct in the output language. In SystemVerilog, this is
-    *   emitted as `label: assert(...)`.
-    * This will generate a boolean property that is clocked using the implicit clock
-    * and disabled in the case where the design has not yet been reset.
-    */
   protected def _applyCondLabelImpl(
     cond:  Bool,
     label: String
@@ -462,20 +319,6 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertProp
     apply(Sequence.BoolSequence(cond), label = Some(label))
   }
 
-  /** Assert, assume, or cover that a boolean predicate holds.
-    * @param cond: a boolean predicate that should be checked.
-    * @param clock: specifies a clock with respect to which all cycle
-    *   delays in the property are expressed. This is a shorthand for
-    *   `prop.clock(clock)`.
-    * @param disable: specifies a condition under which the evaluation
-    *   of the property is disabled. This is a shorthand for
-    *   `prop.disable(disable)`.
-    * @param label: is used to assign a name to the assert, assume, or
-    *   cover construct in the output language. In SystemVerilog, this is
-    *   emitted as `label: assert(...)`.
-    * This will generate a boolean property that is clocked using the implicit clock
-    * and disabled in the case where the design has not yet been reset.
-    */
   protected def _applyCondClockDisableLabelImpl(
     cond:    Bool,
     clock:   Clock,

From f1ea0cc1cc1c17429fcae3eaa84e16d95bfe1bc0 Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Wed, 28 Jan 2026 21:48:40 -0800
Subject: [PATCH 4/9] Move LTLSpec to src/test/scala

---
 .../chiselTests/LTLSpec.scala                 | 26 +++++++++----------
 1 file changed, 13 insertions(+), 13 deletions(-)
 rename src/test/{scala-2 => scala}/chiselTests/LTLSpec.scala (95%)

diff --git a/src/test/scala-2/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala
similarity index 95%
rename from src/test/scala-2/chiselTests/LTLSpec.scala
rename to src/test/scala/chiselTests/LTLSpec.scala
index 92ed71fd1e9..290ce07bfc3 100644
--- a/src/test/scala-2/chiselTests/LTLSpec.scala
+++ b/src/test/scala/chiselTests/LTLSpec.scala
@@ -6,7 +6,7 @@ import chisel3._
 import chisel3.ltl._
 import chisel3.simulator.scalatest.ChiselSim
 import chisel3.simulator.stimulus.RunUntilFinished
-import chisel3.experimental.SourceLine
+import chisel3.experimental.{SourceInfo, SourceLine}
 import circt.stage.ChiselStage
 import org.scalatest.flatspec.AnyFlatSpec
 import org.scalatest.matchers.should.Matchers
@@ -34,7 +34,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class DelaysMod extends RawModule {
     val a, b, c = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val s0: Sequence = a.delay(1)
     val s1: Sequence = b.delayRange(2, 4)
     val s2: Sequence = c.delayAtLeast(5)
@@ -70,7 +70,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class ConcatMod extends RawModule {
     val a, b, c, d, e = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val s0: Sequence = a.concat(b)
     val s1: Sequence = Sequence.concat(c, d, e) // (c concat d) concat e
   }
@@ -92,7 +92,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class RepeatMod extends RawModule {
     val a, b, c, d, e = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val s0: Sequence = a.repeat(1)
     val s1: Sequence = b.repeatRange(2, 4)
     val s2: Sequence = c.repeatAtLeast(5)
@@ -126,7 +126,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class AndOrClockMod extends RawModule {
     val a, b = IO(Input(Bool()))
     val clock = IO(Input(Clock()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val s0: Sequence = a.delay()
     val s1: Sequence = s0.and(b)
     val s2: Sequence = s0.or(b)
@@ -186,7 +186,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class NotMod extends RawModule {
     val a = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val p0: Property = Property.not(a)
   }
   it should "support property not operation" in {
@@ -200,7 +200,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class PropImplicationMod extends RawModule {
     val a, b = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val p0: Property = Property.implication(a, b)
     val p1: Property = a |-> b
     val p2: Property = Property.implicationNonOverlapping(a, b)
@@ -236,7 +236,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class EventuallyMod extends RawModule {
     val a = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val p0: Property = a.eventually
   }
   it should "support property eventually operation" in {
@@ -250,7 +250,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class BasicVerifMod extends RawModule {
     val a = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     AssertProperty(a)
     AssumeProperty(a)
     CoverProperty(a)
@@ -282,7 +282,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   it should "not create layer blocks if already in a layer block" in {
     class Foo extends RawModule {
       val a = IO(Input(Bool()))
-      layer.block(layers.Verification.Cover) {
+      layer.block(chisel3.layers.Verification.Cover) {
         AssertProperty(a)
       }
     }
@@ -305,7 +305,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
     for ((prop, (intrinsic, op)) <- properties) {
       val chirrtl = ChiselStage.emitCHIRRTL(new Module {
         val a = IO(Input(Bool()))
-        implicit val info = SourceLine("Foo.scala", 1, 2)
+        implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
         prop(a)
       })
       val sourceLoc = "@[Foo.scala 1:2]"
@@ -361,7 +361,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class SequenceConvMod extends RawModule {
     val a, b = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     AssertProperty(Sequence(a))
     AssertProperty(Sequence(a, b))
     AssertProperty(Sequence(Delay(), a))
@@ -429,7 +429,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
   class LayerBlockMod extends RawModule {
     val a, b = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     AssertProperty(Sequence(Delay(), a))
     AssumeProperty(a |-> b)
   }

From 31422259fa2e2ff412c639e65757b94fb42884dc Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Wed, 28 Jan 2026 21:49:43 -0800
Subject: [PATCH 5/9] reformat intf

---
 src/main/scala-2/chisel3/ltl/LTLIntf.scala | 2 +-
 src/main/scala-3/chisel3/ltl/LTLIntf.scala | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala-2/chisel3/ltl/LTLIntf.scala b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
index 2d67d8759f6..d1c1ffda6cb 100644
--- a/src/main/scala-2/chisel3/ltl/LTLIntf.scala
+++ b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
@@ -308,4 +308,4 @@ private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
   )(
     implicit sourceInfo: SourceInfo
   ): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
-}
\ No newline at end of file
+}
diff --git a/src/main/scala-3/chisel3/ltl/LTLIntf.scala b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
index d0b7bef6d3a..5d2e625b2c9 100644
--- a/src/main/scala-3/chisel3/ltl/LTLIntf.scala
+++ b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
@@ -304,4 +304,4 @@ private[chisel3] trait AssertPropertyLikeIntf { self: AssertPropertyLike =>
     disable: Disable,
     label:   String
   )(using SourceInfo): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
-}
\ No newline at end of file
+}

From 6263a8915782d2e1f03a9471d300ad1198d0ebdb Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Wed, 28 Jan 2026 21:49:52 -0800
Subject: [PATCH 6/9] reformat spec

---
 src/test/scala/chiselTests/LTLSpec.scala | 66 ++++++++++++------------
 1 file changed, 33 insertions(+), 33 deletions(-)

diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala
index 290ce07bfc3..f9aac0964f3 100644
--- a/src/test/scala/chiselTests/LTLSpec.scala
+++ b/src/test/scala/chiselTests/LTLSpec.scala
@@ -35,12 +35,12 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class DelaysMod extends RawModule {
     val a, b, c = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val s0: Sequence = a.delay(1)
-    val s1: Sequence = b.delayRange(2, 4)
-    val s2: Sequence = c.delayAtLeast(5)
-    val s3: Sequence = a ### b
-    val s4: Sequence = a ##* b
-    val s5: Sequence = a ##+ b
+    val s0:            Sequence = a.delay(1)
+    val s1:            Sequence = b.delayRange(2, 4)
+    val s2:            Sequence = c.delayAtLeast(5)
+    val s3:            Sequence = a ### b
+    val s4:            Sequence = a ##* b
+    val s5:            Sequence = a ##+ b
   }
   it should "support sequence delay operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new DelaysMod)
@@ -71,8 +71,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class ConcatMod extends RawModule {
     val a, b, c, d, e = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val s0: Sequence = a.concat(b)
-    val s1: Sequence = Sequence.concat(c, d, e) // (c concat d) concat e
+    val s0:            Sequence = a.concat(b)
+    val s1:            Sequence = Sequence.concat(c, d, e) // (c concat d) concat e
   }
   it should "support sequence concat operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new ConcatMod)
@@ -93,11 +93,11 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class RepeatMod extends RawModule {
     val a, b, c, d, e = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val s0: Sequence = a.repeat(1)
-    val s1: Sequence = b.repeatRange(2, 4)
-    val s2: Sequence = c.repeatAtLeast(5)
-    val s3: Sequence = d.gotoRepeat(1, 3)
-    val s4: Sequence = e.nonConsecutiveRepeat(1, 3)
+    val s0:            Sequence = a.repeat(1)
+    val s1:            Sequence = b.repeatRange(2, 4)
+    val s2:            Sequence = c.repeatAtLeast(5)
+    val s3:            Sequence = d.gotoRepeat(1, 3)
+    val s4:            Sequence = e.nonConsecutiveRepeat(1, 3)
   }
   it should "support sequence repeat operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new RepeatMod)
@@ -127,20 +127,20 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
     val a, b = IO(Input(Bool()))
     val clock = IO(Input(Clock()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val s0: Sequence = a.delay()
-    val s1: Sequence = s0.and(b)
-    val s2: Sequence = s0.or(b)
-    val si: Sequence = s0.intersect(b)
-    val sn: Sequence = Sequence.intersect(si, s1, s2)
-    val s3: Sequence = s0.clock(clock)
-    val p0: Property = a.eventually
-    val p1: Property = p0.and(b)
-    val p2: Property = p0.or(b)
-    val pi: Property = p0.intersect(b)
-    val pn: Property = Property.intersect(pi, p1, p2)
-    val p3: Property = p0.clock(clock)
-    val u1: Sequence = s0.until(b)
-    val u2: Property = p0.until(b)
+    val s0:            Sequence = a.delay()
+    val s1:            Sequence = s0.and(b)
+    val s2:            Sequence = s0.or(b)
+    val si:            Sequence = s0.intersect(b)
+    val sn:            Sequence = Sequence.intersect(si, s1, s2)
+    val s3:            Sequence = s0.clock(clock)
+    val p0:            Property = a.eventually
+    val p1:            Property = p0.and(b)
+    val p2:            Property = p0.or(b)
+    val pi:            Property = p0.intersect(b)
+    val pn:            Property = Property.intersect(pi, p1, p2)
+    val p3:            Property = p0.clock(clock)
+    val u1:            Sequence = s0.until(b)
+    val u2:            Property = p0.until(b)
   }
   it should "support and, or, intersect, and clock operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new AndOrClockMod)
@@ -187,7 +187,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class NotMod extends RawModule {
     val a = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val p0: Property = Property.not(a)
+    val p0:            Property = Property.not(a)
   }
   it should "support property not operation" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new NotMod)
@@ -201,10 +201,10 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class PropImplicationMod extends RawModule {
     val a, b = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val p0: Property = Property.implication(a, b)
-    val p1: Property = a |-> b
-    val p2: Property = Property.implicationNonOverlapping(a, b)
-    val p3: Property = a |=> b
+    val p0:            Property = Property.implication(a, b)
+    val p1:            Property = a |-> b
+    val p2:            Property = Property.implicationNonOverlapping(a, b)
+    val p3:            Property = a |=> b
   }
   it should "support property implication operation" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new PropImplicationMod)
@@ -237,7 +237,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class EventuallyMod extends RawModule {
     val a = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
-    val p0: Property = a.eventually
+    val p0:            Property = a.eventually
   }
   it should "support property eventually operation" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new EventuallyMod)

From 867e27b3d4898557395c259ab677aa70381a4279 Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Fri, 30 Jan 2026 14:22:51 -0800
Subject: [PATCH 7/9] Move implicit SourceInfos above prots in LTLSpec

I have no idea how this worked before...
---
 src/test/scala/chiselTests/LTLSpec.scala | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala
index f9aac0964f3..bcd9dc0c8f3 100644
--- a/src/test/scala/chiselTests/LTLSpec.scala
+++ b/src/test/scala/chiselTests/LTLSpec.scala
@@ -33,8 +33,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class DelaysMod extends RawModule {
-    val a, b, c = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a, b, c = IO(Input(Bool()))
     val s0:            Sequence = a.delay(1)
     val s1:            Sequence = b.delayRange(2, 4)
     val s2:            Sequence = c.delayAtLeast(5)
@@ -69,8 +69,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class ConcatMod extends RawModule {
-    val a, b, c, d, e = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a, b, c, d, e = IO(Input(Bool()))
     val s0:            Sequence = a.concat(b)
     val s1:            Sequence = Sequence.concat(c, d, e) // (c concat d) concat e
   }
@@ -91,8 +91,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class RepeatMod extends RawModule {
-    val a, b, c, d, e = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a, b, c, d, e = IO(Input(Bool()))
     val s0:            Sequence = a.repeat(1)
     val s1:            Sequence = b.repeatRange(2, 4)
     val s2:            Sequence = c.repeatAtLeast(5)
@@ -124,9 +124,9 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class AndOrClockMod extends RawModule {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b = IO(Input(Bool()))
     val clock = IO(Input(Clock()))
-    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val s0:            Sequence = a.delay()
     val s1:            Sequence = s0.and(b)
     val s2:            Sequence = s0.or(b)
@@ -185,8 +185,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class NotMod extends RawModule {
-    val a = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a = IO(Input(Bool()))
     val p0:            Property = Property.not(a)
   }
   it should "support property not operation" in {
@@ -199,8 +199,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class PropImplicationMod extends RawModule {
-    val a, b = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a, b = IO(Input(Bool()))
     val p0:            Property = Property.implication(a, b)
     val p1:            Property = a |-> b
     val p2:            Property = Property.implicationNonOverlapping(a, b)
@@ -235,8 +235,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class EventuallyMod extends RawModule {
-    val a = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a = IO(Input(Bool()))
     val p0:            Property = a.eventually
   }
   it should "support property eventually operation" in {
@@ -249,8 +249,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class BasicVerifMod extends RawModule {
-    val a = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a = IO(Input(Bool()))
     AssertProperty(a)
     AssumeProperty(a)
     CoverProperty(a)
@@ -281,6 +281,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
   it should "not create layer blocks if already in a layer block" in {
     class Foo extends RawModule {
+      implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
       val a = IO(Input(Bool()))
       layer.block(chisel3.layers.Verification.Cover) {
         AssertProperty(a)
@@ -304,8 +305,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
 
     for ((prop, (intrinsic, op)) <- properties) {
       val chirrtl = ChiselStage.emitCHIRRTL(new Module {
-        val a = IO(Input(Bool()))
         implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+        val a = IO(Input(Bool()))
         prop(a)
       })
       val sourceLoc = "@[Foo.scala 1:2]"
@@ -318,6 +319,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class LabeledVerifMod extends RawModule {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a = IO(Input(Bool()))
     AssertProperty(a, label = Some("foo0"))
     AssumeProperty(a, label = Some("foo1"))
@@ -360,8 +362,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class SequenceConvMod extends RawModule {
-    val a, b = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a, b = IO(Input(Bool()))
     AssertProperty(Sequence(a))
     AssertProperty(Sequence(a, b))
     AssertProperty(Sequence(Delay(), a))
@@ -428,8 +430,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   }
 
   class LayerBlockMod extends RawModule {
-    val a, b = IO(Input(Bool()))
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
+    val a, b = IO(Input(Bool()))
     AssertProperty(Sequence(Delay(), a))
     AssumeProperty(a |-> b)
   }

From e7ae1ab50ab623e8d2648c923dbe8941f7d3da31 Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Fri, 30 Jan 2026 14:50:24 -0800
Subject: [PATCH 8/9] reformat LTLSpecx

---
 src/test/scala/chiselTests/LTLSpec.scala | 66 ++++++++++++------------
 1 file changed, 33 insertions(+), 33 deletions(-)

diff --git a/src/test/scala/chiselTests/LTLSpec.scala b/src/test/scala/chiselTests/LTLSpec.scala
index bcd9dc0c8f3..69dcc55797b 100644
--- a/src/test/scala/chiselTests/LTLSpec.scala
+++ b/src/test/scala/chiselTests/LTLSpec.scala
@@ -35,12 +35,12 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class DelaysMod extends RawModule {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b, c = IO(Input(Bool()))
-    val s0:            Sequence = a.delay(1)
-    val s1:            Sequence = b.delayRange(2, 4)
-    val s2:            Sequence = c.delayAtLeast(5)
-    val s3:            Sequence = a ### b
-    val s4:            Sequence = a ##* b
-    val s5:            Sequence = a ##+ b
+    val s0: Sequence = a.delay(1)
+    val s1: Sequence = b.delayRange(2, 4)
+    val s2: Sequence = c.delayAtLeast(5)
+    val s3: Sequence = a ### b
+    val s4: Sequence = a ##* b
+    val s5: Sequence = a ##+ b
   }
   it should "support sequence delay operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new DelaysMod)
@@ -71,8 +71,8 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class ConcatMod extends RawModule {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b, c, d, e = IO(Input(Bool()))
-    val s0:            Sequence = a.concat(b)
-    val s1:            Sequence = Sequence.concat(c, d, e) // (c concat d) concat e
+    val s0: Sequence = a.concat(b)
+    val s1: Sequence = Sequence.concat(c, d, e) // (c concat d) concat e
   }
   it should "support sequence concat operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new ConcatMod)
@@ -93,11 +93,11 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class RepeatMod extends RawModule {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b, c, d, e = IO(Input(Bool()))
-    val s0:            Sequence = a.repeat(1)
-    val s1:            Sequence = b.repeatRange(2, 4)
-    val s2:            Sequence = c.repeatAtLeast(5)
-    val s3:            Sequence = d.gotoRepeat(1, 3)
-    val s4:            Sequence = e.nonConsecutiveRepeat(1, 3)
+    val s0: Sequence = a.repeat(1)
+    val s1: Sequence = b.repeatRange(2, 4)
+    val s2: Sequence = c.repeatAtLeast(5)
+    val s3: Sequence = d.gotoRepeat(1, 3)
+    val s4: Sequence = e.nonConsecutiveRepeat(1, 3)
   }
   it should "support sequence repeat operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new RepeatMod)
@@ -127,20 +127,20 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b = IO(Input(Bool()))
     val clock = IO(Input(Clock()))
-    val s0:            Sequence = a.delay()
-    val s1:            Sequence = s0.and(b)
-    val s2:            Sequence = s0.or(b)
-    val si:            Sequence = s0.intersect(b)
-    val sn:            Sequence = Sequence.intersect(si, s1, s2)
-    val s3:            Sequence = s0.clock(clock)
-    val p0:            Property = a.eventually
-    val p1:            Property = p0.and(b)
-    val p2:            Property = p0.or(b)
-    val pi:            Property = p0.intersect(b)
-    val pn:            Property = Property.intersect(pi, p1, p2)
-    val p3:            Property = p0.clock(clock)
-    val u1:            Sequence = s0.until(b)
-    val u2:            Property = p0.until(b)
+    val s0: Sequence = a.delay()
+    val s1: Sequence = s0.and(b)
+    val s2: Sequence = s0.or(b)
+    val si: Sequence = s0.intersect(b)
+    val sn: Sequence = Sequence.intersect(si, s1, s2)
+    val s3: Sequence = s0.clock(clock)
+    val p0: Property = a.eventually
+    val p1: Property = p0.and(b)
+    val p2: Property = p0.or(b)
+    val pi: Property = p0.intersect(b)
+    val pn: Property = Property.intersect(pi, p1, p2)
+    val p3: Property = p0.clock(clock)
+    val u1: Sequence = s0.until(b)
+    val u2: Property = p0.until(b)
   }
   it should "support and, or, intersect, and clock operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new AndOrClockMod)
@@ -187,7 +187,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class NotMod extends RawModule {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a = IO(Input(Bool()))
-    val p0:            Property = Property.not(a)
+    val p0: Property = Property.not(a)
   }
   it should "support property not operation" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new NotMod)
@@ -201,10 +201,10 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class PropImplicationMod extends RawModule {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b = IO(Input(Bool()))
-    val p0:            Property = Property.implication(a, b)
-    val p1:            Property = a |-> b
-    val p2:            Property = Property.implicationNonOverlapping(a, b)
-    val p3:            Property = a |=> b
+    val p0: Property = Property.implication(a, b)
+    val p1: Property = a |-> b
+    val p2: Property = Property.implicationNonOverlapping(a, b)
+    val p3: Property = a |=> b
   }
   it should "support property implication operation" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new PropImplicationMod)
@@ -237,7 +237,7 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselSim {
   class EventuallyMod extends RawModule {
     implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a = IO(Input(Bool()))
-    val p0:            Property = a.eventually
+    val p0: Property = a.eventually
   }
   it should "support property eventually operation" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new EventuallyMod)

From 67947ef2791e31ca61d0ee653bfdb6a76657687a Mon Sep 17 00:00:00 2001
From: Jack Koenig <koenig@sifive.com>
Date: Fri, 30 Jan 2026 14:50:28 -0800
Subject: [PATCH 9/9] Add MiMa waivers for sealed traits

---
 release.mill | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/release.mill b/release.mill
index 490ad1b2600..5125fc7e403 100644
--- a/release.mill
+++ b/release.mill
@@ -65,7 +65,11 @@ trait Unipublish extends ChiselCrossModule with ChiselPublishModule with Mima {
     // This is internal and unusable as it will attempt to instantiate classes that were removed long ago.
     ProblemFilter.exclude[MissingClassProblem]("chisel3.internal.RangeTransform*"),
     // No longer a FixedIOModule, now a FixedIORawModule
-    ProblemFilter.exclude[MissingTypesProblem]("chisel3.experimental.inlinetest.TestHarness")
+    ProblemFilter.exclude[MissingTypesProblem]("chisel3.experimental.inlinetest.TestHarness"),
+    // Property is a sealed trait
+    ProblemFilter.exclude[NewMixinForwarderProblem]("chisel3.ltl.Property.*"),
+    // Sequence is a sealed trait
+    ProblemFilter.exclude[NewMixinForwarderProblem]("chisel3.ltl.Sequence.*")
   )
 
   def pluginVersion = v.scalaCrossToVersion(crossScalaVersion)