[Verif] Add RefinementCheckingOp (#8713)

This PR adds the RefinementCheckingOp to the verif dialect. The motivation behind this operation is to be able to automatically check whether a 'target' circuit is a refinement of a 'source' circuit. This should be a small step towards performing translation validation comparable to Alive2. The operation is structurally identical to the LogicEquivalenceCheckingOp, so I factored out most of the ODS into a common CircuitRelationCheckOp. If there is no non-determinism present in the circuits, the operation is also functionally identical to LogicEquivalenceCheckingOp.

Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>

include/circt/Dialect/Verif/VerifOps.td

@@ -224,14 +224,31 @@ def BoundedModelCheckingOp : VerifOp<"bmc", [
   let hasRegionVerifier = true;
 }
 
-def LogicEquivalenceCheckingOp : VerifOp<"lec", [
+// Attempt to prove a binary relation between two circuits
-  IsolatedFromAbove,
+class CircuitRelationCheckOp<string mnemonic, list<Trait> traits = []>
-  SingleBlockImplicitTerminator<"verif::YieldOp">,
+  : VerifOp<mnemonic, !listconcat(traits,
-]> {
+    [IsolatedFromAbove, SingleBlockImplicitTerminator<"verif::YieldOp">])>
+{
+  let results = (outs Optional<I1>:$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<I1>:$areEquivalent);
+  let hasRegionVerifier = true;
-  let regions = (region SizedRegion<1>:$firstCircuit,
+}
-                        SizedRegion<1>:$secondCircuit);
 
-  let assemblyFormat = [{
+def RefinementCheckingOp : CircuitRelationCheckOp<"refines"> {
-    attr-dict (`:` type($areEquivalent)^)?
+  let summary =
-    `first` $firstCircuit
+    "check if the second module is a refinement of the first module";
-    `second` $secondCircuit
+  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",
   ]>
 ]> {

lib/Dialect/Verif/VerifOps.cpp

@@ -93,20 +93,38 @@ LogicalResult CoverOp::canonicalize(CoverOp op, PatternRewriter &rewriter) {
   return AssertLikeOp::canonicalize<ClockedCoverOp>(op, rewriter);
 }
 
+//===----------------------------------------------------------------------===//
+// CircuitRelationCheckOp
+//===----------------------------------------------------------------------===//
+
+template <typename OpTy>
+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() !=
+  return verifyCircuitRelationCheckOpRegions(*this);
-      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 success();
+//===----------------------------------------------------------------------===//
+// RefinementCheckingOp
+//===----------------------------------------------------------------------===//
+
+LogicalResult RefinementCheckingOp::verifyRegions() {
+  return verifyCircuitRelationCheckOpRegions(*this);
 }
 
 //===----------------------------------------------------------------------===//

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() {

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
 //===----------------------------------------------------------------------===//

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):