From d40f5283ba4a3840c92c7cb54bfb1d37c189f90c Mon Sep 17 00:00:00 2001 From: liuyic00 Date: Sun, 19 May 2024 00:40:02 +0800 Subject: [PATCH] [LTL] Add repeat and until operators (#6989) --- docs/Dialects/LTL.md | 25 +++++++++-- .../circt/Dialect/FIRRTL/FIRRTLExpressions.td | 10 +++++ include/circt/Dialect/FIRRTL/FIRRTLVisitors.h | 11 +++-- include/circt/Dialect/LTL/LTLOps.td | 42 +++++++++++++++++++ include/circt/Dialect/LTL/LTLVisitors.h | 12 +++--- .../ExportVerilog/ExportVerilog.cpp | 37 ++++++++++++++++ lib/Conversion/FIRRTLToHW/LowerToHW.cpp | 13 ++++++ lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp | 27 ++++++++++++ lib/Dialect/LTL/LTLFolds.cpp | 15 ++++++- test/Conversion/ExportVerilog/verif.mlir | 28 +++++++++++++ test/Conversion/FIRRTLToHW/intrinsics.mlir | 8 ++++ test/Dialect/FIRRTL/lower-intrinsics.mlir | 7 ++++ test/Dialect/LTL/basic.mlir | 10 +++++ test/Dialect/LTL/canonicalization.mlir | 24 ++++++++--- 14 files changed, 251 insertions(+), 18 deletions(-) diff --git a/docs/Dialects/LTL.md b/docs/Dialects/LTL.md index aacdf8c90a83..a1d8dec33aa3 100644 --- a/docs/Dialects/LTL.md +++ b/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,7 +188,12 @@ 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. @@ -184,6 +201,8 @@ For a sequence u with a fixed length of 2, concatenation can be represented as * 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 diff --git a/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td b/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td index af0bf9088dac..13e9d816a5ee 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td +++ b/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:$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 diff --git a/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h b/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h index 5ec93f1b7ea6..cf734acae4ad 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLVisitors.h +++ b/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); diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td index 4405890ed4c5..bd0fcdf0f4e9 100644 --- a/include/circt/Dialect/LTL/LTLOps.td +++ b/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:$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); diff --git a/include/circt/Dialect/LTL/LTLVisitors.h b/include/circt/Dialect/LTL/LTLVisitors.h index 32df0fcdbba6..b0bc90633a3c 100644 --- a/include/circt/Dialect/LTL/LTLVisitors.h +++ b/include/circt/Dialect/LTL/LTLVisitors.h @@ -21,11 +21,11 @@ class Visitor { ResultType dispatchLTLVisitor(Operation *op, ExtraArgs... args) { auto *thisCast = static_cast(this); return TypeSwitch(op) - .template Case( - [&](auto op) -> ResultType { - return thisCast->visitLTL(op, args...); - }) + .template Case([&](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); diff --git a/lib/Conversion/ExportVerilog/ExportVerilog.cpp b/lib/Conversion/ExportVerilog/ExportVerilog.cpp index e9320ab632a6..2f39d39de8b2 100644 --- a/lib/Conversion/ExportVerilog/ExportVerilog.cpp +++ b/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); diff --git a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp index c36afa1ce1e8..93e24c2bb733 100644 --- a/lib/Conversion/FIRRTLToHW/LowerToHW.cpp +++ b/lib/Conversion/FIRRTLToHW/LowerToHW.cpp @@ -1618,8 +1618,10 @@ struct FIRRTLLowering : public FIRRTLVisitor { 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(op, getLoweredValue(op.getInput()), + op.getBaseAttr(), op.getMoreAttr()); +} + LogicalResult FIRRTLLowering::visitExpr(LTLNotIntrinsicOp op) { return setLoweringToLTL(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( + op, + ValueRange{getLoweredValue(op.getLhs()), getLoweredValue(op.getRhs())}); +} + LogicalResult FIRRTLLowering::visitExpr(LTLEventuallyIntrinsicOp op) { return setLoweringToLTL(op, getLoweredValue(op.getInput())); diff --git a/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp b/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp index 6903a3376ee6..466ee9e12d68 100644 --- a/lib/Dialect/FIRRTL/FIRRTLIntrinsics.cpp +++ b/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(0, 1) || + gi.sizedOutput(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("base")); + auto more = getI64Attr(gi.getParamValue("more")); + rewriter.replaceOpWithNewOp( + gi.op, gi.op.getResultTypes(), adaptor.getOperands()[0], base, more); + } +}; + class CirctLTLClockConverter : public IntrinsicOpConverter { public: @@ -593,6 +617,8 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings( "circt.ltl.concat", "circt_ltl_concat"); lowering.add>( "circt.ltl.implication", "circt_ltl_implication"); + lowering.add>("circt.ltl.until", + "circt_ltl_until"); lowering.add>( "circt.ltl.disable", "circt_ltl_disable"); lowering.add>("circt.ltl.not", @@ -601,6 +627,7 @@ void FIRRTLIntrinsicLoweringDialectInterface::populateIntrinsicLowerings( "circt.ltl.eventually", "circt_ltl_eventually"); lowering.add("circt.ltl.delay", "circt_ltl_delay"); + lowering.add("circt.ltl.repeat", "circt_ltl_repeat"); lowering.add("circt.ltl.clock", "circt_ltl_clock"); lowering.add>( diff --git a/lib/Dialect/LTL/LTLFolds.cpp b/lib/Dialect/LTL/LTLFolds.cpp index 55455463097c..d83d086bbc1d 100644 --- a/lib/Dialect/LTL/LTLFolds.cpp +++ b/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(getResult().getType())) + isa(getInput().getType())) return getInput(); return {}; @@ -91,6 +91,19 @@ void ConcatOp::getCanonicalizationPatterns(RewritePatternSet &results, results.add(results.getContext()); } +//===----------------------------------------------------------------------===// +// RepeatOp +//===----------------------------------------------------------------------===// + +OpFoldResult RepeatOp::fold(FoldAdaptor adaptor) { + // repeat(s, 1, 0) -> s + if (adaptor.getBase() == 1 && adaptor.getMore() == 0 && + isa(getInput().getType())) + return getInput(); + + return {}; +} + //===----------------------------------------------------------------------===// // DisableOp //===----------------------------------------------------------------------===// diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir index 48fff8e7306a..b35068592f24 100644 --- a/test/Conversion/ExportVerilog/verif.mlir +++ b/test/Conversion/ExportVerilog/verif.mlir @@ -107,6 +107,25 @@ hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) { verif.assert %g2 : !ltl.sequence verif.assert %g3 : !ltl.sequence + // CHECK: assert property (a[*0]); + %r0 = ltl.repeat %a, 0, 0 : i1 + verif.assert %r0 : !ltl.sequence + // CHECK: assert property (a[*4]); + %r1 = ltl.repeat %a, 4, 0 : i1 + verif.assert %r1 : !ltl.sequence + // CHECK: assert property (a[*5:6]); + %r2 = ltl.repeat %a, 5, 1 : i1 + verif.assert %r2 : !ltl.sequence + // CHECK: assert property (a[*7:$]); + %r3 = ltl.repeat %a, 7 : i1 + verif.assert %r3 : !ltl.sequence + // CHECK: assert property (a[*]); + %r4 = ltl.repeat %a, 0 : i1 + verif.assert %r4 : !ltl.sequence + // CHECK: assert property (a[+]); + %r5 = ltl.repeat %a, 1 : i1 + verif.assert %r5 : !ltl.sequence + // CHECK: assert property (@(posedge clk) a); // CHECK: assert property (@(negedge clk) a); // CHECK: assert property (@(edge clk) a); @@ -146,6 +165,10 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) { %i6 = ltl.implication %i5, %n0 : !ltl.sequence, !ltl.property verif.assert %i6 : !ltl.property + // CHECK: assert property (a until b); + %u0 = ltl.until %a, %b : i1, i1 + verif.assert %u0 : !ltl.property + // CHECK: assert property (s_eventually a); %e0 = ltl.eventually %a : i1 verif.assert %e0 : !ltl.property @@ -196,6 +219,11 @@ hw.module @Precedence(in %a: i1, in %b: i1) { %e2 = ltl.and %b, %e0 : i1, !ltl.property verif.assert %e1 : !ltl.property verif.assert %e2 : !ltl.property + + // CHECK: assert property ((a until b) and a); + %u0 = ltl.until %a, %b : i1, i1 + %u1 = ltl.and %u0, %a : !ltl.property, i1 + verif.assert %u1 : !ltl.property } // CHECK-LABEL: module SystemVerilogSpecExamples diff --git a/test/Conversion/FIRRTLToHW/intrinsics.mlir b/test/Conversion/FIRRTLToHW/intrinsics.mlir index 8b18481f9f27..5d61a6a6db6d 100644 --- a/test/Conversion/FIRRTLToHW/intrinsics.mlir +++ b/test/Conversion/FIRRTLToHW/intrinsics.mlir @@ -75,12 +75,20 @@ firrtl.circuit "Intrinsics" { // CHECK-NEXT: [[C0:%.+]] = ltl.concat [[D0]], [[L1]] : !ltl.sequence, !ltl.sequence %c0 = firrtl.int.ltl.concat %d0, %l1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK-NEXT: [[R0:%.+]] = ltl.repeat %a, 42 : i1 + // CHECK-NEXT: [[R1:%.+]] = ltl.repeat %b, 42, 1337 : i1 + %r0 = firrtl.int.ltl.repeat %a, 42 : (!firrtl.uint<1>) -> !firrtl.uint<1> + %r1 = firrtl.int.ltl.repeat %b, 42, 1337 : (!firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK-NEXT: [[N0:%.+]] = ltl.not [[C0]] : !ltl.sequence %n0 = firrtl.int.ltl.not %c0 : (!firrtl.uint<1>) -> !firrtl.uint<1> // CHECK-NEXT: [[I0:%.+]] = ltl.implication [[C0]], [[N0]] : !ltl.sequence, !ltl.property %i0 = firrtl.int.ltl.implication %c0, %n0 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK-NEXT: [[U0:%.+]] = ltl.until [[N0]], [[N0]] : !ltl.property, !ltl.property + %u0 = firrtl.int.ltl.until %n0, %n0 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK-NEXT: [[E0:%.+]] = ltl.eventually [[I0]] : !ltl.property %e0 = firrtl.int.ltl.eventually %i0 : (!firrtl.uint<1>) -> !firrtl.uint<1> diff --git a/test/Dialect/FIRRTL/lower-intrinsics.mlir b/test/Dialect/FIRRTL/lower-intrinsics.mlir index c1b0d2daf537..08d08f430e0e 100644 --- a/test/Dialect/FIRRTL/lower-intrinsics.mlir +++ b/test/Dialect/FIRRTL/lower-intrinsics.mlir @@ -55,13 +55,20 @@ firrtl.circuit "Foo" { firrtl.int.generic "circt_ltl_delay" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1> firrtl.int.generic "circt_ltl_delay" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK-NEXT: firrtl.int.ltl.repeat %in0, 42 : + // CHECK-NEXT: firrtl.int.ltl.repeat %in0, 42, 1337 : + firrtl.int.generic "circt_ltl_repeat" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1> + firrtl.int.generic "circt_ltl_repeat" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1> + // CHECK-NEXT: firrtl.int.ltl.concat %in0, %in1 : // CHECK-NEXT: firrtl.int.ltl.not %in0 : // CHECK-NEXT: firrtl.int.ltl.implication %in0, %in1 : + // CHECK-NEXT: firrtl.int.ltl.until %in0, %in1 : // CHECK-NEXT: firrtl.int.ltl.eventually %in0 : firrtl.int.generic "circt_ltl_concat" %in0, %in1: (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> firrtl.int.generic "circt_ltl_not" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1> firrtl.int.generic "circt_ltl_implication" %in0, %in1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> + firrtl.int.generic "circt_ltl_until" %in0, %in1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> firrtl.int.generic "circt_ltl_eventually" %in0 : (!firrtl.uint<1>) -> !firrtl.uint<1> // CHECK-NEXT: firrtl.int.ltl.clock %in0, %clk : diff --git a/test/Dialect/LTL/basic.mlir b/test/Dialect/LTL/basic.mlir index ab5eabc9c9b7..7fcdb7ba78eb 100644 --- a/test/Dialect/LTL/basic.mlir +++ b/test/Dialect/LTL/basic.mlir @@ -62,6 +62,13 @@ ltl.concat %s : !ltl.sequence ltl.concat %s, %s : !ltl.sequence, !ltl.sequence ltl.concat %s, %s, %s : !ltl.sequence, !ltl.sequence, !ltl.sequence +// CHECK: ltl.repeat {{%.+}}, 0 : !ltl.sequence +// CHECK: ltl.repeat {{%.+}}, 42 : !ltl.sequence +// CHECK: ltl.repeat {{%.+}}, 42, 1337 : !ltl.sequence +ltl.repeat %s, 0 : !ltl.sequence +ltl.repeat %s, 42 : !ltl.sequence +ltl.repeat %s, 42, 1337 : !ltl.sequence + //===----------------------------------------------------------------------===// // Properties //===----------------------------------------------------------------------===// @@ -76,6 +83,9 @@ ltl.not %p : !ltl.property // CHECK: ltl.implication {{%.+}}, {{%.+}} : !ltl.sequence, !ltl.property ltl.implication %s, %p : !ltl.sequence, !ltl.property +// CHECK: ltl.until {{%.+}}, {{%.+}} : !ltl.property, !ltl.property +ltl.until %p, %p : !ltl.property, !ltl.property + // CHECK: ltl.eventually {{%.+}} : i1 // CHECK: ltl.eventually {{%.+}} : !ltl.sequence // CHECK: ltl.eventually {{%.+}} : !ltl.property diff --git a/test/Dialect/LTL/canonicalization.mlir b/test/Dialect/LTL/canonicalization.mlir index 1f8e1e99a49b..704256f2c6b8 100644 --- a/test/Dialect/LTL/canonicalization.mlir +++ b/test/Dialect/LTL/canonicalization.mlir @@ -5,12 +5,16 @@ func.func private @Seq(%arg0: !ltl.sequence) func.func private @Prop(%arg0: !ltl.property) // CHECK-LABEL: @DelayFolds -func.func @DelayFolds(%arg0: !ltl.sequence) { - // TODO: This can't happen because the fold changes type, need to be able to cast i1 to sequence +func.func @DelayFolds(%arg0: !ltl.sequence, %arg1: i1) { // delay(s, 0, 0) -> s - // COM: CHECK-NEXT: call @Seq(%arg0) - //%0 = ltl.delay %arg0, 0, 0 : !ltl.sequence - //call @Seq(%0) : (!ltl.sequence) -> () + // delay(i, 0, 0) -> delay(i, 0, 0) + // CHECK-NEXT: ltl.delay %arg1, 0, 0 : i1 + // CHECK-NEXT: call @Seq(%arg0) + // CHECK-NEXT: call @Seq({{%.+}}) + %0 = ltl.delay %arg0, 0, 0 : !ltl.sequence + %n0 = ltl.delay %arg1, 0, 0 : i1 + call @Seq(%0) : (!ltl.sequence) -> () + call @Seq(%n0) : (!ltl.sequence) -> () // delay(delay(s, 1), 2) -> delay(s, 3) // CHECK-NEXT: ltl.delay %arg0, 3 : @@ -95,6 +99,16 @@ func.func @ConcatFolds(%arg0: !ltl.sequence, %arg1: !ltl.sequence, %arg2: !ltl.s return } +// CHECK-LABEL: @RepeatFolds +func.func @RepeatFolds(%arg0: !ltl.sequence) { + // repeat(s, 1, 0) -> s + // CHECK-NEXT: call @Seq(%arg0) + %0 = ltl.repeat %arg0, 1, 0: !ltl.sequence + call @Seq(%0) : (!ltl.sequence) -> () + + return +} + // CHECK-LABEL: @ClockingFolds func.func @ClockingFolds(%arg0: !ltl.property) { // disable(p, false) -> p