[LTL] Add support for new sequence and property ops (#4120)

Add support for `until`, `intersect`, `repeat`, `non_consecutive_repeat`, and `goto_repeat` property operations from SVA.

src/main/scala/chisel3/ltl/LTL.scala

@@ -60,12 +60,34 @@ sealed trait Sequence extends Property {
   /** See `Sequence.concat`. */
   def concat(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)
+
+  /** See `Sequence.repeatRange`. */
+  def repeatRange(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)
+
+  /** See `Sequence.gotoRepeat`. */
+  def gotoRepeat(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)
+
   /** See `Sequence.and`. */
   def and(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)
 
+  /** See `Sequence.intersect`. */
+  def intersect(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)
+
   /** See `Sequence.clock`. */
   override def clock(clock: Clock)(implicit sourceInfo: SourceInfo): Sequence = Sequence.clock(this, clock)
 
@@ -137,6 +159,50 @@ 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 = {
+    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 = {
+    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 = {
+    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 = {
+    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 = {
+    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.
     */
@@ -159,6 +225,25 @@ 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 = {
+    var lhs = arg0
+    for (rhs <- argN) {
+      lhs = OpaqueSequence(LTLIntersectIntrinsic(lhs.inner, rhs.inner))
+    }
+    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 =
+    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.
     */
@@ -209,6 +294,12 @@ sealed trait Property {
   /** See `Property.or`. */
   def or(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)
+
+  /** See `Property.until`. */
+  def until(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)
 
@@ -274,6 +365,25 @@ 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 = {
+    var lhs = arg0
+    for (rhs <- argN) {
+      lhs = OpaqueProperty(LTLIntersectIntrinsic(lhs.inner, rhs.inner))
+    }
+    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 =
+    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.
     */

src/main/scala/chisel3/util/circt/LTLIntrinsics.scala

@@ -65,18 +65,48 @@ private[chisel3] object LTLOrIntrinsic {
     BinaryLTLIntrinsic("or")(lhs, rhs)
 }
 
+/** A wrapper intrinsic for the CIRCT `ltl.intersect` operation. */
+private[chisel3] object LTLIntersectIntrinsic {
+  def apply(lhs: Bool, rhs: Bool)(implicit sourceInfo: SourceInfo) =
+    BinaryLTLIntrinsic("intersect")(lhs, rhs)
+}
+
+/** A wrapper intrinsic for the CIRCT `ltl.until` operation. */
+private[chisel3] object LTLUntilIntrinsic {
+  def apply(lhs: Bool, rhs: Bool)(implicit sourceInfo: SourceInfo) =
+    BinaryLTLIntrinsic("until")(lhs, rhs)
+}
+
 /** A wrapper intrinsic for the CIRCT `ltl.delay` operation. */
 private[chisel3] object LTLDelayIntrinsic {
 
   def apply(delay: Int, length: Option[Int])(_in: Bool)(implicit sourceInfo: SourceInfo) = {
-    val params = length match {
-      case None    => Seq("delay" -> IntParam(delay))
-      case Some(l) => Seq("delay" -> IntParam(delay), "length" -> IntParam(l))
-    }
+    val params = Seq("delay" -> IntParam(delay)) ++ length.map("length" -> IntParam(_))
     UnaryLTLIntrinsic("delay", params)(_in)
   }
 }
 
+/** A wrapper intrinsic for the CIRCT `ltl.repeat` operation. */
+private[chisel3] object LTLRepeatIntrinsic {
+
+  def apply(base: Int, more: Option[Int])(_in: Bool)(implicit sourceInfo: SourceInfo) = {
+    val params = Seq("base" -> IntParam(base)) ++ more.map("more" -> IntParam(_))
+    UnaryLTLIntrinsic("repeat", params)(_in)
+  }
+}
+
+/** A wrapper intrinsic for the CIRCT `ltl.goto_repeat` operation. */
+private[chisel3] object LTLGoToRepeatIntrinsic {
+  def apply(base: Int, more: Int)(_in: Bool)(implicit sourceInfo: SourceInfo) =
+    UnaryLTLIntrinsic("goto_repeat", Seq("base" -> IntParam(base), "more" -> IntParam(more)))(_in)
+}
+
+/** A wrapper intrinsic for the CIRCT `ltl.non_consecutive_repeat` operation. */
+private[chisel3] object LTLNonConsecutiveRepeatIntrinsic {
+  def apply(base: Int, more: Int)(_in: Bool)(implicit sourceInfo: SourceInfo) =
+    UnaryLTLIntrinsic("non_consecutive_repeat", Seq("base" -> IntParam(base), "more" -> IntParam(more)))(_in)
+}
+
 /** A wrapper intrinsic for the CIRCT `ltl.concat` operation. */
 private[chisel3] object LTLConcatIntrinsic {
   def apply(lhs: Bool, rhs: Bool)(implicit sourceInfo: SourceInfo) =

src/test/scala/chiselTests/LTLSpec.scala

@@ -85,36 +85,85 @@ class LTLSpec extends AnyFlatSpec with Matchers with ChiselRunners {
     ChiselStage.emitSystemVerilog(new ConcatMod)
   }
 
+  class RepeatMod extends RawModule {
+    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)
+    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)
+    val sourceLoc = "@[Foo.scala 1:2]"
+    chirrtl should include("input a : UInt<1>")
+    chirrtl should include("input b : UInt<1>")
+    chirrtl should include("input c : UInt<1>")
+    chirrtl should include("input d : UInt<1>")
+    chirrtl should include("input e : UInt<1>")
+    chirrtl should include(f"node repeat = intrinsic(circt_ltl_repeat<base = 1, more = 0> : UInt<1>, a) $sourceLoc")
+    chirrtl should include(f"node repeat_1 = intrinsic(circt_ltl_repeat<base = 2, more = 2> : UInt<1>, b) $sourceLoc")
+    chirrtl should include(f"node repeat_2 = intrinsic(circt_ltl_repeat<base = 5> : UInt<1>, c) $sourceLoc")
+    chirrtl should include(
+      f"node goto_repeat = intrinsic(circt_ltl_goto_repeat<base = 1, more = 2> : UInt<1>, d) $sourceLoc"
+    )
+    chirrtl should include(
+      f"node non_consecutive_repeat = intrinsic(circt_ltl_non_consecutive_repeat<base = 1, more = 2> : UInt<1>, e) $sourceLoc"
+    )
+  }
+  it should "compile sequence repeat operations" in {
+    ChiselStage.emitSystemVerilog(new RepeatMod)
+  }
+
   class AndOrClockMod extends RawModule {
     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)
+    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, and clock operations" in {
+  it should "support and, or, intersect, and clock operations" in {
     val chirrtl = ChiselStage.emitCHIRRTL(new AndOrClockMod)
     val sourceLoc = "@[Foo.scala 1:2]"
 
     // Sequences
     chirrtl should include(f"node delay = intrinsic(circt_ltl_delay<delay = 1, length = 0> : UInt<1>, a) $sourceLoc")
     chirrtl should include(f"node and = intrinsic(circt_ltl_and : UInt<1>, delay, b) $sourceLoc")
     chirrtl should include(f"node or = intrinsic(circt_ltl_or : UInt<1>, delay, b) $sourceLoc")
+    chirrtl should include(f"node intersect = intrinsic(circt_ltl_intersect : UInt<1>, delay, b) $sourceLoc")
+    chirrtl should include(f"node intersect_1 = intrinsic(circt_ltl_intersect : UInt<1>, intersect, and) $sourceLoc")
+    chirrtl should include(f"node intersect_2 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_1, or) $sourceLoc")
     chirrtl should include(f"node clock_1 = intrinsic(circt_ltl_clock : UInt<1>, delay, clock) $sourceLoc")
 
     // Properties
     chirrtl should include(f"node eventually = intrinsic(circt_ltl_eventually : UInt<1>, a) $sourceLoc")
     chirrtl should include(f"node and_1 = intrinsic(circt_ltl_and : UInt<1>, eventually, b) $sourceLoc")
     chirrtl should include(f"node or_1 = intrinsic(circt_ltl_or : UInt<1>, eventually, b) $sourceLoc")
+    chirrtl should include(f"node intersect_3 = intrinsic(circt_ltl_intersect : UInt<1>, eventually, b) $sourceLoc")
+    chirrtl should include(
+      f"node intersect_4 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_3, and_1) $sourceLoc"
+    )
+    chirrtl should include(f"node intersect_5 = intrinsic(circt_ltl_intersect : UInt<1>, intersect_4, or_1) $sourceLoc")
     chirrtl should include(f"node clock_2 = intrinsic(circt_ltl_clock : UInt<1>, eventually, clock) $sourceLoc")
+
+    // Until
+    chirrtl should include(f"node until = intrinsic(circt_ltl_until : UInt<1>, delay, b) $sourceLoc")
+    chirrtl should include(f"node until_1 = intrinsic(circt_ltl_until : UInt<1>, eventually, b) $sourceLoc")
   }
-  it should "compile and, or, and clock operations" in {
+  it should "compile and, or, intersect, and clock operations" in {
     ChiselStage.emitSystemVerilog(new AndOrClockMod)
   }