[Formal] Expose Btor2 target

firrtl/src/main/scala/firrtl/Emitter.scala

@@ -38,6 +38,11 @@ case class EmittedFirrtlCircuitAnnotation(value: EmittedFirrtlCircuit)
 
 final case class EmittedFirrtlCircuit(name: String, value: String, outputSuffix: String) extends EmittedCircuit
 
+final case class EmittedBtor2Circuit(name: String, value: String, outputSuffix: String) extends EmittedCircuit
+
+case class EmittedBtor2CircuitAnnotation(value: EmittedBtor2Circuit)
+    extends EmittedCircuitAnnotation[EmittedBtor2Circuit]
+
 final case class EmittedVerilogCircuit(name: String, value: String, outputSuffix: String) extends EmittedCircuit
 case class EmittedVerilogCircuitAnnotation(value: EmittedVerilogCircuit)
     extends EmittedCircuitAnnotation[EmittedVerilogCircuit]

src/main/scala/circt/stage/Annotations.scala

@@ -57,6 +57,8 @@ object CIRCTTarget {
   /** The SystemVerilog language */
   case object SystemVerilog extends Type
 
+  /* The btor2 format for bounded model checking */
+  case object Btor2 extends Type
 }
 
 /** Annotation that tells [[circt.stage.phases.CIRCT CIRCT]] what target to compile to */
@@ -73,10 +75,11 @@ object CIRCTTargetAnnotation extends HasShellOptions {
         case "hw"            => Seq(CIRCTTargetAnnotation(CIRCTTarget.HW))
         case "verilog"       => Seq(CIRCTTargetAnnotation(CIRCTTarget.Verilog))
         case "systemverilog" => Seq(CIRCTTargetAnnotation(CIRCTTarget.SystemVerilog))
+        case "btor2"         => Seq(CIRCTTargetAnnotation(CIRCTTarget.Btor2))
         case a               => throw new OptionsException(s"Unknown target name '$a'! (Did you misspell it?)")
       },
       helpText = "The CIRCT",
-      helpValueName = Some("{chirrtl|firrtl|hw|verilog|systemverilog}")
+      helpValueName = Some("{chirrtl|firrtl|hw|verilog|systemverilog|btor2}")
     )
   )
 

src/main/scala/circt/stage/ChiselStage.scala

@@ -9,6 +9,7 @@ import firrtl.{AnnotationSeq, EmittedVerilogCircuitAnnotation}
 import firrtl.options.{CustomFileEmission, Dependency, Phase, PhaseManager, Stage, StageMain, Unserializable}
 import firrtl.stage.FirrtlCircuitAnnotation
 import logger.LogLevelAnnotation
+import firrtl.EmittedBtor2CircuitAnnotation
 
 /** Entry point for running Chisel with the CIRCT compiler.
   *
@@ -190,6 +191,31 @@ object ChiselStage {
       Array("--target", "systemverilog") ++ args,
       Seq(ChiselGeneratorAnnotation(() => gen)) ++ firtoolOpts.map(FirtoolOption(_))
     )
+
+  /** Compile a Chisel circuit to btor2
+    *
+    * @param gen         a call-by-name Chisel module
+    * @param args        additional command line arguments to pass to Chisel
+    * @param firtoolOpts additional command line options to pass to firtool
+    * @return a string containing the btor2 output
+    */
+  def emitBtor2(
+    gen:         => RawModule,
+    args:        Array[String] = Array.empty,
+    firtoolOpts: Array[String] = Array.empty
+  ): String = {
+    val annos = Seq(
+      ChiselGeneratorAnnotation(() => gen),
+      CIRCTTargetAnnotation(CIRCTTarget.Btor2)
+    ) ++ (new Shell("circt")).parse(args) ++ firtoolOpts.map(FirtoolOption(_))
+    phase
+      .transform(annos)
+      .collectFirst {
+        case EmittedBtor2CircuitAnnotation(a) => a
+      }
+      .get
+      .value
+  }
 }
 
 /** Command line entry point to [[ChiselStage]] */

src/main/scala/circt/stage/phases/CIRCT.scala

@@ -18,6 +18,8 @@ import firrtl.{AnnotationSeq, EmittedVerilogCircuit, EmittedVerilogCircuitAnnota
 import java.io.File
 import scala.collection.mutable
 import scala.util.control.NoStackTrace
+import firrtl.EmittedBtor2CircuitAnnotation
+import firrtl.EmittedBtor2Circuit
 
 private object Helpers {
   implicit class LogLevelHelpers(logLevel: LogLevel.Value) {
@@ -244,6 +246,7 @@ class CIRCT extends Phase {
           case (Some(CIRCTTarget.Verilog), false)       => None
           case (Some(CIRCTTarget.SystemVerilog), true)  => Seq("--split-verilog", s"-o=${stageOptions.targetDir}")
           case (Some(CIRCTTarget.SystemVerilog), false) => None
+          case (Some(CIRCTTarget.Btor2), false)         => Seq("--btor2")
           case (None, _) =>
             throw new Exception(
               "No 'circtOptions.target' specified. This should be impossible if dependencies are satisfied!"
@@ -302,6 +305,8 @@ class CIRCT extends Phase {
           Seq(EmittedMLIR(outputFileName, result, Some(".hw.mlir")))
         case Some(CIRCTTarget.Verilog) =>
           Seq(EmittedVerilogCircuitAnnotation(EmittedVerilogCircuit(outputFileName, result, ".v")))
+        case Some(CIRCTTarget.Btor2) =>
+          Seq(EmittedBtor2CircuitAnnotation(EmittedBtor2Circuit(outputFileName, result, ".btor2")))
         case Some(CIRCTTarget.SystemVerilog) =>
           Seq(EmittedVerilogCircuitAnnotation(EmittedVerilogCircuit(outputFileName, result, ".sv")))
         case None =>

src/test/scala/circtTests/stage/ChiselStageSpec.scala

@@ -1095,6 +1095,47 @@ class ChiselStageSpec extends AnyFunSpec with Matchers with chiselTests.Utils {
       info(s"'$expectedOutput' exists")
     }
 
+    it("should emit btor2 to string") {
+      import chisel3._
+      import chisel3.ltl._
+
+      class Counter extends Module {
+        val count = RegInit(0.U(32.W))
+        when(count === 42.U) { count := 0.U }.otherwise { count := count + 1.U }
+
+        AssertProperty((count <= 42.U))
+      }
+
+      val btor2 = ChiselStage.emitBtor2(new Counter)
+      btor2 should include("""1 sort bitvec 1
+                             |2 input 1 reset
+                             |3 sort bitvec 32
+                             |4 state 3 count
+                             |5 constd 1 0
+                             |6 state 1 hbr
+                             |7 init 1 6 5
+                             |8 constd 3 43
+                             |9 constd 3 1
+                             |10 constd 3 42
+                             |11 constd 1 -1
+                             |12 constd 3 0
+                             |13 eq 1 4 10
+                             |14 add 3 4 9
+                             |15 ite 3 13 12 14
+                             |16 ult 1 4 8
+                             |17 constd 1 -1
+                             |18 or 1 2 6
+                             |19 xor 1 2 17
+                             |20 and 1 6 19
+                             |21 xor 1 20 11
+                             |22 or 1 21 16
+                             |23 not 1 22
+                             |24 bad 23
+                             |25 ite 3 2 12 15
+                             |26 next 3 4 25
+                             |28 next 1 6 27""".stripMargin)
+    }
+
     it("""should error if give a "--target-directory" option""") {
 
       val exception = intercept[firrtl.options.OptionsException] {