[LTL] Add clocked and disabled property types

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<InferTypeOpInterface>
+]> {
   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<LTLAnySequenceType>:$inputs);
-  let results = (outs LTLSequenceType:$result);
+def ConcatOp : LTLOp<"concat", [
+  Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
+]> {
+  let arguments = (ins Variadic<LTLAnyPropertyType>:$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<InferTypeOpInterface>
+]> {
   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<InferTypeOpInterface>
+]> {
   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<InferTypeOpInterface>
+]> {
   let arguments = (ins LTLAnyPropertyType:$input);
   let results = (outs LTLPropertyType:$result);
   let assemblyFormat = [{
@@ -229,7 +239,7 @@ def ClockOp : LTLOp<"clock", [
   Pure, InferTypeOpInterface, DeclareOpInterfaceMethods<InferTypeOpInterface>
 ]> {
   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<InferTypeOpInterface>
+]> {
+  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

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

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

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

lib/Dialect/LTL/LTLOps.cpp

@@ -23,52 +23,160 @@ using namespace mlir;
 #include "circt/Dialect/LTL/LTL.cpp.inc"
 
 //===----------------------------------------------------------------------===//
-// AndOp / OrOp
+// ClockOp / DisableOp
 //===----------------------------------------------------------------------===//
 
-static LogicalResult inferAndLikeReturnTypes(MLIRContext *context,
-                                             ValueRange operands,
-                                             SmallVectorImpl<Type> &results) {
-  if (llvm::any_of(operands, [](auto operand) {
-        return isa<PropertyType>(operand.getType());
-      })) {
-    results.push_back(PropertyType::get(context));
+LogicalResult
+ClockOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                          ValueRange operands, DictionaryAttr attributes,
+                          OpaqueProperties properties, RegionRange regions,
+                          SmallVectorImpl<Type> &inferredReturnTypes) {
+  auto type = operands[0].getType();
+
+  if (isa<IntegerType>(type)) {
+    inferredReturnTypes.push_back(ClockedSequenceType::get(context));
+  } else if (isa<PropertyType>(type)) {
+    inferredReturnTypes.push_back(ClockedPropertyType::get(context));
+  } else if (isa<DisabledPropertyType>(type)) {
+    inferredReturnTypes.push_back(ClockedDisabledPropertyType::get(context));
+  } else {
+    inferredReturnTypes.push_back(ClockedSequenceType::get(context));
+  }
+  return success();
+}
+
+LogicalResult
+DisableOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                            ValueRange operands, DictionaryAttr attributes,
+                            OpaqueProperties properties, RegionRange regions,
+                            SmallVectorImpl<Type> &inferredReturnTypes) {
+  auto type = operands[0].getType();
+  if (isa<IntegerType>(type) || isa<PropertyType>(type)) {
+    inferredReturnTypes.push_back(DisabledPropertyType::get(context));
+  } else if (isa<ClockedPropertyType>(type)) {
+    inferredReturnTypes.push_back(ClockedDisabledPropertyType::get(context));
+  } else if (isa<ClockedSequenceType>(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<Type> &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<Type> &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<Location> loc,
+                          ValueRange operands, DictionaryAttr attributes,
+                          OpaqueProperties properties, RegionRange regions,
+                          SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferSequenceLikeReturnTypes(context, operands, inferredReturnTypes);
+}
+
+LogicalResult
+ConcatOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                           ValueRange operands, DictionaryAttr attributes,
+                           OpaqueProperties properties, RegionRange regions,
+                           SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferSequenceLikeReturnTypes(context, operands, inferredReturnTypes);
+}
+
+LogicalResult
+NotOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
+                        ValueRange operands, DictionaryAttr attributes,
+                        OpaqueProperties properties, RegionRange regions,
+                        SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes);
+}
+
 LogicalResult
 AndOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
                         ValueRange operands, DictionaryAttr attributes,
                         OpaqueProperties properties, RegionRange regions,
                         SmallVectorImpl<Type> &inferredReturnTypes) {
-  return inferAndLikeReturnTypes(context, operands, inferredReturnTypes);
+  return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes);
 }
 
 LogicalResult
 OrOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
                        ValueRange operands, DictionaryAttr attributes,
                        OpaqueProperties properties, RegionRange regions,
                        SmallVectorImpl<Type> &inferredReturnTypes) {
-  return inferAndLikeReturnTypes(context, operands, inferredReturnTypes);
+  return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes);
 }
 
-//===----------------------------------------------------------------------===//
-// ClockOp
-//===----------------------------------------------------------------------===//
+LogicalResult ImplicationOp::inferReturnTypes(
+    MLIRContext *context, std::optional<Location> loc, ValueRange operands,
+    DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions,
+    SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes);
+}
 
-LogicalResult
-ClockOp::inferReturnTypes(MLIRContext *context, std::optional<Location> loc,
-                          ValueRange operands, DictionaryAttr attributes,
-                          OpaqueProperties properties, RegionRange regions,
-                          SmallVectorImpl<Type> &inferredReturnTypes) {
-  if (isa<PropertyType>(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<Location> loc, ValueRange operands,
+    DictionaryAttr attributes, OpaqueProperties properties, RegionRange regions,
+    SmallVectorImpl<Type> &inferredReturnTypes) {
+  return inferPropertyLikeReturnTypes(context, operands, inferredReturnTypes);
 }