[HW to BTOR2] btor2 conversion pass (#6378)

* Added missing tool in integration test

* Fixed formatting

* Fixed whitespace issue

* Fixed typo in VerilogGeneration.md

* Added skeleton for btor2 lowering pass

* added pattern match skeleton to lowering pass

* Added initial emission of inputs and hw::constant ops

* added constant emission

* added emission for most operations and final assertion

* Added support for muxes, assumptions and wire aliases

* Added support for inputs in btor2

* fixed bug in input generation

* added support for missing comb operations

* Changed input registration to allow for booleans

* Made input type check more robust

* WIP register state transition system generation

* Added support for registers

* refactored hardcoded string

* added names to btor2 states

* Added state initialization support

* Removed state initializer, it should be a firrtl construct and not a btor one

* Removed temporary file emission

* Added back accidentally removed btor2 string printing

* Ran clang-format

* Ran clang-format

* WIP refactored typeswitch

* refactored giant type switch

* Made all string litterals constexpr

* attempting to fix sanity check

* fixed variable name typo

* Attempting to satisfy clang-tidy

* renamed things to make clang happy

* inlined useless helper methods

* Clarified the necessity of important data structures in comments

* fixed formatting

* Changed pass into a Conversion pass

* refactored helper methods

* Checked for case where next is a port when emitted transitions

* Added newline at EOF

* Inherited visitors instead of using a big typeswitch

* Throw an error for unsupported ops and explicitly ignore the rest

* Removed unnecessary functions and refactored runOnOperation

* Fixed formatting

* Attempted to add some test

* Added in ops that weren't covered by visitors

* Added in missing declaration in header

* Included pass in CAPI CmakeLists

* Added infrastructure for btor integration tests

* Revert "Added infrastructure for btor integration tests"

This reverts commit a5ec3da.

* various nitpicking comments accounted for

* used generalized ids for btor2 testcase

* fixed typo in test

* updated test and found small bug

* clang-format

* added support for arbitrary resets

* Updated test to reflect new handling of reset

* Switched to a DFS strategy for emission

* Updated test to align with preemission of register declarations

* Removed gratuitous lookups.

* inlined a bunch of string constatns

* removed certain silent fails and added out of order test

include/circt/Conversion/HWToBTOR2.h

@@ -0,0 +1,32 @@
+//===- HWToBTOR2.h - HW to BTOR2 conversion pass ----------------*- 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
+//
+//===----------------------------------------------------------------------===//
+//
+// This file declares passes which together will convert the HW dialect to a
+// state transition system and emit it as a btor2 string.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_CONVERSION_HWTOBTOR2_H
+#define CIRCT_CONVERSION_HWTOBTOR2_H
+
+#include "mlir/IR/BuiltinOps.h"
+#include "mlir/Pass/Pass.h"
+
+namespace mlir {
+class Pass;
+} // namespace mlir
+
+using namespace mlir;
+
+namespace circt {
+std::unique_ptr<mlir::Pass> createConvertHWToBTOR2Pass(llvm::raw_ostream &os);
+std::unique_ptr<mlir::Pass> createConvertHWToBTOR2Pass();
+
+} // namespace circt
+
+#endif // CIRCT_CONVERSION_HWTOBTOR2_H

include/circt/Conversion/Passes.h

@@ -27,6 +27,7 @@
 #include "circt/Conversion/FIRRTLToHW.h"
 #include "circt/Conversion/FSMToSV.h"
 #include "circt/Conversion/HWArithToHW.h"
+#include "circt/Conversion/HWToBTOR2.h"
 #include "circt/Conversion/HWToLLHD.h"
 #include "circt/Conversion/HWToLLVM.h"
 #include "circt/Conversion/HWToSV.h"

include/circt/Conversion/Passes.td

@@ -563,6 +563,21 @@ def LowerHWToSV : Pass<"lower-hw-to-sv", "hw::HWModuleOp"> {
   let dependentDialects = ["sv::SVDialect"];
 }
 
+//===----------------------------------------------------------------------===//
+// HWToBTOR2
+//===----------------------------------------------------------------------===//
+
+def ConvertHWToBTOR2 : Pass<"convert-hw-to-btor2", "hw::HWModuleOp"> {
+  let summary = "Convert HW to BTOR2";
+  let description = [{
+    This pass converts a HW module into a state transition system that is then 
+    directly used to emit btor2. The output of this pass is thus a btor2 string.
+  }];
+  let constructor = "circt::createConvertHWToBTOR2Pass()";
+  let dependentDialects = ["hw::HWDialect", "sv::SVDialect", "comb::CombDialect",
+                           "seq::SeqDialect"];
+}
+
 //===----------------------------------------------------------------------===//
 // VerifToSV
 //===----------------------------------------------------------------------===//

lib/CAPI/Conversion/CMakeLists.txt

@@ -20,6 +20,7 @@ add_mlir_public_c_api_library(CIRCTCAPIConversion
   CIRCTHWArithToHW
   CIRCTHWToLLHD
   CIRCTHWToLLVM
+  CIRCTHWToBTOR2
   CIRCTHWToSV
   CIRCTHWToSystemC
   CIRCTLLHDToLLVM

lib/Conversion/CMakeLists.txt

@@ -13,6 +13,7 @@ add_subdirectory(FSMToSV)
 add_subdirectory(HandshakeToDC)
 add_subdirectory(HandshakeToHW)
 add_subdirectory(HWArithToHW)
+add_subdirectory(HWToBTOR2)
 add_subdirectory(HWToLLHD)
 add_subdirectory(HWToLLVM)
 add_subdirectory(HWToSV)

lib/Conversion/HWToBTOR2/CMakeLists.txt

@@ -0,0 +1,16 @@
+add_circt_conversion_library(CIRCTHWToBTOR2
+  HWToBTOR2.cpp
+
+  DEPENDS
+  CIRCTConversionPassIncGen
+
+  LINK_COMPONENTS
+  Core
+
+  LINK_LIBS PUBLIC
+  CIRCTHW
+  CIRCTSV
+  CIRCTComb
+  CIRCTSeq
+  MLIRTransforms
+)