[circt-lec] Port to SMT dialect based compiler pipeline (#6908)

Author: maerhart

CMakeLists.txt

@@ -464,13 +464,13 @@ endif()
 llvm_canonicalize_cmake_booleans(CIRCT_LLHD_SIM_ENABLED)
 
 #-------------------------------------------------------------------------------
-# circt-lec Configuration
+# Z3Lib Configuration (for circt-lec and SMT dialect integration tests)
 #-------------------------------------------------------------------------------
 
-# If circt-lec hasn't been explicitly disabled, find it.
-option(CIRCT_LEC_DISABLE "Disable the Logical Equivalence Checker" OFF)
-if(CIRCT_LEC_DISABLE)
-  message(STATUS "Disabling circt-lec")
+# If z3 hasn't been explicitly disabled, find it.
+option(Z3_DISABLE "Disable the z3 tests.")
+if (Z3_DISABLE)
+  message(STATUS "Disabling tests requiring z3.")
 else()
   if(Z3_DIR)
     # Search and load the package configuration file in the specified directory.
@@ -485,15 +485,13 @@ else()
     # Attempt initialising Z3 according to LLVM's `FindZ3` CMake module.
     find_package(Z3)
   endif()
-  
+
   if(Z3_FOUND)
     SET(CIRCT_LEC_Z3_VER 4.8.11)
     if(Z3_VERSION_STRING VERSION_LESS ${CIRCT_LEC_Z3_VER})
       message(WARNING "Cannot build circt-lec with outdated Z3 version ${Z3_VERSION_STRING}, requires ${CIRCT_LEC_Z3_VER}.")
     else()
       message(STATUS "Z3 identified as a logical backend.")
-      # Signal to proceed building circt-lec.
-      set(CIRCT_LEC_ENABLED ON)
     endif()
   endif()
 endif()

include/circt/Conversion/Passes.td

@@ -701,7 +701,7 @@ def ConvertCombToSMT : Pass<"convert-comb-to-smt", "mlir::ModuleOp"> {
 
 def ConvertHWToSMT : Pass<"convert-hw-to-smt", "mlir::ModuleOp"> {
   let summary = "Convert HW ops and constants to SMT ops";
-  let dependentDialects = ["smt::SMTDialect"];
+  let dependentDialects = ["smt::SMTDialect", "mlir::func::FuncDialect"];
 }
 
 //===----------------------------------------------------------------------===//

include/circt/Dialect/SMT/SMTAttributes.h

@@ -13,6 +13,16 @@
 #include "mlir/IR/BuiltinAttributeInterfaces.h"
 #include "mlir/IR/BuiltinAttributes.h"
 
+namespace circt {
+namespace smt {
+namespace detail {
+
+struct BitVectorAttrStorage;
+
+} // namespace detail
+} // namespace smt
+} // namespace circt
+
 #define GET_ATTRDEF_CLASSES
 #include "circt/Dialect/SMT/SMTAttributes.h.inc"
 

include/circt/Dialect/SMT/SMTAttributes.td

@@ -50,6 +50,16 @@ def BitVectorAttr : AttrDef<SMTDialect, "BitVector", [
   let hasCustomAssemblyFormat = true;
   let genVerifyDecl = true;
 
+  // We need to manually define the storage class because the generated one is
+  // buggy (because the APInt asserts matching bitwidth in the `==` operator and
+  // the generated storage uses that directly.
+  // Alternatively: add a type parameter to redundantly store the bitwidth of
+  // of the attribute type, it it's in the order before the 'value' it will be
+  // checked before the APInt equality (this is the reason it works for the
+  // builtin integer attribute), but would be more fragile (and we'd store
+  // duplicate data).
+  let genStorageClass = false;
+
   let builders = [
     AttrBuilder<(ins "llvm::StringRef":$value)>,
     AttrBuilder<(ins "uint64_t":$value, "unsigned":$width)>,