[smt] make SMTLib + Btor2 emitters public objects (#2326)

This will make it easier for formal verification
libraries to make use of these emitters.

3 files changed, 16 insertions, 17 deletions

diff --git a/src/main/scala/firrtl/Emitter.scala b/src/main/scala/firrtl/Emitter.scala
index 760e83fd..589acc70 100644
--- a/src/main/scala/firrtl/Emitter.scala
+++ b/src/main/scala/firrtl/Emitter.scala
@@ -56,10 +56,10 @@ object EmitCircuitAnnotation extends HasShellOptions {
               RunFirrtlTransformAnnotation(new SystemVerilogEmitter),
               EmitCircuitAnnotation(classOf[SystemVerilogEmitter])
             )
-          case "experimental-btor2" =>
-            Seq(RunFirrtlTransformAnnotation(new Btor2Emitter), EmitCircuitAnnotation(classOf[Btor2Emitter]))
-          case "experimental-smt2" =>
-            Seq(RunFirrtlTransformAnnotation(new SMTLibEmitter), EmitCircuitAnnotation(classOf[SMTLibEmitter]))
+          case "experimental-btor2" | "btor2" =>
+            Seq(RunFirrtlTransformAnnotation(Dependency(Btor2Emitter)), EmitCircuitAnnotation(Btor2Emitter.getClass))
+          case "experimental-smt2" | "smt2" =>
+            Seq(RunFirrtlTransformAnnotation(Dependency(SMTLibEmitter)), EmitCircuitAnnotation(SMTLibEmitter.getClass))
           case _ => throw new PhaseException(s"Unknown emitter '$a'! (Did you misspell it?)")
         },
       helpText = "Run the specified circuit emitter (all modules in one file)",
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
index ca472578..cc6a3e8a 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
@@ -22,14 +22,6 @@ private[firrtl] abstract class SMTEmitter private[firrtl] ()
 
   protected def serialize(sys: TransitionSystem): Annotation
 
-  private val BleedingEdgeWarning =
-    """WARNING: The SMT and BTOR2 emitters are experimental preview features.
-      |- they might be removed in future versions without deprecation warning
-      |- their behavior and interfaces might change without notice
-      |- they are unsupported, we won't be able to fix any issues you find in them
-      |- however, we do accept pull requests: https://github.com/freechipsproject/firrtl/pulls
-      |""".stripMargin
-
   override protected def execute(state: CircuitState): CircuitState = {
     val emitCircuit = state.annotations.exists {
       case EmitCircuitAnnotation(a) if this.getClass == a    => true
@@ -39,8 +31,6 @@ private[firrtl] abstract class SMTEmitter private[firrtl] ()
 
     if (!emitCircuit) { return state }
 
-    logger.warn(BleedingEdgeWarning)
-
     val sys = state.annotations.collectFirst { case TransitionSystemAnnotation(sys) => sys }.getOrElse {
       error("Could not find the transition system!")
     }
@@ -62,7 +52,8 @@ case class EmittedSMTModelAnnotation(name: String, src: String, outputSuffix: St
   override def getBytes:         Iterable[Byte] = src.getBytes
 }
 
-private[firrtl] class Btor2Emitter extends SMTEmitter {
+/** Turns the transition system generated by [[FirrtlToTransitionSystem]] into a btor2 file. */
+object Btor2Emitter extends SMTEmitter {
   override def outputSuffix: String = ".btor2"
   override protected def serialize(sys: TransitionSystem): Annotation = {
     val btor = generatedHeader("BTOR", sys.name) + Btor2Serializer.serialize(sys).mkString("\n") + "\n"
@@ -70,7 +61,8 @@ private[firrtl] class Btor2Emitter extends SMTEmitter {
   }
 }
 
-private[firrtl] class SMTLibEmitter extends SMTEmitter {
+/** Turns the transition system generated by [[FirrtlToTransitionSystem]] into an SMTLib file. */
+object SMTLibEmitter extends SMTEmitter {
   override def outputSuffix: String = ".smt2"
   override protected def serialize(sys: TransitionSystem): Annotation = {
     val hasMemory = sys.states.exists(_.sym.isInstanceOf[ArrayExpr])
diff --git a/src/main/scala/firrtl/stage/Forms.scala b/src/main/scala/firrtl/stage/Forms.scala
index 83d019f5..4348ec32 100644
--- a/src/main/scala/firrtl/stage/Forms.scala
+++ b/src/main/scala/firrtl/stage/Forms.scala
@@ -3,6 +3,7 @@
 package firrtl.stage
 
 import firrtl._
+import firrtl.backends.experimental.smt.{Btor2Emitter, SMTLibEmitter}
 import firrtl.options.Dependency
 import firrtl.stage.TransformManager.TransformDependency
 
@@ -130,7 +131,13 @@ object Forms {
     )
 
   val BackendEmitters =
-    Seq(Dependency[VerilogEmitter], Dependency[MinimumVerilogEmitter], Dependency[SystemVerilogEmitter])
+    Seq(
+      Dependency[VerilogEmitter],
+      Dependency[MinimumVerilogEmitter],
+      Dependency[SystemVerilogEmitter],
+      Dependency(SMTLibEmitter),
+      Dependency(Btor2Emitter)
+    )
 
   val LowEmitters = Dependency[LowFirrtlEmitter] +: BackendEmitters