diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td index 371a4e2a74..c5edc697db 100644 --- a/include/circt/Dialect/Verif/VerifOps.td +++ b/include/circt/Dialect/Verif/VerifOps.td @@ -224,14 +224,31 @@ def BoundedModelCheckingOp : VerifOp<"bmc", [ let hasRegionVerifier = true; } -def LogicEquivalenceCheckingOp : VerifOp<"lec", [ - IsolatedFromAbove, - SingleBlockImplicitTerminator<"verif::YieldOp">, -]> { +// Attempt to prove a binary relation between two circuits +class CircuitRelationCheckOp traits = []> + : VerifOp])> +{ + let results = (outs Optional:$isProven); + let regions = (region SizedRegion<1>:$firstCircuit, + SizedRegion<1>:$secondCircuit); + + let assemblyFormat = [{ + attr-dict (`:` type($isProven)^)? + `first` $firstCircuit + `second` $secondCircuit + }]; + + let builders = [OpBuilder<(ins "bool":$hasResult), [{ + build($_builder, $_state, hasResult ? $_builder.getI1Type() : Type{} ); + }]>]; +} + +def LogicEquivalenceCheckingOp : CircuitRelationCheckOp<"lec"> { let summary = "represents a logical equivalence checking problem"; let description = [{ This operation represents a logic equivalence checking problem explicitly in - the IR. There are several possiblities to perform logical equivalence + the IR. There are several possibilities to perform logical equivalence checking. For example, equivalence checking of combinational circuits can be done by constructing a miter circuit and testing whether the result is satisfiable (can be non-zero for some input), or two canonical BDDs could be @@ -241,25 +258,37 @@ def LogicEquivalenceCheckingOp : VerifOp<"lec", [ also the block arguments and yielded values of both regions) have to match. Otherwise, the two should be considered trivially non-equivalent. - The operation can return an boolean result that is `true` iff equivalence + The operation can return a boolean result that is `true` iff equivalence of the two circuits has been proven. The result can be omitted for use-cases which do not allow further processing (e.g., SMT-LIB exporting). }]; - let results = (outs Optional:$areEquivalent); - let regions = (region SizedRegion<1>:$firstCircuit, - SizedRegion<1>:$secondCircuit); + let hasRegionVerifier = true; +} - let assemblyFormat = [{ - attr-dict (`:` type($areEquivalent)^)? - `first` $firstCircuit - `second` $secondCircuit +def RefinementCheckingOp : CircuitRelationCheckOp<"refines"> { + let summary = + "check if the second module is a refinement of the first module"; + let description = [{ + This operation represents a refinement checking problem explicitly in the + IR. Given two (purely combinational) circuits A and B with the same + signature, B refines A iff for all inputs the set of possible output + values of B is a subset of the possible output values of A given the + same input. + + For strictly deterministic circuits the 'refines' relation is identical to + logical equivalence. Informally speaking, refining allows maintaining or + reducing the non-determinism of a circuit. + + If the signatures of the circuits do not match, the second circuit is + trivially assumed to _not_ be a refinement of the first circuit. Sequential + elements (i.e., registers and memories) are currently unsupported. + + The operation can return a boolean result that is `true` iff the refinement + relation has been proven. The result can be omitted for use-cases which do + not allow further processing (e.g., SMT-LIB exporting). }]; - let builders = [OpBuilder<(ins "bool":$hasResult), [{ - build($_builder, $_state, hasResult ? $_builder.getI1Type() : Type{} ); - }]>]; - let hasRegionVerifier = true; } @@ -268,6 +297,7 @@ def YieldOp : VerifOp<"yield", [ ParentOneOf<[ "verif::BoundedModelCheckingOp", "verif::LogicEquivalenceCheckingOp", + "verif::RefinementCheckingOp", "verif::SimulationOp", ]> ]> { diff --git a/lib/Dialect/Verif/VerifOps.cpp b/lib/Dialect/Verif/VerifOps.cpp index 4cd6529e0c..6f53f503aa 100644 --- a/lib/Dialect/Verif/VerifOps.cpp +++ b/lib/Dialect/Verif/VerifOps.cpp @@ -93,20 +93,38 @@ LogicalResult CoverOp::canonicalize(CoverOp op, PatternRewriter &rewriter) { return AssertLikeOp::canonicalize(op, rewriter); } +//===----------------------------------------------------------------------===// +// CircuitRelationCheckOp +//===----------------------------------------------------------------------===// + +template +static LogicalResult verifyCircuitRelationCheckOpRegions(OpTy &op) { + if (op.getFirstCircuit().getArgumentTypes() != + op.getSecondCircuit().getArgumentTypes()) + return op.emitOpError() + << "block argument types of both regions must match"; + if (op.getFirstCircuit().front().getTerminator()->getOperandTypes() != + op.getSecondCircuit().front().getTerminator()->getOperandTypes()) + return op.emitOpError() + << "types of the yielded values of both regions must match"; + + return success(); +} + //===----------------------------------------------------------------------===// // LogicalEquivalenceCheckingOp //===----------------------------------------------------------------------===// LogicalResult LogicEquivalenceCheckingOp::verifyRegions() { - if (getFirstCircuit().getArgumentTypes() != - getSecondCircuit().getArgumentTypes()) - return emitOpError() << "block argument types of both regions must match"; - if (getFirstCircuit().front().getTerminator()->getOperandTypes() != - getSecondCircuit().front().getTerminator()->getOperandTypes()) - return emitOpError() - << "types of the yielded values of both regions must match"; + return verifyCircuitRelationCheckOpRegions(*this); +} - return success(); +//===----------------------------------------------------------------------===// +// RefinementCheckingOp +//===----------------------------------------------------------------------===// + +LogicalResult RefinementCheckingOp::verifyRegions() { + return verifyCircuitRelationCheckOpRegions(*this); } //===----------------------------------------------------------------------===// diff --git a/lib/Tools/circt-lec/ConstructLEC.cpp b/lib/Tools/circt-lec/ConstructLEC.cpp index c8ea3762c1..8cd7ee6694 100644 --- a/lib/Tools/circt-lec/ConstructLEC.cpp +++ b/lib/Tools/circt-lec/ConstructLEC.cpp @@ -100,7 +100,7 @@ Value ConstructLECPass::constructMiter(OpBuilder builder, Location loc, sortTopologically(&lecOp.getFirstCircuit().front()); sortTopologically(&lecOp.getSecondCircuit().front()); - return withResult ? lecOp.getAreEquivalent() : Value{}; + return withResult ? lecOp.getIsProven() : Value{}; } void ConstructLECPass::runOnOperation() { diff --git a/test/Dialect/Verif/basic.mlir b/test/Dialect/Verif/basic.mlir index 3ed0dd8bfb..26a4c2f4af 100644 --- a/test/Dialect/Verif/basic.mlir +++ b/test/Dialect/Verif/basic.mlir @@ -166,6 +166,32 @@ verif.lec {verif.some_attr} first { verif.yield %arg0, %arg1 : i32, i32 {verif.some_attr} } +//===----------------------------------------------------------------------===// +// Refinement Checking related operations +//===----------------------------------------------------------------------===// + +// CHECK: verif.refines first { +// CHECK: } second { +// CHECK: } +verif.refines first { +} second { +} + +// CHECK: verif.refines {verif.some_attr} first { +// CHECK: ^bb0(%{{.*}}: i32, %{{.*}}: i32): +// CHECK: verif.yield %{{.*}}, %{{.*}} : i32, i32 {verif.some_attr} +// CHECK: } second { +// CHECK: ^bb0(%{{.*}}: i32, %{{.*}}: i32): +// CHECK: verif.yield %{{.*}}, %{{.*}} : i32, i32 {verif.some_attr} +// CHECK: } +verif.refines {verif.some_attr} first { +^bb0(%arg0: i32, %arg1: i32): + verif.yield %arg0, %arg1 : i32, i32 {verif.some_attr} +} second { +^bb0(%arg0: i32, %arg1: i32): + verif.yield %arg0, %arg1 : i32, i32 {verif.some_attr} +} + //===----------------------------------------------------------------------===// // Bounded Model Checking related operations //===----------------------------------------------------------------------===// diff --git a/test/Dialect/Verif/errors.mlir b/test/Dialect/Verif/errors.mlir index 71ed1174ae..721a43d941 100644 --- a/test/Dialect/Verif/errors.mlir +++ b/test/Dialect/Verif/errors.mlir @@ -22,6 +22,28 @@ verif.lec first { // ----- +// expected-error @below {{types of the yielded values of both regions must match}} +verif.refines first { +^bb0(%arg0: i32): + verif.yield %arg0 : i32 +} second { +^bb0(%arg0: i32): + verif.yield +} + +// ----- + +// expected-error @below {{block argument types of both regions must match}} +verif.refines first { +^bb0(%arg0: i32, %arg1: i32): + verif.yield %arg0 : i32 +} second { +^bb0(%arg0: i32): + verif.yield %arg0 : i32 +} + +// ----- + // expected-error @below {{init region must have no arguments}} verif.bmc bound 10 num_regs 0 initial_values [] init { ^bb0(%clk: !seq.clock):