[FSM] Lower FSM to SMT dialect

include/circt/Conversion/FSMToSMT.h

@@ -0,0 +1,26 @@
+//===- FSMToSMT.h - FSM to SMT-LIB conversions ------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_CONVERSION_FSMTOSMT_FSMTOSMT_H
+#define CIRCT_CONVERSION_FSMTOSMT_FSMTOSMT_H
+
+#include <memory>
+
+namespace mlir {
+class Pass;
+} // namespace mlir
+
+namespace circt {
+
+#define GEN_PASS_DECL_CONVERTFSMTOSMT
+#include "circt/Conversion/Passes.h.inc"
+
+std::unique_ptr<mlir::Pass> createConvertFSMToSMTPass();
+} // namespace circt
+
+#endif // CIRCT_CONVERSION_FSMTOSMT_FSMTOSMT_H

include/circt/Conversion/Passes.h

@@ -32,6 +32,7 @@
 #include "circt/Conversion/ExportVerilog.h"
 #include "circt/Conversion/FIRRTLToHW.h"
 #include "circt/Conversion/FSMToCore.h"
+#include "circt/Conversion/FSMToSMT.h"
 #include "circt/Conversion/FSMToSV.h"
 #include "circt/Conversion/HWArithToHW.h"
 #include "circt/Conversion/HWToBTOR2.h"

include/circt/Conversion/Passes.td

@@ -385,6 +385,20 @@ def ConvertFSMToSV : Pass<"convert-fsm-to-sv", "mlir::ModuleOp"> {
   ];
 }
 
+//===----------------------------------------------------------------------===//
+// FSMToSMT
+//===----------------------------------------------------------------------===//
+
+def ConvertFSMToSMT : Pass<"convert-fsm-to-smt", "mlir::ModuleOp"> {
+  let summary = "Convert FSM to SMT - Safety Properties";
+  let constructor = "circt::createConvertFSMToSMTPass()";
+  let dependentDialects = ["circt::comb::CombDialect", "mlir::smt::SMTDialect",
+                           "circt::verif::VerifDialect"];
+  let options = [Option<"withTime", "with-time", "bool", "false",
+                        "whether to include a time paramter in the relation">,
+  ];
+}
+
 //===----------------------------------------------------------------------===//
 // CoreToFSM
 //===----------------------------------------------------------------------===//

lib/CAPI/Conversion/CMakeLists.txt

@@ -21,6 +21,7 @@ add_circt_public_c_api_library(CIRCTCAPIConversion
   CIRCTExportVerilog
   CIRCTFIRRTLToHW
   CIRCTFSMToSV
+  CIRCTFSMToSMT
   CIRCTFSMToCore
   CIRCTHandshakeToDC
   CIRCTHandshakeToHW

lib/CAPI/Dialect/CMakeLists.txt

@@ -203,6 +203,7 @@ add_circt_public_c_api_library(CIRCTCAPIFSM
   CIRCTFSM
   CIRCTFSMTransforms
   CIRCTFSMToSV
+  CIRCTFSMToSMT
   CIRCTCoreToFSM
   CIRCTFSMToCore
 )

lib/CAPI/Dialect/FSM.cpp

@@ -19,6 +19,7 @@ using namespace circt::fsm;
 void registerFSMPasses() {
   registerPasses();
   circt::registerConvertFSMToSVPass();
+  circt::registerConvertFSMToSMTPass();
   circt::registerConvertFSMToCorePass();
 }
 MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(FSM, fsm, FSMDialect)

lib/Conversion/CMakeLists.txt

@@ -18,6 +18,7 @@ add_subdirectory(ExportVerilog)
 add_subdirectory(FIRRTLToHW)
 add_subdirectory(FSMToCore)
 add_subdirectory(FSMToSV)
+add_subdirectory(FSMToSMT)
 add_subdirectory(HandshakeToDC)
 add_subdirectory(HandshakeToHW)
 add_subdirectory(HWArithToHW)

lib/Conversion/FSMToSMT/CMakeLists.txt

@@ -0,0 +1,19 @@
+add_circt_conversion_library(CIRCTFSMToSMT 
+    FSMToSMT.cpp
+
+    DEPENDS 
+    CIRCTConversionPassIncGen
+
+    LINK_COMPONENTS 
+    Core
+
+    LINK_LIBS PUBLIC 
+    MLIRSMT
+    CIRCTComb
+    CIRCTVerif
+    CIRCTHW
+    CIRCTEmit
+    CIRCTFSM
+    CIRCTSupport
+    MLIRTransforms
+)