[circt-lec] Fixed equivalence check for multiple outputs (#5358)

Adapted solver constraints to ensure all outputs must be equal.

integration_test/circt-lec/hw.mlir

@@ -40,3 +40,28 @@ hw.module @notnot(%in: i1) -> (out: i1) {
 // hw.output
 //  RUN: circt-lec %s -c1=basic -c2=basic -v=false | FileCheck %s --check-prefix=HW_OUTPUT
 //  HW_OUTPUT: c1 == c2
+
+
+hw.module @constZeroZero(%in: i1) -> (o1: i1, o2: i1) {
+  %zero = hw.constant 0 : i1
+  hw.output %zero, %zero : i1, i1
+}
+
+hw.module @xorZeroZero(%in: i1) -> (o1: i1, o2: i1) {
+  %zero = comb.xor bin %in, %in : i1
+  hw.output %zero, %zero : i1, i1
+}
+
+hw.module @constZeroOne(%in: i1) -> (o1: i1, o2: i1) {
+  %zero = hw.constant 0 : i1
+  %one  = hw.constant 1 : i1
+  hw.output %zero, %one : i1, i1
+}
+
+// Equivalent modules with two outputs
+//  RUN: circt-lec %s -c1=constZeroZero -c2=xorZeroZero -v=false | FileCheck %s --check-prefix=TWOOUTPUTS
+//  TWOOUTPUTS: c1 == c2
+
+// Modules with one equivalent and one non-equivalent output
+//  RUN: not circt-lec %s -c1=constZeroZero -c2=constZeroOne -v=false | FileCheck %s --check-prefix=TWOOUTPUTSFAIL
+//  TWOOUTPUTSFAIL: c1 != c2

lib/LogicalEquivalence/Solver.cpp

@@ -173,6 +173,8 @@ LogicalResult Solver::constrainCircuits() {
     return failure();
   }
 
+  z3::expr_vector outputTerms(context);
+
   const auto *c1outIt = c1Outputs.begin();
   const auto *c2outIt = c2Outputs.begin();
   for (unsigned i = 0; i < nc1Outputs; i++) {
@@ -182,8 +184,11 @@ LogicalResult Solver::constrainCircuits() {
       return failure();
     }
     // Their ith outputs have to be equivalent.
-    solver.add(*c1outIt++ != *c2outIt++);
+    outputTerms.push_back(*c1outIt++ != *c2outIt++);
   }
 
+  // The circuits are not equivalent iff any of the outputs is not equal
+  solver.add(z3::mk_or(outputTerms));
+
   return success();
 }