aboutsummaryrefslogtreecommitdiff
path: root/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala')
-rw-r--r--src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala16
1 files changed, 4 insertions, 12 deletions
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])