Add pono backend to chisel formal for bmc

.github/workflows/test.yml

@@ -128,7 +128,7 @@ jobs:
     runs-on: ubuntu-20.04
     strategy:
       matrix:
-        backend: [z3, cvc4, btormc, bitwuzla]
+        backend: [z3, cvc4, btormc, bitwuzla, pono]
     steps:
       - name: Checkout
         uses: actions/checkout@v3

src/main/scala/chiseltest/formal/backends/Maltese.scala

@@ -2,7 +2,7 @@
 
 package chiseltest.formal.backends
 
-import chiseltest.formal.backends.btor.BtormcModelChecker
+import chiseltest.formal.backends.btor._
 import chiseltest.formal.backends.smt._
 import chiseltest.formal.{DoNotModelUndef, DoNotOptimizeFormal, FailedBoundedCheckException}
 import firrtl2._
@@ -56,6 +56,8 @@ private case object BoolectorEngineAnnotation extends FormalEngineAnnotation
   */
 case object BitwuzlaEngineAnnotation extends FormalEngineAnnotation
 
+case object PonoEngineAnnotation extends FormalEngineAnnotation
+
 /** Formal Verification based on the firrtl compiler's SMT backend and the maltese SMT libraries solver bindings. */
 private[chiseltest] object Maltese {
   def bmc(circuit: ir.Circuit, annos: AnnotationSeq, kMax: Int, resetLength: Int = 0): Unit = {
@@ -166,10 +168,11 @@ private[chiseltest] object Maltese {
     engines.map {
       case CVC4EngineAnnotation      => new SMTModelChecker(CVC4SMTLib)
       case Z3EngineAnnotation        => new SMTModelChecker(Z3SMTLib)
-      case BtormcEngineAnnotation    => new BtormcModelChecker(targetDir)
+      case BtormcEngineAnnotation    => new Btor2ModelChecker(BtormcBtor2, targetDir)
       case Yices2EngineAnnotation    => new SMTModelChecker(Yices2SMTLib)
       case BoolectorEngineAnnotation => new SMTModelChecker(BoolectorSMTLib)
       case BitwuzlaEngineAnnotation  => new SMTModelChecker(BitwuzlaSMTLib)
+      case PonoEngineAnnotation      => new Btor2ModelChecker(PonoBtor2, targetDir)
     }
   }
 

src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala

@@ -5,10 +5,34 @@ package chiseltest.formal.backends.btor
 import chiseltest.formal.backends._
 import firrtl2.backends.experimental.smt._
 
-class BtormcModelChecker(targetDir: os.Path) extends IsModelChecker {
+private[chiseltest] trait Solver {
+  def name(): String
+  def cmd(btorFile: String, kMax: Int): Seq[String]
+  def valid_return_codes(): Set[Int]
+}
+
+object BtormcBtor2 extends Solver {
+  override def name(): String = "btormc"
+  override def cmd(btorFile: String, kMax: Int): Seq[String] = {
+    val kmaxOpt = if (kMax > 0) Seq("--kmax", kMax.toString) else Seq()
+    Seq("btormc") ++ kmaxOpt ++ Seq(btorFile)
+  }
+  def valid_return_codes(): Set[Int] = Set(0)
+}
+
+object PonoBtor2 extends Solver {
+  override def name(): String = "pono"
+  override def cmd(btorFile: String, kMax: Int): Seq[String] = {
+    val kmaxOpt = if (kMax > 0) Seq("-k", kMax.toString) else Seq()
+    Seq("pono") ++ Seq("-e", "bmc") ++ kmaxOpt ++ Seq("--witness") ++ Seq(btorFile)
+  }
+  def valid_return_codes(): Set[Int] = Set(0, 255)
+}
+
+class Btor2ModelChecker(solver: Solver, targetDir: os.Path) extends IsModelChecker {
   override val fileExtension = ".btor2"
-  override val name:   String = "btormc"
-  override val prefix: String = "btormc"
+  override val name:   String = solver.name()
+  override val prefix: String = solver.name()
 
   override def check(sys: TransitionSystem, kMax: Int): ModelCheckResult = {
     // serialize the system to btor2
@@ -18,29 +42,31 @@ class BtormcModelChecker(targetDir: os.Path) extends IsModelChecker {
     os.write.over(targetDir / filename, lines.mkString("", "\n", "\n"))
 
     // execute model checker
-    val kmaxOpt = if (kMax > 0) Seq("--kmax", kMax.toString) else Seq()
-    val cmd = Seq("btormc") ++ kmaxOpt ++ Seq(filename)
+    val cmd = solver.cmd(filename, kMax)
     val r = os.proc(cmd).call(cwd = targetDir, check = false)
 
     // write stdout to file for debugging
     val res = r.out.lines()
     os.write.over(targetDir / (filename + ".out"), res.mkString("", "\n", "\n"))
 
     // check to see if we were successful
-    assert(r.exitCode == 0, s"We expect btormc to always return 0, not ${r.exitCode}. Maybe there was an error.")
+    assert(
+      solver.valid_return_codes().contains(r.exitCode),
+      s"We expect ${solver.name()} to always return one of " +
+        s"${solver.valid_return_codes()}, not ${r.exitCode}. " +
+        s"Maybe there was an error."
+    )
     val isSat = res.nonEmpty && res.head.trim.startsWith("sat")
 
     if (isSat) {
       val witness = Btor2WitnessParser.read(res, 1).head
-      ModelCheckFail(Btor2ModelChecker.convertWitness(sys, witness))
+      ModelCheckFail(convertWitness(sys, witness))
     } else {
       ModelCheckSuccess()
     }
   }
-}
 
-object Btor2ModelChecker {
-  def convertWitness(sys: TransitionSystem, bw: Btor2Witness): Witness = {
+  private def convertWitness(sys: TransitionSystem, bw: Btor2Witness): Witness = {
     val badNames = sys.signals.filter(_.lbl == IsBad).map(_.name).toIndexedSeq
     val failed = bw.failed.map(badNames)
     Witness(failed, bw.regInit, bw.memInit, bw.inputs)

src/main/scala/chiseltest/formal/package.scala

@@ -8,5 +8,6 @@ package object formal {
   val Z3EngineAnnotation = backends.Z3EngineAnnotation
   val BtormcEngineAnnotation = backends.BtormcEngineAnnotation
   val BitwuzlaEngineAnnotation = backends.BitwuzlaEngineAnnotation
+  val PonoEngineAnnotation = backends.PonoEngineAnnotation
   val MagicPacketTracker = vips.MagicPacketTracker
 }

src/test/scala/chiseltest/formal/FormalBackendOption.scala

@@ -17,6 +17,7 @@ object FormalBackendOption {
       case Some("z3")        => Z3EngineAnnotation
       case Some("cvc4")      => CVC4EngineAnnotation
       case Some("btormc")    => BtormcEngineAnnotation
+      case Some("pono")      => PonoEngineAnnotation
       case Some("yices2")    => throw new RuntimeException("yices is not supported yet")
       case Some("boolector") => throw new RuntimeException("boolector is not supported yet")
       case Some("bitwuzla")  => BitwuzlaEngineAnnotation