[LTL] Canonicalize ltl.and to comb.and for i1 properties (#7759)

Extend `ltl.and`, `ltl.or`, and `ltl.intersect` to infer their return
type as `i1` if all operands are `i1`. Also add a canonicalization
method that replaces these ops with `comb.and` and `comb.or` if they
operate entirely on `i1`.

include/circt/Dialect/LTL/LTLOps.td

@@ -39,6 +39,7 @@ def AndOp : AssocLTLOp<"and"> {
     If any of the `$inputs` is of type `!ltl.property`, the result of the op is
     an `!ltl.property`. Otherwise it is an `!ltl.sequence`.
   }];
+  let hasCanonicalizeMethod = 1;
 }
 
 def OrOp : AssocLTLOp<"or"> {
@@ -47,6 +48,7 @@ def OrOp : AssocLTLOp<"or"> {
     If any of the `$inputs` is of type `!ltl.property`, the result of the op is
     an `!ltl.property`. Otherwise it is an `!ltl.sequence`.
   }];
+  let hasCanonicalizeMethod = 1;
 }
 
 def IntersectOp : AssocLTLOp<"intersect"> {
@@ -56,6 +58,7 @@ def IntersectOp : AssocLTLOp<"intersect"> {
     and have the same start and end times. This differs from `ltl.and` which doesn't 
     consider the timings of each operand, only their results. 
   }];
+  let hasCanonicalizeMethod = 1;
 }
 
 //===----------------------------------------------------------------------===//

lib/Dialect/LTL/LTLFolds.cpp

@@ -46,6 +46,35 @@ namespace patterns {
 #include "circt/Dialect/LTL/LTLFolds.cpp.inc"
 } // namespace patterns
 
+//===----------------------------------------------------------------------===//
+// AndOp / OrOp / IntersectOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult AndOp::canonicalize(AndOp op, PatternRewriter &rewriter) {
+  if (op.getType() == rewriter.getI1Type()) {
+    rewriter.replaceOpWithNewOp<comb::AndOp>(op, op.getInputs(), true);
+    return success();
+  }
+  return failure();
+}
+
+LogicalResult OrOp::canonicalize(OrOp op, PatternRewriter &rewriter) {
+  if (op.getType() == rewriter.getI1Type()) {
+    rewriter.replaceOpWithNewOp<comb::OrOp>(op, op.getInputs(), true);
+    return success();
+  }
+  return failure();
+}
+
+LogicalResult IntersectOp::canonicalize(IntersectOp op,
+                                        PatternRewriter &rewriter) {
+  if (op.getType() == rewriter.getI1Type()) {
+    rewriter.replaceOpWithNewOp<comb::AndOp>(op, op.getInputs(), true);
+    return success();
+  }
+  return failure();
+}
+
 //===----------------------------------------------------------------------===//
 // DelayOp
 //===----------------------------------------------------------------------===//

lib/Dialect/LTL/LTLOps.cpp

@@ -33,9 +33,12 @@ static LogicalResult inferAndLikeReturnTypes(MLIRContext *context,
         return isa<PropertyType>(operand.getType());
       })) {
     results.push_back(PropertyType::get(context));
-  } else {
+  } else if (llvm::any_of(operands, [](auto operand) {
-
+               return isa<SequenceType>(operand.getType());
+             })) {
     results.push_back(SequenceType::get(context));
+  } else {
+    results.push_back(IntegerType::get(context, 1));
   }
   return success();
 }

test/Conversion/ExportVerilog/verif.mlir

@@ -94,14 +94,14 @@ hw.module @Sequences(in %clk: i1, in %a: i1, in %b: i1) {
   %c3 = ltl.concat %d1, %d2, %d3 : !ltl.sequence, !ltl.sequence, !ltl.sequence
   sv.assert_property %c3 : !ltl.sequence
 
-  // CHECK: assert property (a and b);
+  // CHECK: assert property (a and ##0 a);
-  %g0 = ltl.and %a, %b : i1, i1
+  %g0 = ltl.and %a, %d0 : i1, !ltl.sequence
   sv.assert_property %g0 : !ltl.sequence
   // CHECK: assert property (a ##0 a and a ##4 a);
   %g1 = ltl.and %c0, %c1 : !ltl.sequence, !ltl.sequence
   sv.assert_property %g1 : !ltl.sequence
-  // CHECK: assert property (a or b);
+  // CHECK: assert property (a or ##0 a);
-  %g2 = ltl.or %a, %b : i1, i1
+  %g2 = ltl.or %a, %d0 : i1, !ltl.sequence
   sv.assert_property %g2 : !ltl.sequence
   // CHECK: assert property (a ##0 a or a ##4 a);
   %g3 = ltl.or %c0, %c1 : !ltl.sequence, !ltl.sequence
@@ -207,17 +207,18 @@ hw.module @Properties(in %clk: i1, in %a: i1, in %b: i1) {
 
 // CHECK-LABEL: module Precedence
 hw.module @Precedence(in %a: i1, in %b: i1) {
-  // CHECK: assert property ((a or b) and b);
+  // CHECK: assert property ((a or ##0 b) and b);
-  %a0 = ltl.or %a, %b : i1, i1
+  %a0 = ltl.delay %b, 0, 0 : i1
-  %a1 = ltl.and %a0, %b : !ltl.sequence, i1
+  %a1 = ltl.or %a, %a0 : i1, !ltl.sequence
-  sv.assert_property %a1 : !ltl.sequence
+  %a2 = ltl.and %a1, %b : !ltl.sequence, i1
+  sv.assert_property %a2 : !ltl.sequence
 
-  // CHECK: assert property (##1 (a or b));
+  // CHECK: assert property (##1 (a or ##0 b));
-  %d0 = ltl.delay %a0, 1, 0 : !ltl.sequence
+  %d0 = ltl.delay %a1, 1, 0 : !ltl.sequence
   sv.assert_property %d0 : !ltl.sequence
 
-  // CHECK: assert property (not (a or b));
+  // CHECK: assert property (not (a or ##0 b));
-  %n0 = ltl.not %a0 : !ltl.sequence
+  %n0 = ltl.not %a1 : !ltl.sequence
   sv.assert_property %n0 : !ltl.property
 
   // CHECK: assert property (a and (a |-> b));

test/Dialect/LTL/basic.mlir

@@ -38,7 +38,7 @@ 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 %s0 : i1 to index
 unrealized_conversion_cast %s1 : !ltl.sequence to index
 unrealized_conversion_cast %s2 : !ltl.sequence to index
 unrealized_conversion_cast %p0 : !ltl.property to index

test/Dialect/LTL/canonicalization.mlir

@@ -128,3 +128,18 @@ func.func @NonConsecutiveRepeatFolds(%arg0: !ltl.sequence) {
 
   return
 }
+
+// CHECK-LABEL: @CanonicalizeToComb
+func.func @CanonicalizeToComb(%arg0: i1, %arg1: i1, %arg2: i1) {
+  // CHECK-NEXT: comb.and bin %arg0, %arg1, %arg2 : i1
+  %0 = ltl.and %arg0, %arg1, %arg2 : i1, i1, i1
+  // CHECK-NEXT: comb.or bin %arg0, %arg1, %arg2 : i1
+  %1 = ltl.or %arg0, %arg1, %arg2 : i1, i1, i1
+  // CHECK-NEXT: comb.and bin %arg0, %arg1, %arg2 : i1
+  %2 = ltl.intersect %arg0, %arg1, %arg2 : i1, i1, i1
+
+  call @Bool(%0) : (i1) -> ()
+  call @Bool(%1) : (i1) -> ()
+  call @Bool(%2) : (i1) -> ()
+  return
+}