diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td index 1938a7f3b2..7f0cbd4545 100644 --- a/include/circt/Dialect/LTL/LTLOps.td +++ b/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; } //===----------------------------------------------------------------------===// diff --git a/lib/Dialect/LTL/LTLFolds.cpp b/lib/Dialect/LTL/LTLFolds.cpp index d01672996e..963dc2022e 100644 --- a/lib/Dialect/LTL/LTLFolds.cpp +++ b/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(op, op.getInputs(), true); + return success(); + } + return failure(); +} + +LogicalResult OrOp::canonicalize(OrOp op, PatternRewriter &rewriter) { + if (op.getType() == rewriter.getI1Type()) { + rewriter.replaceOpWithNewOp(op, op.getInputs(), true); + return success(); + } + return failure(); +} + +LogicalResult IntersectOp::canonicalize(IntersectOp op, + PatternRewriter &rewriter) { + if (op.getType() == rewriter.getI1Type()) { + rewriter.replaceOpWithNewOp(op, op.getInputs(), true); + return success(); + } + return failure(); +} + //===----------------------------------------------------------------------===// // DelayOp //===----------------------------------------------------------------------===// diff --git a/lib/Dialect/LTL/LTLOps.cpp b/lib/Dialect/LTL/LTLOps.cpp index 80c74f14ae..1114de512f 100644 --- a/lib/Dialect/LTL/LTLOps.cpp +++ b/lib/Dialect/LTL/LTLOps.cpp @@ -33,9 +33,12 @@ static LogicalResult inferAndLikeReturnTypes(MLIRContext *context, return isa(operand.getType()); })) { results.push_back(PropertyType::get(context)); - } else { - + } else if (llvm::any_of(operands, [](auto operand) { + return isa(operand.getType()); + })) { results.push_back(SequenceType::get(context)); + } else { + results.push_back(IntegerType::get(context, 1)); } return success(); } diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir index cc317ec007..bbe39ad348 100644 --- a/test/Conversion/ExportVerilog/verif.mlir +++ b/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); - %g0 = ltl.and %a, %b : i1, i1 + // CHECK: assert property (a and ##0 a); + %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); - %g2 = ltl.or %a, %b : i1, i1 + // CHECK: assert property (a or ##0 a); + %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); - %a0 = ltl.or %a, %b : i1, i1 - %a1 = ltl.and %a0, %b : !ltl.sequence, i1 - sv.assert_property %a1 : !ltl.sequence + // CHECK: assert property ((a or ##0 b) and b); + %a0 = ltl.delay %b, 0, 0 : i1 + %a1 = ltl.or %a, %a0 : i1, !ltl.sequence + %a2 = ltl.and %a1, %b : !ltl.sequence, i1 + sv.assert_property %a2 : !ltl.sequence - // CHECK: assert property (##1 (a or b)); - %d0 = ltl.delay %a0, 1, 0 : !ltl.sequence + // CHECK: assert property (##1 (a or ##0 b)); + %d0 = ltl.delay %a1, 1, 0 : !ltl.sequence sv.assert_property %d0 : !ltl.sequence - // CHECK: assert property (not (a or b)); - %n0 = ltl.not %a0 : !ltl.sequence + // CHECK: assert property (not (a or ##0 b)); + %n0 = ltl.not %a1 : !ltl.sequence sv.assert_property %n0 : !ltl.property // CHECK: assert property (a and (a |-> b)); diff --git a/test/Dialect/LTL/basic.mlir b/test/Dialect/LTL/basic.mlir index ebaa462047..70727244f1 100644 --- a/test/Dialect/LTL/basic.mlir +++ 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 diff --git a/test/Dialect/LTL/canonicalization.mlir b/test/Dialect/LTL/canonicalization.mlir index 671bd81742..f1979e749e 100644 --- a/test/Dialect/LTL/canonicalization.mlir +++ b/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 +}