llvm · fabianschuiki · May 24, 2023 · Jan 13, 2023 · Jan 20, 2023 · Jan 27, 2023
diff --git a/cmake/modules/AddCIRCT.cmake b/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()
diff --git a/cmake/modules/CMakeLists.txt b/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}")

diff --git a/tools/circt-lec/Circuit.h → include/circt/LogicalEquivalence/Circuit.h b/tools/circt-lec/Circuit.h → include/circt/LogicalEquivalence/Circuit.h
diff --git a/tools/circt-lec/LogicExporter.h → .../circt/LogicalEquivalence/LogicExporter.h b/tools/circt-lec/LogicExporter.h → .../circt/LogicalEquivalence/LogicExporter.h
diff --git a/tools/circt-lec/Solver.h → include/circt/LogicalEquivalence/Solver.h b/tools/circt-lec/Solver.h → include/circt/LogicalEquivalence/Solver.h
diff --git a/tools/circt-lec/Utility.h → include/circt/LogicalEquivalence/Utility.h b/tools/circt-lec/Utility.h → include/circt/LogicalEquivalence/Utility.h
diff --git a/lib/CMakeLists.txt b/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)

diff --git a/lib/LogicalEquivalence/CMakeLists.txt b/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()
diff --git a/tools/circt-lec/Circuit.cpp → lib/LogicalEquivalence/Circuit.cpp b/tools/circt-lec/Circuit.cpp → 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"

diff --git a/tools/circt-lec/LogicExporter.cpp → lib/LogicalEquivalence/LogicExporter.cpp b/tools/circt-lec/LogicExporter.cpp → lib/LogicalEquivalence/LogicExporter.cpp
@@ -10,10 +10,10 @@
 ///
 //===----------------------------------------------------------------------===//
 
-#include "LogicExporter.h
6D4E
"
-#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"

diff --git a/tools/circt-lec/Solver.cpp → lib/LogicalEquivalence/Solver.cpp b/tools/circt-lec/Solver.cpp → 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>

diff --git a/tools/circt-lec/CMakeLists.txt b/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

diff --git a/tools/circt-lec/circt-lec.cpp b/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"