From f958c7e0da70a7d21c7d7066bfd4f83ffbbed0e3 Mon Sep 17 00:00:00 2001
From: Hideto Ueno <uenoku.tokotoko@gmail.com>
Date: Sat, 16 May 2026 20:47:19 -0700
Subject: [PATCH] [circt-lec] Lower comb truth tables before SMT conversion

---
 test/Tools/circt-lec/truth-table.mlir | 14 ++++++++++++++
 tools/circt-lec/CMakeLists.txt        |  1 +
 tools/circt-lec/circt-lec.cpp         |  2 ++
 3 files changed, 17 insertions(+)
 create mode 100644 test/Tools/circt-lec/truth-table.mlir

diff --git a/test/Tools/circt-lec/truth-table.mlir b/test/Tools/circt-lec/truth-table.mlir
new file mode 100644
index 000000000000..ba3ca2da70ce
--- /dev/null
+++ b/test/Tools/circt-lec/truth-table.mlir
@@ -0,0 +1,14 @@
+// RUN: circt-lec %s --c1 table --c2 xor --emit-mlir | FileCheck %s
+
+// CHECK-LABEL: smt.solver()
+// CHECK-NOT: comb.truth_table
+// CHECK: smt.ite
+hw.module @table(in %a : i1, in %b : i1, out result : i1) {
+  %0 = comb.truth_table %a, %b -> [false, true, true, false]
+  hw.output %0 : i1
+}
+
+hw.module @xor(in %a : i1, in %b : i1, out result : i1) {
+  %0 = comb.xor %a, %b : i1
+  hw.output %0 : i1
+}
diff --git a/tools/circt-lec/CMakeLists.txt b/tools/circt-lec/CMakeLists.txt
index e5fb42ac9c98..31c174a95f9d 100644
--- a/tools/circt-lec/CMakeLists.txt
+++ b/tools/circt-lec/CMakeLists.txt
@@ -14,6 +14,7 @@ target_link_libraries(circt-lec
   PRIVATE
   CIRCTComb
   CIRCTCombToSMT
+  CIRCTCombTransforms
   CIRCTDatapath
   CIRCTDatapathToSMT
   CIRCTEmitTransforms
diff --git a/tools/circt-lec/circt-lec.cpp b/tools/circt-lec/circt-lec.cpp
index 1a8e1626182d..d8d1637258c2 100644
--- a/tools/circt-lec/circt-lec.cpp
+++ b/tools/circt-lec/circt-lec.cpp
@@ -19,6 +19,7 @@
 #include "circt/Conversion/SynthToComb.h"
 #include "circt/Conversion/VerifToSMT.h"
 #include "circt/Dialect/Comb/CombDialect.h"
+#include "circt/Dialect/Comb/CombPasses.h"
 #include "circt/Dialect/Datapath/DatapathDialect.h"
 #include "circt/Dialect/Emit/EmitDialect.h"
 #include "circt/Dialect/Emit/EmitPasses.h"
@@ -238,6 +239,7 @@ static LogicalResult executeLEC(MLIRContext &context) {
     pm.addPass(createConstructLEC(opts));
   }
   pm.addPass(createConvertSynthToComb());
+  pm.addPass(comb::createLowerComb());
   pm.addPass(createConvertHWToSMT());
   pm.addPass(createConvertDatapathToSMT());
   pm.addPass(createConvertCombToSMT());