From e6b73aef352561620a5310af2bc83757209a498b Mon Sep 17 00:00:00 2001
From: Liam Gallagher <liam.d.gallagher@protonmail.com>
Date: Sun, 14 Jan 2024 20:21:44 +0000
Subject: [PATCH] Add pono backend to chisel formal for bmc

---
 .../chiseltest/formal/backends/Maltese.scala  |  7 +++--
 .../backends/btor/Btor2ModelChecker.scala     | 29 ++++++++++++++-----
 .../scala/chiseltest/formal/package.scala     |  1 +
 3 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/src/main/scala/chiseltest/formal/backends/Maltese.scala b/src/main/scala/chiseltest/formal/backends/Maltese.scala
index d86948384..642a7b67d 100644
--- a/src/main/scala/chiseltest/formal/backends/Maltese.scala
+++ b/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)
     }
   }
 
diff --git a/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala b/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala
index 2548e0826..571f2ba74 100644
--- a/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala
+++ b/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala
@@ -5,7 +5,25 @@ 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 cmd(btorFile: String, kMax: Int): Seq[String]
+}
+
+object BtormcBtor2 extends Solver {
+  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)
+  }
+}
+
+object PonoBtor2 extends Solver {
+  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("--vcd", "ignore.vcd") ++ Seq(btorFile)
+  }
+}
+
+class Btor2ModelChecker(solver: Solver, targetDir: os.Path) extends IsModelChecker {
   override val fileExtension = ".btor2"
   override val name:   String = "btormc"
   override val prefix: String = "btormc"
@@ -18,8 +36,7 @@ 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
@@ -32,15 +49,13 @@ class BtormcModelChecker(targetDir: os.Path) extends IsModelChecker {
 
     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)
diff --git a/src/main/scala/chiseltest/formal/package.scala b/src/main/scala/chiseltest/formal/package.scala
index 4dfc86ddb..d967fe294 100644
--- a/src/main/scala/chiseltest/formal/package.scala
+++ b/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
 }