[circt-lec] Move `circt-lec` files to CIRCT library (#4544)

This moves most of the circt-lec code into a CIRCT library. No existing library directories seemed appropriate, hence the addition of the Verification directories.

---------

Co-authored-by: frog-in-the-well <106834163+frog-in-the-well@users.noreply.github.com>

cmake/modules/AddCIRCT.cmake

@@ -59,3 +59,8 @@ function(add_circt_translation_library name)
   set_property(GLOBAL APPEND PROPERTY CIRCT_TRANSLATION_LIBS ${name})
   add_circt_library(${ARGV} DEPENDS circt-headers)
 endfunction()
+
+function(add_circt_verification_library name)
+  set_property(GLOBAL APPEND PROPERTY CIRCT_VERIFICATION_LIBS ${name})
+  add_circt_library(${ARGV} DEPENDS circt-headers)
+endfunction()

cmake/modules/CMakeLists.txt

@@ -22,6 +22,7 @@ get_property(CIRCT_DIALECT_LIBS GLOBAL PROPERTY CIRCT_DIALECT_LIBS)
 get_property(CIRCT_CONVERSION_LIBS GLOBAL PROPERTY CIRCT_CONVERSION_LIBS)
 get_property(CIRCT_TRANSLATION_LIBS GLOBAL PROPERTY CIRCT_TRANSLATION_LIBS)
 get_property(CIRCT_ANALYSIS_LIBS GLOBAL PROPERTY CIRCT_ANALYSIS_LIBS)
+get_property(CIRCT_VERIFICATION_LIBS GLOBAL PROPERTY CIRCT_VERIFICATION_LIBS)
 
 # Generate CIRCTConfig.cmake for the build tree.
 set(CIRCT_CONFIG_CMAKE_DIR "${circt_cmake_builddir}")

lib/CMakeLists.txt

@@ -7,6 +7,7 @@ add_subdirectory(Bindings)
 add_subdirectory(CAPI)
 add_subdirectory(Conversion)
 add_subdirectory(Dialect)
+add_subdirectory(LogicalEquivalence)
 add_subdirectory(Firtool)
 add_subdirectory(Reduce)
 add_subdirectory(Scheduling)

lib/LogicalEquivalence/CMakeLists.txt

@@ -0,0 +1,25 @@
+if(CIRCT_LEC_ENABLED)
+  add_circt_verification_library(CIRCTLogicalEquivalence
+    Solver.cpp
+    Circuit.cpp
+    LogicExporter.cpp
+
+    LINK_COMPONENTS
+    Core
+
+    LINK_LIBS
+    ${Z3_LIBRARIES}
+    
+    LINK_LIBS PUBLIC
+    MLIRTransforms
+    MLIRTranslateLib
+    CIRCTComb
+    CIRCTHW
+    CIRCTSupport
+  )
+  target_include_directories(CIRCTLogicalEquivalence
+    PRIVATE
+    ${Z3_INCLUDE_DIR}
+    ${Z3_CXX_INCLUDE_DIRS}
+  )
+endif()

lib/LogicalEquivalence/Circuit.cpp

@@ -11,10 +11,10 @@
 ///
 //===----------------------------------------------------------------------===//
 
-#include "Circuit.h"
-#include "LogicExporter.h"
-#include "Solver.h"
-#include "Utility.h"
+#include "circt/LogicalEquivalence/Circuit.h"
+#include "circt/LogicalEquivalence/LogicExporter.h"
+#include "circt/LogicalEquivalence/Solver.h"
+#include "circt/LogicalEquivalence/Utility.h"
 #include "mlir/IR/Builders.h"
 
 #define DEBUG_TYPE "lec-circuit"

lib/LogicalEquivalence/LogicExporter.cpp

@@ -10,10 +10,10 @@
 ///
 //===----------------------------------------------------------------------===//
 
-#include "LogicExporter.h"
-#include "Circuit.h"
-#include "Solver.h"
-#include "Utility.h"
+#include "circt/LogicalEquivalence/LogicExporter.h"
+#include "circt/LogicalEquivalence/Circuit.h"
+#include "circt/LogicalEquivalence/Solver.h"
+#include "circt/LogicalEquivalence/Utility.h"
 #include "llvm/ADT/TypeSwitch.h"
 
 #define DEBUG_TYPE "lec-exporter"

lib/LogicalEquivalence/Solver.cpp

@@ -10,10 +10,10 @@
 ///
 //===----------------------------------------------------------------------===//
 
-#include "Solver.h"
-#include "Circuit.h"
-#include "LogicExporter.h"
-#include "Utility.h"
+#include "circt/LogicalEquivalence/Solver.h"
+#include "circt/LogicalEquivalence/Circuit.h"
+#include "circt/LogicalEquivalence/LogicExporter.h"
+#include "circt/LogicalEquivalence/Utility.h"
 #include "mlir/IR/Builders.h"
 #include <string>
 #include <z3++.h>

tools/circt-lec/CMakeLists.txt

@@ -2,27 +2,14 @@
 if(CIRCT_LEC_ENABLED)
   add_llvm_tool(circt-lec
     circt-lec.cpp
-    Circuit.cpp
-    LogicExporter.cpp
-    Solver.cpp
   )
 
   target_link_libraries(circt-lec
     PRIVATE
-    MLIRTransforms
-    MLIRTranslateLib
-    CIRCTComb
-    CIRCTHW
-    CIRCTSupport
+    CIRCTLogicalEquivalence
     ${Z3_LIBRARIES}
   )
 
-  target_include_directories(circt-lec SYSTEM
-    PRIVATE
-    ${Z3_INCLUDE_DIR}
-    ${Z3_CXX_INCLUDE_DIRS}
-  )
-
   # Correct the runpath when linking shared libraries.
   if(BUILD_SHARED_LIBS)
     set_target_properties(circt-lec PROPERTIES

tools/circt-lec/circt-lec.cpp

@@ -12,10 +12,10 @@
 ///
 //===----------------------------------------------------------------------===//
 
-#include "LogicExporter.h"
-#include "Solver.h"
-#include "Utility.h"
 #include "circt/InitAllDialects.h"
+#include "circt/LogicalEquivalence/LogicExporter.h"
+#include "circt/LogicalEquivalence/Solver.h"
+#include "circt/LogicalEquivalence/Utility.h"
 #include "circt/Support/Version.h"
 #include "mlir/IR/Diagnostics.h"
 #include "mlir/IR/OwningOpRef.h"