formal: add bitwuzla backend

.github/workflows/test.yml

@@ -74,7 +74,7 @@ jobs:
       - name: Install Tabby OSS Cad Suite (from YosysHQ)
         uses: YosysHQ/setup-oss-cad-suite@v1
         with:
-          osscadsuite-version: '2021-11-09'
+          osscadsuite-version: '2022-08-18'
       - name: Print Verilator Version
         run: verilator --version
       - name: Setup Scala
@@ -132,40 +132,47 @@ jobs:
 
   formal:
     name: formal verification tests
-    runs-on: ${{ matrix.os }}
+    runs-on: ubuntu-20.04
     strategy:
       matrix:
-        os: [ubuntu-20.04, macos-latest]
-        backend: [z3, cvc4, btormc]
+        backend: [z3, cvc4, btormc, bitwuzla]
     steps:
       - name: Checkout
         uses: actions/checkout@v2
-      - name: Install Z3 and CVC4 for Ubuntu
+      - name: Install Z3 and CVC4
         if: runner.os == 'Linux'
         run: |
           sudo apt-get install -y z3 cvc4
           z3 --version
           cvc4 --version
-      - name: Install Z3 and CVC4 for MacOS
-        if: runner.os == 'macOS'
-        run: |
-          brew install z3
-          brew tap cvc4/cvc4
-          brew install cvc4/cvc4/cvc4
-          z3 --version
-          cvc4 --version
       - name: Install Tabby OSS Cad Suite (from YosysHQ)
-        if: matrix.backend == 'btormc'
         uses: YosysHQ/setup-oss-cad-suite@v1
         with:
-          osscadsuite-version: '2021-11-09'
+          osscadsuite-version: '2022-08-18'
       - name: Setup Scala
         uses: olafurpg/setup-scala@v10
         with:
           java-version: [email protected]
       - name: Test
         run: sbt "testOnly -- -n Formal -Dformal_engine=${{ matrix.backend }}"
 
+  formal-mac:
+    name: formal verification tests on mac
+    runs-on: macos-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      - name: Install Z3 for MacOS
+        run: |
+          brew install z3
+          z3 --version
+      - name: Setup Scala
+        uses: olafurpg/setup-scala@v10
+        with:
+          java-version: [email protected]
+      - name: Test
+        run: sbt "testOnly -- -n Formal -Dformal_engine=z3"
+
   doc:
     name: Documentation and Formatting
     runs-on: ubuntu-20.04
@@ -186,7 +193,7 @@ jobs:
   # When adding new jobs, please add them to `needs` below
   all_tests_passed:
     name: "all tests passed"
-    needs: [test, doc, verilator, verilator-mac, formal, icarus, test-mac]
+    needs: [test, doc, verilator, verilator-mac, formal, formal-mac, icarus, test-mac]
     runs-on: ubuntu-latest
     steps:
       - run: echo Success!

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

@@ -30,6 +30,24 @@ case object Z3EngineAnnotation extends FormalEngineAnnotation
   */
 case object BtormcEngineAnnotation extends FormalEngineAnnotation
 
+/** Use a SMTLib based model checker with the yices2 SMT solver.
+  * @note yices2 often performs better than Z3 or CVC4.
+  * @note yices2 is not supported yet, because we have not figured out yet how to deal with memory initialization
+  */
+private case object Yices2EngineAnnotation extends FormalEngineAnnotation
+
+/** Use a SMTLib based model checker with the boolector SMT solver.
+  * @note boolector often performs better than Z3 or CVC4.
+  * @note boolecter is not supported, because some bugs that were fixed in bitwuzla still remain in boolector
+  *       leading to crashes when trying to get-value of arrays.
+  */
+private case object BoolectorEngineAnnotation extends FormalEngineAnnotation
+
+/** Use a SMTLib based model checker with the bitwuzla SMT solver.
+  * @note bitwuzla often performs better than Z3 or CVC4.
+  */
+case object BitwuzlaEngineAnnotation 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 = {
@@ -138,9 +156,12 @@ private[chiseltest] object Maltese {
     val engines = annos.collect { case a: FormalEngineAnnotation => a }
     assert(engines.nonEmpty, "You need to provide at least one formal engine annotation!")
     engines.map {
-      case CVC4EngineAnnotation   => new SMTModelChecker(CVC4SMTLib)
-      case Z3EngineAnnotation     => new SMTModelChecker(Z3SMTLib)
-      case BtormcEngineAnnotation => new BtormcModelChecker(targetDir)
+      case CVC4EngineAnnotation      => new SMTModelChecker(CVC4SMTLib)
+      case Z3EngineAnnotation        => new SMTModelChecker(Z3SMTLib)
+      case BtormcEngineAnnotation    => new BtormcModelChecker(targetDir)
+      case Yices2EngineAnnotation    => new SMTModelChecker(Yices2SMTLib)
+      case BoolectorEngineAnnotation => new SMTModelChecker(BoolectorSMTLib)
+      case BitwuzlaEngineAnnotation  => new SMTModelChecker(BitwuzlaSMTLib)
     }
   }
 

src/main/scala/chiseltest/formal/backends/smt/CompactSmtEncoding.scala

@@ -0,0 +1,67 @@
+// SPDX-License-Identifier: Apache-2.0
+// Author: Kevin Laeufer <[email protected]>
+
+package chiseltest.formal.backends.smt
+
+import firrtl.backends.experimental.smt._
+import scala.collection.mutable
+
+class CompactSmtEncoding(sys: TransitionSystem) extends TransitionSystemSmtEncoding {
+  import SMTTransitionSystemEncoder._
+  private def id(s: String): String = SMTLibSerializer.escapeIdentifier(s)
+  private val stateType = id(sys.name + "_s")
+  private val stateInitFun = id(sys.name + "_i")
+  private val stateTransitionFun = id(sys.name + "_t")
+
+  private val states = mutable.ArrayBuffer[UTSymbol]()
+
+  def defineHeader(ctx: SolverContext): Unit = encode(sys).foreach(ctx.runCommand)
+
+  private def appendState(ctx: SolverContext): UTSymbol = {
+    val s = UTSymbol(s"s${states.length}", stateType)
+    ctx.runCommand(DeclareUninterpretedSymbol(s.name, s.tpe))
+    states.append(s)
+    s
+  }
+
+  def init(ctx: SolverContext): Unit = {
+    assert(states.isEmpty)
+    val s0 = appendState(ctx)
+    ctx.assert(BVFunctionCall(stateInitFun, List(s0), 1))
+  }
+
+  def unroll(ctx: SolverContext): Unit = {
+    assert(states.nonEmpty)
+    appendState(ctx)
+    val tStates = states.takeRight(2).toList
+    ctx.assert(BVFunctionCall(stateTransitionFun, tStates, 1))
+  }
+
+  /** returns an expression representing the constraint in the current state */
+  def getConstraint(name: String): BVExpr = {
+    assert(states.nonEmpty)
+    val foo = id(name + "_f")
+    BVFunctionCall(foo, List(states.last), 1)
+  }
+
+  /** returns an expression representing the assertion in the current state */
+  def getAssertion(name: String): BVExpr = {
+    assert(states.nonEmpty)
+    val foo = id(name + "_f")
+    BVFunctionCall(foo, List(states.last), 1)
+  }
+
+  def getSignalAt(sym: BVSymbol, k: Int): BVExpr = {
+    assert(states.length > k, s"no state s$k")
+    val state = states(k)
+    val foo = id(sym.name + "_f")
+    BVFunctionCall(foo, List(state), sym.width)
+  }
+
+  def getSignalAt(sym: ArraySymbol, k: Int): ArrayExpr = {
+    assert(states.length > k, s"no state s$k")
+    val state = states(k)
+    val foo = id(sym.name + "_f")
+    ArrayFunctionCall(foo, List(state), sym.indexWidth, sym.dataWidth)
+  }
+}

src/main/scala/chiseltest/formal/backends/smt/SMTLibResponseParser.scala

@@ -72,33 +72,56 @@ private object SMTLibResponseParser {
   }
 }
 
-sealed trait SExpr
+sealed trait SExpr {
+  def isEmpty: Boolean
+}
 case class SExprNode(children: List[SExpr]) extends SExpr {
   override def toString = children.mkString("(", " ", ")")
+  override def isEmpty: Boolean = children.isEmpty || children.forall(_.isEmpty)
 }
 case class SExprLeaf(value: String) extends SExpr {
   override def toString = value
+  override def isEmpty: Boolean = value.trim.isEmpty
 }
 
 /** simple S-Expression parser to make sense of SMTLib solver output */
 object SExprParser {
   def parse(line: String): SExpr = {
-    val tokens = line
-      .replace("(", " ( ")
-      .replace(")", " ) ")
-      .split("\\s+")
-      .filterNot(_.isEmpty)
-      .toList
+    val tokens = tokenize(line)
 
-    assert(tokens.nonEmpty)
-    if (tokens.head == "(") {
+    if (tokens.isEmpty) {
+      SExprLeaf("")
+    } else if (tokens.head == "(") {
       parseSExpr(tokens.tail)._1
     } else {
-      assert(tokens.tail.isEmpty)
+      assert(tokens.tail.isEmpty, s"multiple tokens, but not starting with a `(`:\n${tokens.mkString(" ")}")
       SExprLeaf(tokens.head)
     }
   }
 
+  // tokenization with | as escape character
+  private def tokenize(line: String): List[String] = {
+    var tokens: List[String] = List()
+    var inEscape = false
+    var tmp = ""
+    def finish(): Unit = {
+      if (tmp.nonEmpty) {
+        tokens = tokens :+ tmp
+        tmp = ""
+      }
+    }
+    line.foreach {
+      case '('                                   => finish(); tokens = tokens :+ "("
+      case ')'                                   => finish(); tokens = tokens :+ ")"
+      case '|' if inEscape                       => tmp += '|'; finish(); inEscape = false
+      case '|' if !inEscape                      => finish(); inEscape = true; tmp = "|"
+      case ' ' | '\t' | '\r' | '\n' if !inEscape => finish()
+      case other                                 => tmp += other
+    }
+    finish()
+    tokens
+  }
+
   private def parseSExpr(tokens: List[String]): (SExpr, List[String]) = {
     var t = tokens
     var elements = List[SExpr]()