From 74365bbfa421afcac2734506d2d97d571b284b53 Mon Sep 17 00:00:00 2001 From: Liam Gallagher Date: Sun, 14 Jan 2024 20:21:44 +0000 Subject: [PATCH 1/2] Add pono backend to chisel formal for bmc --- .github/workflows/test.yml | 2 +- .../chiseltest/formal/backends/Maltese.scala | 7 +++-- .../backends/btor/Btor2ModelChecker.scala | 29 ++++++++++++++----- .../scala/chiseltest/formal/package.scala | 1 + .../formal/FormalBackendOption.scala | 1 + 5 files changed, 30 insertions(+), 10 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 158d0906b..d55a91c3b 100644 --- a/.github/workflows/test.yml +++ b/.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 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 } diff --git a/src/test/scala/chiseltest/formal/FormalBackendOption.scala b/src/test/scala/chiseltest/formal/FormalBackendOption.scala index 8a1ab4b51..162d40b7c 100644 --- a/src/test/scala/chiseltest/formal/FormalBackendOption.scala +++ b/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 From 5dead24cd1cac5150690532f94db179b3ac13b73 Mon Sep 17 00:00:00 2001 From: Liam Gallagher Date: Sun, 21 Jan 2024 17:05:43 +0000 Subject: [PATCH 2/2] Add list of valid return values for btor modelcheckers. Use `--witness` to generate witness output rather than relying on `--vcd` --- .../backends/btor/Btor2ModelChecker.scala | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala b/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala index 571f2ba74..31efe134d 100644 --- a/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala +++ b/src/main/scala/chiseltest/formal/backends/btor/Btor2ModelChecker.scala @@ -6,27 +6,33 @@ import chiseltest.formal.backends._ import firrtl2.backends.experimental.smt._ 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("--vcd", "ignore.vcd") ++ Seq(btorFile) + 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 @@ -44,7 +50,12 @@ class Btor2ModelChecker(solver: Solver, targetDir: os.Path) extends IsModelCheck 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) {