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)
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..d1c1ffda6cb
--- /dev/null
+++ b/src/main/scala-2/chisel3/ltl/LTLIntf.scala
@@ -0,0 +1,311 @@
+// 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. 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. 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. Equivalent to
+    * `##[delay:$]` in SVA.
+    */
+  def delayAtLeast(seq: Sequence, delay: Int)(implicit sourceInfo: SourceInfo): Sequence = _delayAtLeast(seq, delay)
+
+  /** 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. 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. 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. 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 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,
+    * 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. 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. 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 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 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 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. 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. Equivalent to `not prop` in SVA. */
+  def not(prop: Property)(implicit sourceInfo: SourceInfo): Property = _not(prop)
+
+  /** 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 `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 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. 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. 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 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 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 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,
+    disable: Option[Disable] = Module.disableOption,
+    label:   Option[String] = None
+  )(
+    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,
+    disable: Disable,
+    label:   String
+  )(
+    implicit sourceInfo: SourceInfo
+  ): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
+}
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..5d2e625b2c9
--- /dev/null
+++ b/src/main/scala-3/chisel3/ltl/LTLIntf.scala
@@ -0,0 +1,307 @@
+// 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. 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. 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. Equivalent to
+    * `##[delay:$]` in SVA.
+    */
+  def delayAtLeast(seq: Sequence, delay: Int)(using SourceInfo): Sequence = _delayAtLeast(seq, delay)
+
+  /** 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. 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. 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. Equivalent to
+    * `s[n:$]` in SVA.
+    */
+  def repeatAtLeast(seq: Sequence, n: Int)(using SourceInfo): Sequence = _repeatAtLeast(seq, n)
+
+  /** 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,
+    * 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. 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. Equivalent to
+    * `arg0 or arg1 or ... or argN` in SVA.
+    */
+  def or(arg0: Sequence, argN: Sequence*)(using SourceInfo): Sequence = _or(arg0, argN: _*)
+
+  /** 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 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 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. 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. Equivalent to `not prop` in SVA. */
+  def not(prop: Property)(using SourceInfo): Property = _not(prop)
+
+  /** 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 `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 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. 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. Equivalent to
+    * `arg0 or arg1 or ... or argN` in SVA.
+    */
+  def or(arg0: Property, argN: Property*)(using SourceInfo): Property = _or(arg0, argN: _*)
+
+  /** 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 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 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,
+    disable: Option[Disable] = Module.disableOption,
+    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,
+    disable: Disable,
+    label:   String
+  )(using SourceInfo): Unit = _applyCondClockDisableLabelImpl(cond, clock, disable, label)
+}
diff --git a/src/main/scala/chisel3/ltl/LTL.scala b/src/main/scala/chisel3/ltl/LTL.scala
index a663ae4d2ee..bd65d1ab413 100644
--- a/src/main/scala/chisel3/ltl/LTL.scala
+++ b/src/main/scala/chisel3/ltl/LTL.scala
@@ -46,74 +46,64 @@ 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,37 +111,22 @@ 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`.
-    */
   implicit class BoolSequence(val inner: Bool) extends Sequence with SequenceAtom
 
-  /** 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))
   }
 
-  /** 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))
@@ -159,54 +134,32 @@ object Sequence {
     lhs
   }
 
-  /** 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))
   }
 
-  /** 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))
   }
 
-  /** 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))
   }
 
-  /** 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 = {
+  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.
-    */
-  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))
   }
 
-  /** 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))
@@ -214,10 +167,7 @@ object Sequence {
     lhs
   }
 
-  /** 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))
@@ -225,11 +175,7 @@ object Sequence {
     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.
-    */
-  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))
@@ -237,36 +183,23 @@ object Sequence {
     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.
-    */
-  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:
-    *
-    * `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 = {
+  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,33 +208,28 @@ 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.
     */
   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,41 +237,23 @@ 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.
-    * 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 =
+  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))
@@ -351,10 +261,7 @@ object Property {
     lhs
   }
 
-  /** 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))
@@ -362,11 +269,7 @@ object Property {
     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.
-    */
-  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))
@@ -374,39 +277,19 @@ object Property {
     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.
-    */
-  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) {
-
-  /** 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(
+sealed abstract class AssertPropertyLike(defaultLayer: Layer) extends AssertPropertyLikeIntf {
+
+  protected def _applyImpl(
     prop:    => Property,
     clock:   Option[Clock] = Module.clockOption,
     disable: Option[Disable] = Module.disableOption,
@@ -419,12 +302,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     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.
-    */
-  def apply(
+  protected def _applyCondImpl(
     cond: Bool
   )(
     implicit sourceInfo: SourceInfo
@@ -432,15 +310,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     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.
-    */
-  def apply(
+  protected def _applyCondLabelImpl(
     cond:  Bool,
     label: String
   )(
@@ -449,21 +319,7 @@ sealed abstract class AssertPropertyLike(defaultLayer: Layer) {
     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.
-    */
-  def apply(
+  protected def _applyCondClockDisableLabelImpl(
     cond:    Bool,
     clock:   Clock,
     disable: Disable,
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..69dcc55797b 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
@@ -33,8 +33,8 @@ 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()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b, c, d, e = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b, c, d, e = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 = 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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     AssertProperty(a)
     AssumeProperty(a)
     CoverProperty(a)
@@ -281,8 +281,9 @@ 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(layers.Verification.Cover) {
+      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 {
+        implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
         val a = IO(Input(Bool()))
-        implicit val info = SourceLine("Foo.scala", 1, 2)
         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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     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 {
+    implicit val info: SourceInfo = SourceLine("Foo.scala", 1, 2)
     val a, b = IO(Input(Bool()))
-    implicit val info = SourceLine("Foo.scala", 1, 2)
     AssertProperty(Sequence(Delay(), a))
     AssumeProperty(a |-> b)
   }