[Verif][LEC] Make LECOp result optional to avoid unsafe conversion (#8701)

#8497 introduced a lowering pattern for the LogicEquivalenceCheckingOp which changes behavior depending on whether the result of the operation is used. This is generally not safe and can cause lowerings to erroneously consider the result to be used/unused. The pattern must only depend on the operation itself, not on its def-use context.

By making the result of the operation optional, we should be able to retain the current behavior. In the pattern op.use_empty() is simply replaced by op.getNumResults() == 0. However, we now have to decide at the point of creating the LogicEquivalenceCheckingOp whether the result should be made accessible to the IR.


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

Author: fzi-hielscher

include/circt/Dialect/Verif/VerifOps.td

@@ -236,20 +236,30 @@ def LogicEquivalenceCheckingOp : VerifOp<"lec", [
     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
     constructed and compared for identity, etc.
-    
+
     The number and types of the inputs and outputs of the two circuits (and thus
     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
+    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 I1:$areEquivalent);
+  let results = (outs Optional<I1>:$areEquivalent);
   let regions = (region SizedRegion<1>:$firstCircuit,
                         SizedRegion<1>:$secondCircuit);
 
   let assemblyFormat = [{
-    attr-dict `first` $firstCircuit `second` $secondCircuit
+    attr-dict (`:` type($areEquivalent)^)?
+    `first` $firstCircuit
+    `second` $secondCircuit
   }];
 
+  let builders = [OpBuilder<(ins "bool":$hasResult), [{
+      build($_builder, $_state, hasResult ? $_builder.getI1Type() : Type{} );
+    }]>];
+
   let hasRegionVerifier = true;
 }
 

lib/Conversion/VerifToSMT/VerifToSMT.cpp

@@ -93,12 +93,12 @@ struct LogicEquivalenceCheckingOpConversion
       return success();
     }
 
-    auto unusedResult = op.use_empty();
+    auto hasNoResult = op.getNumResults() == 0;
 
     // Solver will only return a result when it is used to check the returned
     // value.
     smt::SolverOp solver;
-    if (unusedResult)
+    if (hasNoResult)
       solver = rewriter.create<smt::SolverOp>(loc, TypeRange{}, ValueRange{});
     else
       solver = rewriter.create<smt::SolverOp>(loc, rewriter.getI1Type(),
@@ -163,7 +163,7 @@ struct LogicEquivalenceCheckingOpConversion
     // operations empty. If the result is used, we create a check operation with
     // the result type of the operation and yield the result of the check
     // operation.
-    if (unusedResult) {
+    if (hasNoResult) {
       auto checkOp = rewriter.create<smt::CheckOp>(loc, TypeRange{});
       rewriter.createBlock(&checkOp.getSatRegion());
       rewriter.create<smt::YieldOp>(loc);

lib/Tools/circt-lec/ConstructLEC.cpp

@@ -35,7 +35,7 @@ struct ConstructLECPass
   void runOnOperation() override;
   hw::HWModuleOp lookupModule(StringRef name);
   Value constructMiter(OpBuilder builder, Location loc, hw::HWModuleOp moduleA,
-                       hw::HWModuleOp moduleB);
+                       hw::HWModuleOp moduleB, bool withResult);
 };
 } // namespace
 
@@ -69,10 +69,13 @@ hw::HWModuleOp ConstructLECPass::lookupModule(StringRef name) {
 
 Value ConstructLECPass::constructMiter(OpBuilder builder, Location loc,
                                        hw::HWModuleOp moduleA,
-                                       hw::HWModuleOp moduleB) {
+                                       hw::HWModuleOp moduleB,
+                                       bool withResult) {
+
   // Create the miter circuit that return equivalence result.
-  auto lecOp = builder.create<verif::LogicEquivalenceCheckingOp>(loc);
-  Value areEquivalent = lecOp.getAreEquivalent();
+  auto lecOp =
+      builder.create<verif::LogicEquivalenceCheckingOp>(loc, withResult);
+
   builder.cloneRegionBefore(moduleA.getBody(), lecOp.getFirstCircuit(),
                             lecOp.getFirstCircuit().end());
   builder.cloneRegionBefore(moduleB.getBody(), lecOp.getSecondCircuit(),
@@ -97,7 +100,7 @@ Value ConstructLECPass::constructMiter(OpBuilder builder, Location loc,
   sortTopologically(&lecOp.getFirstCircuit().front());
   sortTopologically(&lecOp.getSecondCircuit().front());
 
-  return areEquivalent;
+  return withResult ? lecOp.getAreEquivalent() : Value{};
 }
 
 void ConstructLECPass::runOnOperation() {
@@ -121,7 +124,7 @@ void ConstructLECPass::runOnOperation() {
 
   // Only construct the miter with no additional insertions.
   if (insertMode == lec::InsertAdditionalModeEnum::None) {
-    constructMiter(builder, loc, moduleA, moduleB);
+    constructMiter(builder, loc, moduleA, moduleB, /*withResult*/ false);
     return;
   }
 
@@ -157,7 +160,9 @@ void ConstructLECPass::runOnOperation() {
   builder.createBlock(&entryFunc.getBody());
 
   // Create the miter circuit that returns equivalence result.
-  auto areEquivalent = constructMiter(builder, loc, moduleA, moduleB);
+  auto areEquivalent =
+      constructMiter(builder, loc, moduleA, moduleB, /*withResult*/ true);
+  assert(!!areEquivalent && "Expected LEC operation with result.");
 
   // TODO: we should find a more elegant way of reporting the result than
   // already inserting some LLVM here

test/Conversion/VerifToSMT/verif-to-smt.mlir

@@ -54,7 +54,7 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) {
   // CHECK: smt.yield [[FALSE]]
   // CHECK: smt.yield [[TRUE]]
   // CHECK: smt.yield [[V8]] :
-  %1 = verif.lec first {
+  %1 = verif.lec : i1 first {
   ^bb0(%arg1: i32, %arg2: i32):
     verif.yield %arg1, %arg2 : i32, i32
   } second {
@@ -67,23 +67,23 @@ func.func @test_lec(%arg0: !smt.bv<1>) -> (i1, i1, i1) {
   // CHECK: [[V9:%.+]] = smt.declare_fun : !smt.bv<32>
   // CHECK: [[V10:%.+]] = smt.distinct [[V9]], [[V9]] : !smt.bv<32>
   // CHECK: smt.assert [[V10]]
-  %2 = verif.lec first {
+  %2 = verif.lec : i1  first {
   ^bb0(%arg1: i32):
     verif.yield %arg1 : i32
   } second {
   ^bb0(%arg1: i32):
     verif.yield %arg1 : i32
   }
 
-  %3 = verif.lec first {
+  %3 = verif.lec : i1 first {
   ^bb0(%arg1: i32):
     verif.yield
   } second {
   ^bb0(%arg1: i32):
     verif.yield
   }
 
-  %4 = verif.lec first {
+  verif.lec first {
   ^bb0(%arg1: i32):
     verif.yield %arg1 : i32
   } second {

test/Tools/circt-lec/construct-lec.mlir

@@ -11,7 +11,7 @@ hw.module @modB0(in %in0: i32, in %in1: i32, out out: i32) {
 }
 
 // CHECK: func.func @modA0() {
-// CHECK:   [[V0:%.+]] = verif.lec first {
+// CHECK:   [[V0:%.+]] = verif.lec : i1 first {
 // CHECK:   ^bb0([[ARG0:%.+]]: i32, [[ARG1:%.+]]: i32):
 // CHECK:     [[V1:%.+]] = comb.add [[ARG0]], [[ARG1]]
 // CHECK:     verif.yield [[V1]]
@@ -48,7 +48,7 @@ hw.module @modB1() {
 }
 
 // CHECK1: func.func @modA1() {
-// CHECK1:   [[V0:%.+]] = verif.lec first {
+// CHECK1:   [[V0:%.+]] = verif.lec : i1 first {
 // CHECK1:   } second {
 // CHECK1:   }
 // CHECK1:   [[V1:%.+]] = llvm.mlir.addressof @"c1 == c2\0A" : !llvm.ptr
@@ -61,5 +61,5 @@ hw.module @modB1() {
 // RUN: circt-opt --construct-lec="first-module=modA0 second-module=modB0 insert-mode=none" %s | FileCheck %s --check-prefix=CHECK2
 
 // CHECK2-NOT: func.func
-// CHECK2: verif.lec
+// CHECK2: verif.lec first
 // CHECK2-NOT: llvm.mlir.global