[LTL] Add repeat and until operators (#6989)

docs/Dialects/LTL.md

@@ -9,8 +9,6 @@ This dialect provides operations and types to model [Linear Temporal Logic](http
 
 The main goal of the `ltl` dialect is to capture the core formalism underpinning SystemVerilog Assertions (SVAs), the de facto standard for describing temporal logic sequences and properties in hardware verification. (See IEEE 1800-2017 section 16 "Assertions".) We expressly try *not* to model this dialect like an AST for SVAs, but instead try to strip away all the syntactic sugar and Verilog quirks, and distill out the core foundation as an IR. Within the CIRCT project, this dialect intends to enable emission of rich temporal assertions as part of the Verilog output, but also provide a foundation for formal tools built ontop of CIRCT.
 
-As a primary reference, the `ltl` dialect attempts to model SVAs after the [Linear Temporal Logic](https://en.wikipedia.org/wiki/Linear_temporal_logic) formalism as a way to distill SystemVerilog's syntactic sugar and quirks down to a core representation. However, most definitions of LTL tend to be rather academic in nature and may be lacking certain building blocks to make them useful in practice. (See section on [concatenation](#concatenation) below.) To inform some practical design decisions, the `ltl` dialect tries to think of temporal sequences as "regular expressions over time", borrowing from their wide applicability and usefulness.
-
 
 ### Sequences and Properties
 
@@ -30,6 +28,7 @@ The core building blocks for modeling temporal logic in the `ltl` dialect are *s
 
 - `always s` checks that the sequence `s` holds in every cycle. This is often referred to as the **G** (or "globally") operator in LTL.
 - `eventually s` checks that the sequence `s` will hold at some cycle now or in the future. This is often referred to as the **F** (or "finally") operator in LTL.
+- `p until q` checks that the property `p` holds in every cycle before the first cycle `q` holds. This is often referred to as the **U** (or "until") operator in LTL.
 - `s implies t` checks that whenever the sequence `s` is observed, it is immediately followed by sequence `t`.
 
 Traditional definitions of the LTL formalism do not make a distinction between sequences and properties. Most of their operators fall into the property category, for example, quantifiers like *globally*, *finally*, *release*, and *until*. The set of sequence operators is usually very small, since it is not necessary for academic treatment, consisting only of the *next* operator. The `ltl` dialect provides a richer set of operations to model sequences.
@@ -133,6 +132,19 @@ The `ltl.implication` op implements the overlapping case `|->`, such that the tw
 An important benefit of only modeling the overlapping `|->` implication operator is that it does not interact with a clock. The end point of the left-hand sequence is the starting point of the right-hand sequence. There is no notion of delay between the end of the left and the start of the right sequence. Compare this to the `|=>` operator in SVA, which implies that the right-hand sequence happens at "strictly the next clock tick", which requires the operator to have a notion of time and clocking. As described above, it is still possible to model this using an explicit `ltl.delay` op, which already has an established interaction with a clock.
 
 
+### Repetition
+
+Consecutive repetition repeats the sequence by a number of times. For example, `s[*3]` repeats the sequence `s` three times, which is equivalent to `s ##1 s ##1 s`. This also applies when the sequence `s` matches different traces with different lengths. For example `(##[0:3] a)[*2]` is equivalent to the disjunction of all the combinations such as `a ##1 a`, `a ##1 (##3 a)`, `(##3 a) ##1 (##2 a)`. However, the repetition with unbounded range cannot be expanded to the concatenations as it produces an infinite formula.
+
+The definition of `ltl.repeat` is similar to that of `ltl.delay`. The mapping from SVA's consecutive repetition to the LTL dialect is as follows:
+
+- `seq[*N]`. **Fixed repeat.** Repeats `N` times. Equivalent to `ltl.repeat %seq, N, 0`.
+- `seq[*N:M]`. **Bounded range repeat.** Repeats `N` to `M` times. Equivalent to `ltl.repeat %seq, N, (M-N)`.
+- `seq[*N:$]`. **Unbounded range repeat.** Repeats `N` to an indefinite finite number of times. Equivalent to `ltl.repeat %seq, N`.
+- `seq[*]`. Shorthand for `seq[*0:$]`. Equivalent to `ltl.repeat %seq, 0`.
+- `seq[+]`. Shorthand for `seq[*1:$]`. Equivalent to `ltl.repeat %seq, 1`.
+
+
 ### Clocking
 
 Sequence and property expressions in SVAs can specify a clock with respect to which all cycle delays are expressed. (See IEEE 1800-2017 section 16.16 "Clock resolution".) These map to the `ltl.clock` operation.
@@ -176,14 +188,21 @@ The `ltl.delay` sequence operation represents various shorthands for the *next*/
 | `ltl.delay %a, 2`    | **XXF**a                    |
 
 
-### Concatenation
+### Until and Eventually
+
+`ltl.until` is *weak*, meaning the property will hold even if the trace does not contain enough clock cycles to evaluate the property. `ltl.eventually` is *strong*, where `ltl.eventually %p` means `p` must hold at some point in the trace.
+
+
+### Concatenation and Repetition
 
 The `ltl.concat` sequence operation does not have a direct equivalent in LTL. It builds a longer sequence by composing multiple shorter sequences one after another. LTL has no concept of concatenation, or a *"v happens after u"*, where the point in time at which v starts is dependent on how long the sequence u was.
 
 For a sequence u with a fixed length of 2, concatenation can be represented as *"(u happens) and (v happens 2 cycles in the future)"*, u ∧ **XX**v. If u has a dynamic length though, for example a delay between 1 and 2, `ltl.delay %u, 1, 1` or **X**u ∨ **XX**u in LTL, there is no fixed number of cycles by which the sequence v can be delayed to make it start after u. Instead, all different-length variants of sequence u have to be enumerated and combined with a copy of sequence v delayed by the appropriate amount: (**X**u ∧ **XX**v) ∨ (**XX**u ∧ **XXX**v). This is basically saying "u delayed by 1 to 2 cycles followed by v" is the same as either *"u delayed by 1 cycle and v delayed by 2 cycles"*, or *"u delayed by 2 cycles and v delayed by 3 cycles"*.
 
 The *"v happens after u"* relationship is crucial to express sequences efficiently, which is why the LTL dialect has the `ltl.concat` op. If sequences are thought of as regular expressions over time, for example, `a(b|cd)` or *"a followed by either (b) or (c followed by d)"*, the importance of having a concatenation operation as temporal connective becomes apparent. Why LTL formalisms tend to not include such an operator is unclear.
 
+As for `ltl.repeat`, it also relies on the semantics of *v happens after u* to compose the repeated sequences. Unlike `ltl.concat`, which can be expanded by LTL operators within a finite formula size, unbounded repetition cannot be expanded by listing all cases. This means unbounded repetition imports semantics that LTL cannot describe. The LTL dialect has this operation because it is necessary and useful for regular expressions and SVA.
+
 
 ## Types
 

include/circt/Dialect/FIRRTL/FIRRTLExpressions.td

@@ -1429,10 +1429,20 @@ def LTLDelayIntrinsicOp : LTLIntrinsicOp<"delay"> {
   }];
 }
 def LTLConcatIntrinsicOp : BinaryLTLIntrinsicOp<"concat">;
+def LTLRepeatIntrinsicOp : LTLIntrinsicOp<"repeat"> {
+  let arguments = (ins UInt1Type:$input,
+                       I64Attr:$base,
+                       OptionalAttr<I64Attr>:$more);
+  let assemblyFormat = [{
+    $input `,` $base (`,` $more^)? attr-dict `:`
+    functional-type(operands, results)
+  }];
+}
 
 // Properties
 def LTLNotIntrinsicOp : UnaryLTLIntrinsicOp<"not">;
 def LTLImplicationIntrinsicOp : BinaryLTLIntrinsicOp<"implication">;
+def LTLUntilIntrinsicOp : BinaryLTLIntrinsicOp<"until">;
 def LTLEventuallyIntrinsicOp : UnaryLTLIntrinsicOp<"eventually">;
 
 // Clocking

include/circt/Dialect/FIRRTL/FIRRTLVisitors.h

@@ -50,10 +50,11 @@ class ExprVisitor {
             IsXIntrinsicOp, PlusArgsValueIntrinsicOp, PlusArgsTestIntrinsicOp,
             SizeOfIntrinsicOp, ClockGateIntrinsicOp, ClockInverterIntrinsicOp,
             ClockDividerIntrinsicOp, LTLAndIntrinsicOp, LTLOrIntrinsicOp,
-            LTLDelayIntrinsicOp, LTLConcatIntrinsicOp, LTLNotIntrinsicOp,
-            LTLImplicationIntrinsicOp, LTLEventuallyIntrinsicOp,
-            LTLClockIntrinsicOp, LTLDisableIntrinsicOp, Mux2CellIntrinsicOp,
-            Mux4CellIntrinsicOp, HasBeenResetIntrinsicOp,
+            LTLDelayIntrinsicOp, LTLConcatIntrinsicOp, LTLRepeatIntrinsicOp,
+            LTLNotIntrinsicOp, LTLImplicationIntrinsicOp, LTLUntilIntrinsicOp,
+            LTLEventuallyIntrinsicOp, LTLClockIntrinsicOp,
+            LTLDisableIntrinsicOp, Mux2CellIntrinsicOp, Mux4CellIntrinsicOp,
+            HasBeenResetIntrinsicOp,
             // Miscellaneous.
             BitsPrimOp, HeadPrimOp, MuxPrimOp, PadPrimOp, ShlPrimOp, ShrPrimOp,
             TailPrimOp, VerbatimExprOp, HWStructCastOp, BitCastOp, RefSendOp,
@@ -171,8 +172,10 @@ class ExprVisitor {
   HANDLE(LTLOrIntrinsicOp, Unhandled);
   HANDLE(LTLDelayIntrinsicOp, Unhandled);
   HANDLE(LTLConcatIntrinsicOp, Unhandled);
+  HANDLE(LTLRepeatIntrinsicOp, Unhandled);
   HANDLE(LTLNotIntrinsicOp, Unhandled);
   HANDLE(LTLImplicationIntrinsicOp, Unhandled);
+  HANDLE(LTLUntilIntrinsicOp, Unhandled);
   HANDLE(LTLEventuallyIntrinsicOp, Unhandled);
   HANDLE(LTLClockIntrinsicOp, Unhandled);
   HANDLE(LTLDisableIntrinsicOp, Unhandled);

include/circt/Dialect/LTL/LTLOps.td

@@ -151,6 +151,31 @@ def ConcatOp : LTLOp<"concat", [Pure]> {
   }];
 }
 
+def RepeatOp : LTLOp<"repeat", [Pure]> {
+  let arguments = (ins
+    LTLAnySequenceType:$input,
+    I64Attr:$base,
+    OptionalAttr<I64Attr>:$more);
+  let results = (outs LTLSequenceType:$result);
+  let assemblyFormat = [{
+    $input `,` $base (`,` $more^)? attr-dict `:` type($input)
+  }];
+  let hasFolder = 1;
+
+  let summary = "Repeats a sequence by a number of times.";
+  let description = [{
+    Repeat the `$input` sequence at least `$base` times, at most `$base` +
+    `$more` times. The number must be greater than or equal to zero. Omitting
+    `$more` indicates an unbounded but finite repetition. For example:
+
+    - `ltl.repeat %seq, 2, 0` repeats `%seq` exactly 2 times.
+    - `ltl.repeat %seq, 2, 2` repeats `%seq` 2, 3, or 4 times.
+    - `ltl.repeat %seq, 2` repeats `%seq` 2 or more times. The number of times
+      is unbounded but finite.
+    - `ltl.repeat %seq, 0, 0` represents an empty sequence.
+  }];
+}
+
 //===----------------------------------------------------------------------===//
 // Properties
 //===----------------------------------------------------------------------===//
@@ -191,6 +216,23 @@ def ImplicationOp : LTLOp<"implication", [Pure]> {
   }];
 }
 
+def UntilOp: LTLOp<"until", [Pure]> {
+  let arguments = (ins LTLAnyPropertyType:$input,
+                       LTLAnyPropertyType:$condition);
+  let results = (outs LTLPropertyType:$result);
+  let assemblyFormat = [{
+    operands attr-dict `:` type(operands)
+  }];
+
+  let summary = "Property always holds until another property holds.";
+  let description = [{
+    Checks that the `$input` property always holds until the `$condition`
+    property holds once. This operator is weak: the property will hold even if
+    `$input` always holds and `$condition` never holds. This operator is
+    nonoverlapping: `$input` does not have to hold when `$condition` holds.
+  }];
+}
+
 def EventuallyOp : LTLOp<"eventually", [Pure]> {
   let arguments = (ins LTLAnyPropertyType:$input);
   let results = (outs LTLPropertyType:$result);

include/circt/Dialect/LTL/LTLVisitors.h

@@ -21,11 +21,11 @@ class Visitor {
   ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args) {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
-        .template Case<AndOp, OrOp, DelayOp, ConcatOp, NotOp, ImplicationOp,
-                       EventuallyOp, ClockOp, DisableOp>(
-            [&](auto op) -> ResultType {
-              return thisCast->visitLTL(op, args...);
-            })
+        .template Case<AndOp, OrOp, DelayOp, ConcatOp, RepeatOp, NotOp,
+                       ImplicationOp, UntilOp, EventuallyOp, ClockOp,
+                       DisableOp>([&](auto op) -> ResultType {
+          return thisCast->visitLTL(op, args...);
+        })
         .Default([&](auto) -> ResultType {
           return thisCast->visitInvalidLTL(op, args...);
         });
@@ -52,8 +52,10 @@ class Visitor {
   HANDLE(OrOp, Unhandled);
   HANDLE(DelayOp, Unhandled);
   HANDLE(ConcatOp, Unhandled);
+  HANDLE(RepeatOp, Unhandled);
   HANDLE(NotOp, Unhandled);
   HANDLE(ImplicationOp, Unhandled);
+  HANDLE(UntilOp, Unhandled);
   HANDLE(EventuallyOp, Unhandled);
   HANDLE(ClockOp, Unhandled);
   HANDLE(DisableOp, Unhandled);

lib/Conversion/ExportVerilog/ExportVerilog.cpp

@@ -3410,8 +3410,10 @@ class PropertyEmitter : public EmitterBase,
   EmittedProperty visitLTL(ltl::OrOp op);
   EmittedProperty visitLTL(ltl::DelayOp op);
   EmittedProperty visitLTL(ltl::ConcatOp op);
+  EmittedProperty visitLTL(ltl::RepeatOp op);
   EmittedProperty visitLTL(ltl::NotOp op);
   EmittedProperty visitLTL(ltl::ImplicationOp op);
+  EmittedProperty visitLTL(ltl::UntilOp op);
   EmittedProperty visitLTL(ltl::EventuallyOp op);
   EmittedProperty visitLTL(ltl::ClockOp op);
   EmittedProperty visitLTL(ltl::DisableOp op);
@@ -3557,6 +3559,34 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ConcatOp op) {
   return {PropertyPrecedence::Concat};
 }
 
+EmittedProperty PropertyEmitter::visitLTL(ltl::RepeatOp op) {
+  emitNestedProperty(op.getInput(), PropertyPrecedence::Unary);
+  if (auto more = op.getMore()) {
+    if (*more == 0) {
+      ps << "[*";
+      ps.addAsString(op.getBase());
+      ps << "]";
+    } else {
+      ps << "[*";
+      ps.addAsString(op.getBase());
+      ps << ":";
+      ps.addAsString(op.getBase() + *more);
+      ps << "]";
+    }
+  } else {
+    if (op.getBase() == 0) {
+      ps << "[*]";
+    } else if (op.getBase() == 1) {
+      ps << "[+]";
+    } else {
+      ps << "[*";
+      ps.addAsString(op.getBase());
+      ps << ":$]";
+    }
+  }
+  return {PropertyPrecedence::Unary};
+}
+
 EmittedProperty PropertyEmitter::visitLTL(ltl::NotOp op) {
   ps << "not" << PP::space;
   emitNestedProperty(op.getInput(), PropertyPrecedence::Unary);
@@ -3592,6 +3622,13 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ImplicationOp op) {
   return {PropertyPrecedence::Implication};
 }
 
+EmittedProperty PropertyEmitter::visitLTL(ltl::UntilOp op) {
+  emitNestedProperty(op.getInput(), PropertyPrecedence::Until);
+  ps << PP::space << "until" << PP::space;
+  emitNestedProperty(op.getCondition(), PropertyPrecedence::Until);
+  return {PropertyPrecedence::Until};
+}
+
 EmittedProperty PropertyEmitter::visitLTL(ltl::EventuallyOp op) {
   ps << "s_eventually" << PP::space;
   emitNestedProperty(op.getInput(), PropertyPrecedence::Qualifier);

lib/Conversion/FIRRTLToHW/LowerToHW.cpp

@@ -1618,8 +1618,10 @@ struct FIRRTLLowering : public FIRRTLVisitor<FIRRTLLowering, LogicalResult> {
   LogicalResult visitExpr(LTLOrIntrinsicOp op);
   LogicalResult visitExpr(LTLDelayIntrinsicOp op);
   LogicalResult visitExpr(LTLConcatIntrinsicOp op);
+  LogicalResult visitExpr(LTLRepeatIntrinsicOp op);
   LogicalResult visitExpr(LTLNotIntrinsicOp op);
   LogicalResult visitExpr(LTLImplicationIntrinsicOp op);
+  LogicalResult visitExpr(LTLUntilIntrinsicOp op);
   LogicalResult visitExpr(LTLEventuallyIntrinsicOp op);
   LogicalResult visitExpr(LTLClockIntrinsicOp op);
   LogicalResult visitExpr(LTLDisableIntrinsicOp op);
@@ -3733,6 +3735,11 @@ LogicalResult FIRRTLLowering::visitExpr(LTLConcatIntrinsicOp op) {
       ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())});
 }
 
+LogicalResult FIRRTLLowering::visitExpr(LTLRepeatIntrinsicOp op) {
+  return setLoweringToLTL<ltl::RepeatOp>(op, getLoweredValue(op.getInput()),
+                                         op.getBaseAttr(), op.getMoreAttr());
+}
+
 LogicalResult FIRRTLLowering::visitExpr(LTLNotIntrinsicOp op) {
   return setLoweringToLTL<ltl::NotOp>(op, getLoweredValue(op.getInput()));
 }
@@ -3743,6 +3750,12 @@ LogicalResult FIRRTLLowering::visitExpr(LTLImplicationIntrinsicOp op) {
       ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())});
 }
 
+LogicalResult FIRRTLLowering::visitExpr(LTLUntilIntrinsicOp op) {
+  return setLoweringToLTL<ltl::UntilOp>(
+      op,
+      ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())});
+}
+
 LogicalResult FIRRTLLowering::visitExpr(LTLEventuallyIntrinsicOp op) {
   return setLoweringToLTL<ltl::EventuallyOp>(op,
                                              getLoweredValue(op.getInput()));

lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp

@@ -357,6 +357,30 @@ class CirctLTLDelayConverter : public IntrinsicConverter {
   }
 };
 
+class CirctLTLRepeatConverter : public IntrinsicConverter {
+public:
+  using IntrinsicConverter::IntrinsicConverter;
+
+  bool check(GenericIntrinsic gi) override {
+    return gi.hasNInputs(1) || gi.sizedInput<UIntType>(0, 1) ||
+           gi.sizedOutput<UIntType>(1) || gi.namedIntParam("base") ||
+           gi.namedIntParam("more", true) || gi.hasNParam(1, 1);
+  }
+
+  void convert(GenericIntrinsic gi, GenericIntrinsicOpAdaptor adaptor,
+               PatternRewriter &rewriter) override {
+    auto getI64Attr = [&](IntegerAttr val) {
+      if (!val)
+        return IntegerAttr();
+      return rewriter.getI64IntegerAttr(val.getValue().getZExtValue());
+    };
+    auto base = getI64Attr(gi.getParamValue<IntegerAttr>("base"));
+    auto more = getI64Attr(gi.getParamValue<IntegerAttr>("more"));
+    rewriter.replaceOpWithNewOp<LTLRepeatIntrinsicOp>(
+        gi.op, gi.op.getResultTypes(), adaptor.getOperands()[0], base, more);
+  }
+};
+
 class CirctLTLClockConverter
     : public IntrinsicOpConverter<LTLClockIntrinsicOp> {
 public:
@@ -593,6 +617,8 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings(
       "circt.ltl.concat", "circt_ltl_concat");
   lowering.add<CirctLTLBinaryConverter<LTLImplicationIntrinsicOp>>(
       "circt.ltl.implication", "circt_ltl_implication");
+  lowering.add<CirctLTLBinaryConverter<LTLUntilIntrinsicOp>>("circt.ltl.until",
+                                                             "circt_ltl_until");
   lowering.add<CirctLTLBinaryConverter<LTLDisableIntrinsicOp>>(
       "circt.ltl.disable", "circt_ltl_disable");
   lowering.add<CirctLTLUnaryConverter<LTLNotIntrinsicOp>>("circt.ltl.not",
@@ -601,6 +627,7 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings(
       "circt.ltl.eventually", "circt_ltl_eventually");
 
   lowering.add<CirctLTLDelayConverter>("circt.ltl.delay", "circt_ltl_delay");
+  lowering.add<CirctLTLRepeatConverter>("circt.ltl.repeat", "circt_ltl_repeat");
   lowering.add<CirctLTLClockConverter>("circt.ltl.clock", "circt_ltl_clock");
 
   lowering.add<CirctVerifConverter<VerifAssertIntrinsicOp>>(

lib/Dialect/LTL/LTLFolds.cpp

@@ -62,7 +62,7 @@ namespace patterns {
 OpFoldResult DelayOp::fold(FoldAdaptor adaptor) {
   // delay(s, 0, 0) -> s
   if (adaptor.getDelay() == 0 && adaptor.getLength() == 0 &&
-      !isa<SequenceType>(getResult().getType()))
+      isa<SequenceType>(getInput().getType()))
     return getInput();
 
   return {};
@@ -91,6 +91,19 @@ void ConcatOp::getCanonicalizationPatterns(RewritePatternSet &results,
   results.add<patterns::FlattenConcats>(results.getContext());
 }
 
+//===----------------------------------------------------------------------===//
+// RepeatOp
+//===----------------------------------------------------------------------===//
+
+OpFoldResult RepeatOp::fold(FoldAdaptor adaptor) {
+  // repeat(s, 1, 0) -> s
+  if (adaptor.getBase() == 1 && adaptor.getMore() == 0 &&
+      isa<SequenceType>(getInput().getType()))
+    return getInput();
+
+  return {};
+}
+
 //===----------------------------------------------------------------------===//
 // DisableOp
 //===----------------------------------------------------------------------===//