diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td index 4405890ed4c5..1fcc80248e4c 100644 --- a/include/circt/Dialect/LTL/LTLOps.td +++ b/include/circt/Dialect/LTL/LTLOps.td @@ -53,7 +53,9 @@ def OrOp : AssocLTLOp<"or"> { // Sequences //===----------------------------------------------------------------------===// -def DelayOp : LTLOp<"delay", [Pure]> { +def DelayOp : LTLOp<"delay", [ + Pure, InferTypeOpInterface, DeclareOpInterfaceMethods +]> { let arguments = (ins LTLAnySequenceType:$input, I64Attr:$delay, @@ -92,9 +94,11 @@ def DelayOp : LTLOp<"delay", [Pure]> { }]; } -def ConcatOp : LTLOp<"concat", [Pure]> { - let arguments = (ins Variadic:$inputs); - let results = (outs LTLSequenceType:$result); +def ConcatOp : LTLOp<"concat", [ + Pure, InferTypeOpInterface, DeclareOpInterfaceMethods +]> { + let arguments = (ins Variadic:$inputs); + let results = (outs LTLAnyPropertyType:$result); let assemblyFormat = [{ $inputs attr-dict `:` type($inputs) }]; @@ -155,7 +159,9 @@ def ConcatOp : LTLOp<"concat", [Pure]> { // Properties //===----------------------------------------------------------------------===// -def NotOp : LTLOp<"not", [Pure]> { +def NotOp : LTLOp<"not", [ + Pure, InferTypeOpInterface, DeclareOpInterfaceMethods +]> { let arguments = (ins LTLAnyPropertyType:$input); let results = (outs LTLPropertyType:$result); let assemblyFormat = [{ @@ -170,7 +176,9 @@ def NotOp : LTLOp<"not", [Pure]> { }]; } -def ImplicationOp : LTLOp<"implication", [Pure]> { +def ImplicationOp : LTLOp<"implication", [ + Pure, InferTypeOpInterface, DeclareOpInterfaceMethods +]> { let arguments = (ins LTLAnySequenceType:$antecedent, LTLAnyPropertyType:$consequent); let results = (outs LTLPropertyType:$result); @@ -191,7 +199,9 @@ def ImplicationOp : LTLOp<"implication", [Pure]> { }]; } -def EventuallyOp : LTLOp<"eventually", [Pure]> { +def EventuallyOp : LTLOp<"eventually", [ + Pure, InferTypeOpInterface, DeclareOpInterfaceMethods +]> { let arguments = (ins LTLAnyPropertyType:$input); let results = (outs LTLPropertyType:$result); let assemblyFormat = [{ @@ -229,7 +239,7 @@ def ClockOp : LTLOp<"clock", [ Pure, InferTypeOpInterface, DeclareOpInterfaceMethods ]> { let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock); - let results = (outs LTLSequenceOrPropertyType:$result); + let results = (outs LTLAnyClockedType:$result); let assemblyFormat = [{ $input `,` $edge $clock attr-dict `:` type($input) }]; @@ -248,9 +258,11 @@ def ClockOp : LTLOp<"clock", [ }]; } -def DisableOp : LTLOp<"disable", [Pure]> { - let arguments = (ins LTLAnyPropertyType:$input, I1:$condition); - let results = (outs LTLPropertyType:$result); +def DisableOp : LTLOp<"disable", [ + Pure, InferTypeOpInterface, DeclareOpInterfaceMethods +]> { + let arguments = (ins LTLAnyNonDisabledPropertyType:$input, I1:$condition); + let results = (outs LTLDisabledPropertyType:$result); let assemblyFormat = [{ $input `if` $condition attr-dict `:` type($input) }]; @@ -264,7 +276,10 @@ def DisableOp : LTLOp<"disable", [Pure]> { `$input`, the resulting property is disabled. The disabling is "infectious". If a property is disabled, it also implicitly - disables all properties that use it. Consider the following example: + disables all properties that use it. Note that only one disbale can be associated + to a given property. + + Consider the following example: ``` %0 = ltl.disable %prop if %cond %1 = ltl.or %0, %otherProp diff --git a/include/circt/Dialect/LTL/LTLTypes.h b/include/circt/Dialect/LTL/LTLTypes.h index 514377b0e597..716988f689df 100644 --- a/include/circt/Dialect/LTL/LTLTypes.h +++ b/include/circt/Dialect/LTL/LTLTypes.h @@ -15,4 +15,28 @@ #define GET_TYPEDEF_CLASSES #include "circt/Dialect/LTL/LTLTypes.h.inc" +namespace circt { +namespace ltl { +/// Return true if the specified type is a clocked ltl type. This checks +/// that it is either an ltl.clocked_property, an ltl.clocked_sequence or an +/// ltl.clocked_disabled_property. +bool isClocked(mlir::Type type); + +/// Return true if the specified type is a disabled ltl type. This checks +/// that it is either an ltl.disabled_property, or an +/// ltl.clocked_disabled_property. +bool isDisabled(mlir::Type type); + +/// Return true if the specified type is a property ltl type. This checks +/// that it is either an ltl.clocked_property, an ltl.disabled_property, an +/// ltl.clocked_disabled_property, or an ltl.property. +bool isProperty(mlir::Type type); + +/// Return true if the specified type is a sequence ltl type. This checks +/// that it is either an ltl.sequence, or an ltl.clocked_sequence. +bool isSequence(mlir::Type type); + +} // namespace ltl +} // namespace circt + #endif // CIRCT_DIALECT_LTL_LTLTYPES_H diff --git a/include/circt/Dialect/LTL/LTLTypes.td b/include/circt/Dialect/LTL/LTLTypes.td index 194849f37c51..10fa630fd759 100644 --- a/include/circt/Dialect/LTL/LTLTypes.td +++ b/include/circt/Dialect/LTL/LTLTypes.td @@ -28,6 +28,19 @@ def LTLSequenceType : LTLTypeDef<"Sequence", "sequence"> { }]; } +def LTLClockedSequenceType : LTLTypeDef<"ClockedSequence", "clocked_sequence"> { + let summary = "LTL clocked sequence type"; + let description = [{ + The `ltl.clocked_sequence` type represents a sequence of linear temporal logic, + associated to a specific clock for example, *"A is true two cycles after B is true"*. + + Note that this type explicitly identifies a *clocked sequence*, i.e., a boolean + value (`i1`), or the result of a delay or concatenation, associated to a clock. + Operations that accept a sequence as an operand will use the `AnySequence` constraint, + which also accepts `i1`. + }]; +} + def LTLPropertyType : LTLTypeDef<"Property", "property"> { let summary = "LTL property type"; let description = [{ @@ -42,8 +55,48 @@ def LTLPropertyType : LTLTypeDef<"Property", "property"> { }]; } -def LTLAnySequenceType : AnyTypeOf<[I1, LTLSequenceType]>; -def LTLAnyPropertyType : AnyTypeOf<[I1, LTLSequenceType, LTLPropertyType]>; -def LTLSequenceOrPropertyType : AnyTypeOf<[LTLSequenceType, LTLPropertyType]>; +def LTLDisabledPropertyType : LTLTypeDef<"DisabledProperty", "disabled_property"> { + let summary = "LTL disabled property type"; + let description = [{ + The `ltl.disabled_property` type represents a verifiable property built from linear + temporal logic sequences and quantifiers that has explicitly been given a disable condition, + for example, *"if you see sequence A, eventually you will see sequence B unless D holds"*. + + Note that this type explicitly identifies a *disabled property*, i.e. any `i1`, + `ltl.sequence` or `ltl.property` that was disabled using `ltl.disable`. + }]; +} + +def LTLClockedPropertyType : LTLTypeDef<"ClockedProperty", "clocked_property"> { + let summary = "LTL clocked property type"; + let description = [{ + The `ltl.clocked_property` type represents a verifiable property built from linear + temporal logic sequences and quantifiers that has explicitly been associated to a clock signal. + + Note that this type explicitly identifies a *clocked property*, i.e. any `i1`, + `ltl.sequence` or `ltl.property` that was tied to a clock using `ltl.clock`. + }]; +} + +def LTLClockedDisabledPropertyType : LTLTypeDef<"ClockedDisabledProperty", "clocked_disabled_property"> { + let summary = "LTL clocked and disabled property type"; + let description = [{ + The `ltl.clocked_disabled_property` type represents a verifiable property built from linear + temporal logic sequences and quantifiers that has explicitly been associated to a clock signal and + and has a disable condition. + + Note that this type explicitly identifies a *clocked property*, i.e. any `i1`, + `ltl.sequence` or `ltl.property` that was tied to a clock using `ltl.clock` and + given a disable condition using `ltl.disable`. + }]; +} + +def LTLAnySequenceType : AnyTypeOf<[I1, LTLSequenceType, LTLClockedSequenceType]>; +def LTLAnyPropertyType : AnyTypeOf<[I1, LTLSequenceType, LTLClockedSequenceType, LTLPropertyType, + LTLDisabledPropertyType, LTLClockedPropertyType, LTLClockedDisabledPropertyType]>; +def LTLAnyPurePropertyType : AnyTypeOf<[I1, LTLSequenceType, LTLPropertyType]>; +def LTLAnyNonDisabledPropertyType : AnyTypeOf<[I1, LTLSequenceType, LTLClockedSequenceType, + LTLPropertyType, LTLClockedPropertyType]>; +def LTLAnyClockedType : AnyTypeOf<[LTLClockedSequenceType, LTLClockedPropertyType, LTLClockedDisabledPropertyType]>; #endif // CIRCT_DIALECT_LTL_LTLTYPES_TD diff --git a/lib/Dialect/LTL/CMakeLists.txt b/lib/Dialect/LTL/CMakeLists.txt index 466fe64433b8..31a91664a8af 100644 --- a/lib/Dialect/LTL/CMakeLists.txt +++ b/lib/Dialect/LTL/CMakeLists.txt @@ -2,6 +2,7 @@ add_circt_dialect_library(CIRCTLTL LTLDialect.cpp LTLFolds.cpp LTLOps.cpp + LTLTypes.cpp ADDITIONAL_HEADER_DIRS ${CIRCT_MAIN_INCLUDE_DIR}/circt/Dialect/LTL diff --git a/lib/Dialect/LTL/LTLOps.cpp b/lib/Dialect/LTL/LTLOps.cpp index c9d335e7f00a..d97e9145b65e 100644 --- a/lib/Dialect/LTL/LTLOps.cpp +++ b/lib/Dialect/LTL/LTLOps.cpp @@ -23,29 +23,140 @@ using namespace mlir; #include "circt/Dialect/LTL/LTL.cpp.inc" //===----------------------------------------------------------------------===// -// AndOp / OrOp +// ClockOp / DisableOp //===----------------------------------------------------------------------===// -static LogicalResult inferAndLikeReturnTypes(MLIRContext *context, - ValueRange operands, - SmallVectorImpl &results) { - if (llvm::any_of(operands, [](auto operand) { - return isa(operand.getType()); - })) { - results.push_back(PropertyType::get(context)); +LogicalResult +ClockOp::inferReturnTypes(MLIRContext *context, std::optional loc, + ValueRange operands, DictionaryAttr attributes, + OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + auto type = operands[0].getType(); + + if (isa(type)) { + inferredReturnTypes.push_back(ClockedSequenceType::get(context)); + } else if (isa(type)) { + inferredReturnTypes.push_back(ClockedPropertyType::get(context)); + } else if (isa(type)) { + inferredReturnTypes.push_back(ClockedDisabledPropertyType::get(context)); + } else { + inferredReturnTypes.push_back(ClockedSequenceType::get(context)); + } + return success(); +} + +LogicalResult +DisableOp::inferReturnTypes(MLIRContext *context, std::optional loc, + ValueRange operands, DictionaryAttr attributes, + OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + auto type = operands[0].getType(); + if (isa(type) || isa(type)) { + inferredReturnTypes.push_back(DisabledPropertyType::get(context)); + } else if (isa(type)) { + inferredReturnTypes.push_back(ClockedDisabledPropertyType::get(context)); + } else if (isa(type)) { + inferredReturnTypes.push_back(ClockedDisabledPropertyType::get(context)); } else { + inferredReturnTypes.push_back(DisabledPropertyType::get(context)); + } + return success(); +} + +//===----------------------------------------------------------------------===// +// Property and Sequence logical ops +//===----------------------------------------------------------------------===// + +static LogicalResult +inferPropertyLikeReturnTypes(MLIRContext *context, ValueRange operands, + SmallVectorImpl &results) { + bool clocked = llvm::any_of( + operands, [](auto operand) { return isClocked(operand.getType()); }); + bool disabled = llvm::any_of( + operands, [](auto operand) { return isDisabled(operand.getType()); }); + + if (clocked) { + if (disabled) { + results.push_back(ClockedDisabledPropertyType::get(context)); + } else { + results.push_back(ClockedPropertyType::get(context)); + } + + } else { + if (disabled) { + results.push_back(DisabledPropertyType::get(context)); + } else { + results.push_back(PropertyType::get(context)); + } + } + return success(); +} + +static LogicalResult +inferSequenceLikeReturnTypes(MLIRContext *context, ValueRange operands, + SmallVectorImpl &results) { + bool clocked = llvm::any_of( + operands, [](auto operand) { return isClocked(operand.getType()); }); + bool disabled = llvm::any_of( + operands, [](auto operand) { return isDisabled(operand.getType()); }); + bool prop = llvm::any_of( + operands, [](auto operand) { return isProperty(operand.getType()); }); + + if (clocked) { + if (disabled) { + results.push_back(ClockedDisabledPropertyType::get(context)); + } else { + if (prop) { + results.push_back(ClockedPropertyType::get(context)); + } else { + results.push_back(ClockedSequenceType::get(context)); + } + } - results.push_back(SequenceType::get(context)); + } else { + if (disabled) { + results.push_back(DisabledPropertyType::get(context)); + } else { + if (prop) { + results.push_back(PropertyType::get(context)); + } else { + results.push_back(SequenceType::get(context)); + } + } } return success(); } +LogicalResult +DelayOp::inferReturnTypes(MLIRContext *context, std::optional loc, + ValueRange operands, DictionaryAttr attributes, + OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + return inferSequenceLikeReturnTypes(context, operands, inferredReturnTypes); +} + +LogicalResult +ConcatOp::inferReturnTypes(MLIRContext *context, std::optional loc, + ValueRange operands, DictionaryAttr attributes, + OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + return inferSequenceLikeReturnTypes(context, operands, inferredReturnTypes); +} + +LogicalResult +NotOp::inferReturnTypes(MLIRContext *context, std::optional loc, + ValueRange operands, DictionaryAttr attributes, + OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes); +} + LogicalResult AndOp::inferReturnTypes(MLIRContext *context, std::optional loc, ValueRange operands, DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions, SmallVectorImpl &inferredReturnTypes) { - return inferAndLikeReturnTypes(context, operands, inferredReturnTypes); + return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes); } LogicalResult @@ -53,22 +164,19 @@ OrOp::inferReturnTypes(MLIRContext *context, std::optional loc, ValueRange operands, DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions, SmallVectorImpl &inferredReturnTypes) { - return inferAndLikeReturnTypes(context, operands, inferredReturnTypes); + return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes); } -//===----------------------------------------------------------------------===// -// ClockOp -//===----------------------------------------------------------------------===// +LogicalResult ImplicationOp::inferReturnTypes( + MLIRContext *context, std::optional loc, ValueRange operands, + DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes); +} -LogicalResult -ClockOp::inferReturnTypes(MLIRContext *context, std::optional loc, - ValueRange operands, DictionaryAttr attributes, - OpaqueProperties properties, RegionRange regions, - SmallVectorImpl &inferredReturnTypes) { - if (isa(operands[0].getType())) { - inferredReturnTypes.push_back(PropertyType::get(context)); - } else { - inferredReturnTypes.push_back(SequenceType::get(context)); - } - return success(); +LogicalResult EventuallyOp::inferReturnTypes( + MLIRContext *context, std::optional loc, ValueRange operands, + DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions, + SmallVectorImpl &inferredReturnTypes) { + return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes); } diff --git a/lib/Dialect/LTL/LTLTypes.cpp b/lib/Dialect/LTL/LTLTypes.cpp new file mode 100644 index 000000000000..9aec69383d1f --- /dev/null +++ b/lib/Dialect/LTL/LTLTypes.cpp @@ -0,0 +1,24 @@ +#include "circt/Dialect/LTL/LTLTypes.h" +#include "circt/Dialect/LTL/LTLOps.h" + +using namespace circt; +using namespace ltl; + +bool circt::ltl::isClocked(mlir::Type type) { + return isa(type); +} + +bool circt::ltl::isDisabled(mlir::Type type) { + return isa(type); +} + +bool circt::ltl::isProperty(mlir::Type type) { + return isa< + ClockedPropertyType, DisabledPropertyType, + ClockedDisabledPropertyType, PropertyType>(type); +} + +bool circt::ltl::isSequence(mlir::Type type) { + return isa(type); +} diff --git a/test/Conversion/ExportVerilog/prepare-for-emission.mlir b/test/Conversion/ExportVerilog/prepare-for-emission.mlir index 17dd7d7aad4a..20707ae255b0 100644 --- a/test/Conversion/ExportVerilog/prepare-for-emission.mlir +++ b/test/Conversion/ExportVerilog/prepare-for-emission.mlir @@ -159,10 +159,10 @@ module attributes {circt.loweringOptions = "disallowExpressionInliningInPorts"} // CHECK: %[[READ:.+]] = sv.read_inout %[[WIRE]] // CHECK: ltl.disable %{{.+}} if %[[READ]] %i0 = ltl.implication %a, %b : i1, i1 - %k0 = ltl.clock %i0, posedge %clk : !ltl.property - %k5 = ltl.disable %k0 if %b_xor_b : !ltl.property + %k0 = ltl.clock %i0, posedge %clk : !ltl.clocked_property + %k5 = ltl.disable %k0 if %b_xor_b : !ltl.clcoked_disabled_property - verif.assert %k5: !ltl.property + verif.assert %k5: !ltl.clcoked_disabled_property } } diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir index 48fff8e7306a..a5c23c10756a 100644 --- a/test/Conversion/ExportVerilog/verif.mlir +++ b/test/Conversion/ExportVerilog/verif.mlir @@ -102,10 +102,10 @@ hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) { %g1 = ltl.and %c0, %c1 : !ltl.sequence, !ltl.sequence %g2 = ltl.or %a, %b : i1, i1 %g3 = ltl.or %c0, %c1 : !ltl.sequence, !ltl.sequence - verif.assert %g0 : !ltl.sequence - verif.assert %g1 : !ltl.sequence - verif.assert %g2 : !ltl.sequence - verif.assert %g3 : !ltl.sequence + verif.assert %g0 : !ltl.property + verif.assert %g1 : !ltl.property + verif.assert %g2 : !ltl.property + verif.assert %g3 : !ltl.property // CHECK: assert property (@(posedge clk) a); // CHECK: assert property (@(negedge clk) a); @@ -117,11 +117,11 @@ hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) { %k2 = ltl.clock %a, edge %clk : i1 %k3 = ltl.clock %d1, posedge %clk : !ltl.sequence %k4 = ltl.concat %b, %k0 : i1, !ltl.sequence - verif.assert %k0 : !ltl.sequence - verif.assert %k1 : !ltl.sequence - verif.assert %k2 : !ltl.sequence - verif.assert %k3 : !ltl.sequence - verif.assert %k4 : !ltl.sequence + verif.assert %k0 : !ltl.clocked_sequence + verif.assert %k1 : !ltl.clocked_sequence + verif.assert %k2 : !ltl.clocked_sequence + verif.assert %k3 : !ltl.clocked_sequence + verif.assert %k4 : !ltl.clocked_sequence } // CHECK-LABEL: module Properties @@ -157,11 +157,11 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) { // CHECK: assert property (@(posedge clk) disable iff (b) not a); %k0 = ltl.clock %i0, posedge %clk : !ltl.property %k1 = ltl.clock %n0, negedge %b : !ltl.property - %k2 = ltl.implication %i2, %k1 : !ltl.sequence, !ltl.property - %k3 = ltl.clock %k2, posedge %clk : !ltl.property - %k4 = ltl.disable %n0 if %b : !ltl.property - %k5 = ltl.disable %k0 if %b : !ltl.property - %k6 = ltl.clock %k4, posedge %clk : !ltl.property + %k2 = ltl.implication %i2, %k1 : !ltl.sequence, !ltl.clocked_property + %k3 = ltl.clock %k2, posedge %clk : !ltl.clocked_property + %k4 = ltl.disable %n0 if %b : !ltl.disabled_property + %k5 = ltl.disable %k0 if %b : !ltl.clocked_disabled_property + %k6 = ltl.clock %k4, posedge %clk : !ltl.clocked_disabled_property verif.assert %k0 : !ltl.property verif.assert %k3 : !ltl.property verif.assert %k4 : !ltl.property @@ -216,14 +216,14 @@ hw.module @SystemVerilogSpecExamples(in %clk: i1, in %a: i1, in %b: i1, in %c: i %b0 = ltl.delay %c, 1, 0 : i1 %b1 = ltl.concat %b, %b0, %a1 : i1, !ltl.sequence, !ltl.sequence %b2 = ltl.implication %a, %b1 : i1, !ltl.sequence - %b3 = ltl.clock %b2, posedge %clk : !ltl.property + %b3 = ltl.clock %b2, posedge %clk : !ltl.clocked_property verif.assert %b3 : !ltl.property // CHECK: assert property (@(posedge clk) disable iff (e) a |-> not b ##1 c ##1 d); %c0 = ltl.not %b1 : !ltl.sequence %c1 = ltl.implication %a, %c0 : i1, !ltl.property - %c2 = ltl.disable %c1 if %e : !ltl.property - %c3 = ltl.clock %c2, posedge %clk : !ltl.property + %c2 = ltl.disable %c1 if %e : !ltl.disabled_property + %c3 = ltl.clock %c2, posedge %clk : !ltl.clocked_disabled_property verif.assert %c3 : !ltl.property // CHECK: assert property (##1 a |-> b); @@ -244,8 +244,8 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) { %0 = comb.and %fell_reset, %not_isLive : i1 %1 = ltl.eventually %isLive : i1 %2 = ltl.implication %0, %1 : i1, !ltl.property - %3 = ltl.disable %2 if %reset : !ltl.property - %liveness_after_reset = ltl.clock %3, posedge %clock : !ltl.property + %3 = ltl.disable %2 if %reset : !ltl.disabled_property + %liveness_after_reset = ltl.clock %3, posedge %clock : !ltl.clocked_disabled_property verif.assert %liveness_after_reset : !ltl.property verif.assume %liveness_after_reset : !ltl.property @@ -254,8 +254,8 @@ hw.module @LivenessExample(in %clock: i1, in %reset: i1, in %isLive: i1) { %4 = ltl.delay %not_isLive, 1, 0 : i1 %5 = ltl.concat %isLive, %4 : i1, !ltl.sequence %6 = ltl.implication %5, %1 : !ltl.sequence, !ltl.property - %7 = ltl.disable %6 if %reset : !ltl.property - %liveness_after_fall = ltl.clock %7, posedge %clock : !ltl.property + %7 = ltl.disable %6 if %reset : !ltl.disabled_property + %liveness_after_fall = ltl.clock %7, posedge %clock : !ltl.clocked_disabled_property verif.assert %liveness_after_fall : !ltl.property verif.assume %liveness_after_fall : !ltl.property } diff --git a/test/Conversion/FIRRTLToHW/intrinsics.mlir b/test/Conversion/FIRRTLToHW/intrinsics.mlir index 8b18481f9f27..aed5e668dd68 100644 --- a/test/Conversion/FIRRTLToHW/intrinsics.mlir +++ b/test/Conversion/FIRRTLToHW/intrinsics.mlir @@ -68,17 +68,17 @@ firrtl.circuit "Intrinsics" { %d1 = firrtl.int.ltl.delay %b, 42, 1337 : (!firrtl.uint<1>) -> !firrtl.uint<1> // CHECK-NEXT: [[L0:%.+]] = ltl.and [[D0]], [[D1]] : !ltl.sequence, !ltl.sequence - // CHECK-NEXT: [[L1:%.+]] = ltl.or %a, [[L0]] : i1, !ltl.sequence + // CHECK-NEXT: [[L1:%.+]] = ltl.or %a, [[L0]] : i1, !ltl.property %l0 = firrtl.int.ltl.and %d0, %d1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> %l1 = firrtl.int.ltl.or %a, %l0 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK-NEXT: [[C0:%.+]] = ltl.concat [[D0]], [[L1]] : !ltl.sequence, !ltl.sequence + // CHECK-NEXT: [[C0:%.+]] = ltl.concat [[D0]], [[L1]] : !ltl.property, !ltl.sequence %c0 = firrtl.int.ltl.concat %d0, %l1 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK-NEXT: [[N0:%.+]] = ltl.not [[C0]] : !ltl.sequence + // CHECK-NEXT: [[N0:%.+]] = ltl.not [[C0]] : !ltl.property %n0 = firrtl.int.ltl.not %c0 : (!firrtl.uint<1>) -> !firrtl.uint<1> - // CHECK-NEXT: [[I0:%.+]] = ltl.implication [[C0]], [[N0]] : !ltl.sequence, !ltl.property + // CHECK-NEXT: [[I0:%.+]] = ltl.implication [[C0]], [[N0]] : !ltl.property, !ltl.property %i0 = firrtl.int.ltl.implication %c0, %n0 : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> // CHECK-NEXT: [[E0:%.+]] = ltl.eventually [[I0]] : !ltl.property @@ -87,15 +87,15 @@ firrtl.circuit "Intrinsics" { // CHECK-NEXT: [[K0:%.+]] = ltl.clock [[I0]], posedge [[CLK]] : !ltl.property %k0 = firrtl.int.ltl.clock %i0, %clk : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1> - // CHECK-NEXT: [[D2:%.+]] = ltl.disable [[K0]] if %b : !ltl.property + // CHECK-NEXT: [[D2:%.+]] = ltl.disable [[K0]] if %b : !ltl.clocked_property %d2 = firrtl.int.ltl.disable %k0, %b : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1> // CHECK-NEXT: verif.assert %a : i1 // CHECK-NEXT: verif.assert %a label "hello" : i1 - // CHECK-NEXT: verif.assume [[C0]] : !ltl.sequence - // CHECK-NEXT: verif.assume [[C0]] label "hello" : !ltl.sequence - // CHECK-NEXT: verif.cover [[K0]] : !ltl.property - // CHECK-NEXT: verif.cover [[K0]] label "hello" : !ltl.property + // CHECK-NEXT: verif.assume [[C0]] : !ltl.property + // CHECK-NEXT: verif.assume [[C0]] label "hello" : !ltl.property + // CHECK-NEXT: verif.cover [[K0]] : !ltl.clocked_property + // CHECK-NEXT: verif.cover [[K0]] label "hello" : !ltl.clocked_property firrtl.int.verif.assert %a : !firrtl.uint<1> firrtl.int.verif.assert %a {label = "hello"} : !firrtl.uint<1> firrtl.int.verif.assume %c0 : !firrtl.uint<1> diff --git a/test/Conversion/LTLToCore/assertproperty.mlir b/test/Conversion/LTLToCore/assertproperty.mlir index 5c4454b9220f..be9bc6097fb3 100644 --- a/test/Conversion/LTLToCore/assertproperty.mlir +++ b/test/Conversion/LTLToCore/assertproperty.mlir @@ -29,8 +29,8 @@ module { //CHECK: sv.always posedge %1 { //CHECK: sv.assert %7, immediate //CHECK: } - %14 = ltl.clock %13, posedge %0 : !ltl.property - verif.assert %14 : !ltl.property + %14 = ltl.clock %13, posedge %0 : !ltl.disabled_property + verif.assert %14 : !ltl.clocked_disabled_property //CHECK: hw.output hw.output diff --git a/test/Dialect/LTL/basic.mlir b/test/Dialect/LTL/basic.mlir index ab5eabc9c9b7..0942521eff87 100644 --- a/test/Dialect/LTL/basic.mlir +++ b/test/Dialect/LTL/basic.mlir @@ -38,9 +38,9 @@ ltl.or %p, %p : !ltl.property, !ltl.property %p1 = ltl.and %p, %true : !ltl.property, i1 %p2 = ltl.and %s, %p : !ltl.sequence, !ltl.property %p3 = ltl.and %p, %s : !ltl.property, !ltl.sequence -unrealized_conversion_cast %s0 : !ltl.sequence to index -unrealized_conversion_cast %s1 : !ltl.sequence to index -unrealized_conversion_cast %s2 : !ltl.sequence to index +unrealized_conversion_cast %s0 : !ltl.property to index +unrealized_conversion_cast %s1 : !ltl.property to index +unrealized_conversion_cast %s2 : !ltl.property to index unrealized_conversion_cast %p0 : !ltl.property to index unrealized_conversion_cast %p1 : !ltl.property to index unrealized_conversion_cast %p2 : !ltl.property to index @@ -87,11 +87,11 @@ ltl.eventually %p : !ltl.property // Clocking //===----------------------------------------------------------------------===// -// CHECK: ltl.clock {{%.+}}, posedge {{%.+}} : !ltl.sequence -// CHECK: ltl.clock {{%.+}}, negedge {{%.+}} : !ltl.sequence -// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : i1 -// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.sequence -// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.property +// CHECK: ltl.clock {{%.+}}, posedge {{%.+}} : !ltl.clocked_sequence +// CHECK: ltl.clock {{%.+}}, negedge {{%.+}} : !ltl.clocked_sequence +// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.clocked_property +// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.clocked_sequence +// CHECK: ltl.clock {{%.+}}, edge {{%.+}} : !ltl.clocked_property ltl.clock %s, posedge %true : !ltl.sequence ltl.clock %s, negedge %true : !ltl.sequence %clk0 = ltl.clock %true, edge %true : i1 @@ -100,9 +100,9 @@ ltl.clock %s, negedge %true : !ltl.sequence // Type inference. `unrealized_conversion_cast` used to detect unexpected return // types on `ltl.and`. -unrealized_conversion_cast %clk0 : !ltl.sequence to index -unrealized_conversion_cast %clk1 : !ltl.sequence to index -unrealized_conversion_cast %clk2 : !ltl.property to index +unrealized_conversion_cast %clk0 : !ltl.clocked_sequence to index +unrealized_conversion_cast %clk1 : !ltl.clocked_sequence to index +unrealized_conversion_cast %clk2 : !ltl.clocked_property to index // CHECK: ltl.disable {{%.+}} if {{%.+}} : !ltl.property ltl.disable %p if %true : !ltl.property diff --git a/test/Dialect/LTL/canonicalization.mlir b/test/Dialect/LTL/canonicalization.mlir index 1f8e1e99a49b..30711b20a487 100644 --- a/test/Dialect/LTL/canonicalization.mlir +++ b/test/Dialect/LTL/canonicalization.mlir @@ -2,7 +2,7 @@ func.func private @Bool(%arg0: i1) func.func private @Seq(%arg0: !ltl.sequence) -func.func private @Prop(%arg0: !ltl.property) +func.func private @Prop(%arg0: !ltl.disabled_property) // CHECK-LABEL: @DelayFolds func.func @DelayFolds(%arg0: !ltl.sequence) { @@ -101,6 +101,6 @@ func.func @ClockingFolds(%arg0: !ltl.property) { // CHECK-NEXT: call @Prop(%arg0) %false = hw.constant false %0 = ltl.disable %arg0 if %false : !ltl.property - call @Prop(%0) : (!ltl.property) -> () + call @Prop(%0) : (!ltl.disabled_property) -> () return }