[Formal] Expose Btor2 target

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

@@ -190,6 +190,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 EmittedVerilogCircuitAnnotation(a) => a
+      }
+      .get
+      .value
+  }
 }
 
 /** Command line entry point to [[ChiselStage]] */

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

@@ -1095,6 +1095,22 @@ 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 ChiselStageSpec.Foo)
+      println(btor2)
+    }
+
     it("""should error if give a "--target-directory" option""") {
 
       val exception = intercept[firrtl.options.OptionsException] {