[circt-lec] Report failing points

[uenoku]

$ cat bar.mlir
hw.module @A(out out_1: i12, out out_2: i12) {
  %0 = hw.constant 2: i12
  hw.output %0, %0 : i12, i12
}

hw.module @B(out out_1 : i12, out out_2: i12) {
  %0 = hw.constant 2: i12
  %1 = hw.constant 3: i12
  hw.output %0, %1 : i12, i12
}
$ circt-lec bar.mlir --c1 A --c2 B --shared-libs=z3/build/libz3.so
c1 != c2

Right now it only tells us yes or no, so it would be nice to report failing points ideally with (executable) counter examples

[hovind]

$ cat bar.mlir
hw.module @A(out out_1: i12, out out_2: i12) {
  %0 = hw.constant 2: i12
  hw.output %0, %0 : i12, i12
}

hw.module @B(out out_1 : i12, out out_2: i12) {
  %0 = hw.constant 2: i12
  %1 = hw.constant 3: i12
  hw.output %0, %1 : i12, i12
}
$ circt-lec bar.mlir --c1 A --c2 B --shared-libs=z3/build/libz3.so
c1 != c2

Right now it only tells us yes or no, so it would be nice to report failing points ideally with (executable) counter examples

A very crude way I've done this locally is

diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td
index 7b83a6dcc..27e3cfee9 100644
--- a/include/circt/Dialect/Verif/VerifOps.td
+++ b/include/circt/Dialect/Verif/VerifOps.td
@@ -237,6 +237,8 @@ def LogicEquivalenceCheckingOp : VerifOp<"lec", [
   }];
 
   let results = (outs I1:$areEquivalent);
+  let arguments = (ins StrArrayAttr:$inputNames);
+
   let regions = (region SizedRegion<1>:$firstCircuit,
                         SizedRegion<1>:$secondCircuit);
 
diff --git a/lib/Conversion/VerifToSMT/VerifToSMT.cpp b/lib/Conversion/VerifToSMT/VerifToSMT.cpp
index 57ef512d1..ee5b86666 100644
--- a/lib/Conversion/VerifToSMT/VerifToSMT.cpp
+++ b/lib/Conversion/VerifToSMT/VerifToSMT.cpp
@@ -106,8 +106,8 @@ struct LogicEquivalenceCheckingOpConversion
 
     // Second, create the symbolic values we replace the block arguments with
     SmallVector<Value> inputs;
-    for (auto arg : adaptor.getFirstCircuit().getArguments())
-      inputs.push_back(rewriter.create<smt::DeclareFunOp>(loc, arg.getType()));
+    for (auto [arg, prefix] : llvm::zip(adaptor.getFirstCircuit().getArguments(), adaptor.getInputNames()))
+      inputs.push_back(rewriter.create<smt::DeclareFunOp>(loc, arg.getType(), cast<StringAttr>(prefix)));
 
     // Third, inline the blocks
     // Note: the argument value replacement does not happen immediately, but
diff --git a/lib/Tools/circt-lec/ConstructLEC.cpp b/lib/Tools/circt-lec/ConstructLEC.cpp
index d4f50df53..0828c3a40 100644
--- a/lib/Tools/circt-lec/ConstructLEC.cpp
+++ b/lib/Tools/circt-lec/ConstructLEC.cpp
@@ -110,7 +110,7 @@ void ConstructLECPass::runOnOperation() {
 
   builder.createBlock(&entryFunc.getBody());
 
-  auto lecOp = builder.create<verif::LogicEquivalenceCheckingOp>(loc);
+  auto lecOp = builder.create<verif::LogicEquivalenceCheckingOp>(loc, ArrayAttr::get(builder.getContext(), moduleA.getModuleType().getInputNames()));
   Value areEquivalent = lecOp.getAreEquivalent();
   builder.cloneRegionBefore(moduleA.getBody(), lecOp.getFirstCircuit(),
                             lecOp.getFirstCircuit().end());
diff --git a/tools/circt-lec/circt-lec.cpp b/tools/circt-lec/circt-lec.cpp
index 3a8e0c0ff..624a22963 100644
--- a/tools/circt-lec/circt-lec.cpp
+++ b/tools/circt-lec/circt-lec.cpp
@@ -106,6 +106,10 @@ static cl::list<std::string> sharedLibs{
     "shared-libs", llvm::cl::desc("Libraries to link dynamically"),
     cl::MiscFlags::CommaSeparated, llvm::cl::cat(mainCategory)};
 
+static llvm::cl::opt<bool> verboseSolver{
+    "verbose-solver", llvm::cl::desc("Print verbose solver output"),
+    llvm::cl::init(false), llvm::cl::cat(mainCategory)};
+
 #else
 
 enum OutputFormat { OutputMLIR, OutputLLVM, OutputSMTLIB };
@@ -226,7 +230,9 @@ static LogicalResult executeLEC(MLIRContext &context) {
   pm.addPass(createSimpleCanonicalizerPass());
 
   if (outputFormat != OutputMLIR && outputFormat != OutputSMTLIB) {
-    pm.addPass(createLowerSMTToZ3LLVM());
+    LowerSMTToZ3LLVMOptions lowerSMTOptions;
+    lowerSMTOptions.debug = verboseSolver;
+    pm.addPass(createLowerSMTToZ3LLVM(lowerSMTOptions));
     pm.addPass(createCSEPass());
     pm.addPass(createSimpleCanonicalizerPass());
     pm.addPass(LLVM::createDIScopeForLLVMFuncOpPass());

which outputs something like

$ ./build/bin/circt-lec --verbose-solver --c1=adder --c2=completeAdder /tmp/easy.mlir --shared-libs=/usr/lib/x86_64-linux-gnu/libz3.so
------------------------------------ Solver ------------------------------------
(declare-fun in2!1 () (_ BitVec 2))
(declare-fun in1!0 () (_ BitVec 2))
(assert (let ((a!1 (ite (= (ite (= #b01 in2!1) #b1 #b0) #b1) #b01 (bvadd in1!0 in2!1)))
      (a!2 (concat (bvxor ((_ extract 1 1) in1!0)
                          ((_ extract 1 1) in2!1)
                          (bvand ((_ extract 0 0) in1!0)
                                 ((_ extract 0 0) in2!1)))
                   (bvxor ((_ extract 0 0) in1!0) ((_ extract 0 0) in2!1)))))
  (distinct a!1 a!2)))

--------------------------------------------------------------------------------
------------------------------------ Model -------------------------------------
in1!0 -> #b10
in2!1 -> #b01

--------------------------------------------------------------------------------
c1 != c2

I understand that this is quite far from what we ultimately want, but it has been useful for me, so I was wondering if there was any interest in upstreaming until we get something better?