[HWToSMT][circt-lec] Resolve transitive !smt.bool -> i1 -> !smt.bv<1>…

… casts. (#7006)

integration_test/circt-lec/comb.mlir

@@ -68,7 +68,21 @@ hw.module @decomposedAnd(in %in1: i1, in %in2: i1, out out: i1) {
 // TODO
 
 // comb.icmp
-// TODO
+//  RUN: circt-lec %s -c1=eqInv -c2=constFalse --shared-libs=%libz3 | FileCheck %s --check-prefix=COMB_ICMPEQ
+//  COMB_ICMPEQ: c1 == c2
+hw.module @eqInv(in %a: i8, out eq: i1) {
+  %ones = hw.constant -1 : i8
+  %inv_a = comb.xor bin %a, %ones : i8
+  %eq = comb.icmp bin eq %a, %inv_a : i8
+  hw.output %eq : i1
+}
+
+hw.module @constFalse(in %a: i8, out eq: i1) {
+  %eq = hw.constant false
+  hw.output %eq : i1
+}
+
+// TODO: Other icmp predicates
 
 // comb.mods
 // TODO

lib/Conversion/HWToSMT/HWToSMT.cpp

@@ -145,6 +145,32 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) {
         return builder.create<smt::IteOp>(loc, inputs[0], constOne, constZero);
       });
 
+  // Convert an unrealized conversion cast from 'smt.bool' to i1
+  // into a direct conversion from 'smt.bool' to 'smt.bv<1>'.
+  converter.addTargetMaterialization(
+      [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs,
+          Location loc) -> std::optional<Value> {
+        if (inputs.size() != 1 || resultType.getWidth() != 1)
+          return std::nullopt;
+
+        auto intType = dyn_cast<IntegerType>(inputs[0].getType());
+        if (!intType || intType.getWidth() != 1)
+          return std::nullopt;
+
+        auto castOp =
+            inputs[0].getDefiningOp<mlir::UnrealizedConversionCastOp>();
+        if (!castOp || castOp.getInputs().size() != 1)
+          return std::nullopt;
+
+        if (!isa<smt::BoolType>(castOp.getInputs()[0].getType()))
+          return std::nullopt;
+
+        Value constZero = builder.create<smt::BVConstantOp>(loc, 0, 1);
+        Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
+        return builder.create<smt::IteOp>(loc, castOp.getInputs()[0], constOne,
+                                          constZero);
+      });
+
   // Convert a 'smt.bv<1>'-typed value to a 'smt.bool'-typed value
   converter.addTargetMaterialization(
       [&](OpBuilder &builder, smt::BoolType resultType, ValueRange inputs,