formal: add bitwuzla backend support

.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

@@ -4,59 +4,60 @@
 package chiseltest.formal.backends.smt
 
 import scala.annotation.tailrec
+import scala.collection.mutable
 
 private object SMTLibResponseParser {
   def parseValue(v: String): Option[BigInt] = {
     val expr = SExprParser.parse(v)
     expr match {
       // this is the assignment, something like ((in #b00000))
-      case SExprNode(List(SExprNode(List(_, value)))) => parseValue(value)
-      case _                                          => throw new NotImplementedError(s"Unexpected response: $expr")
+      case SExprNode(Seq(SExprNode(Seq(_, value)))) => parseValue(value)
+      case _                                        => throw new NotImplementedError(s"Unexpected response: $expr")
     }
   }
 
   @tailrec
   private def parseValue(e: SExpr): Option[BigInt] = e match {
     case SExprLeaf(valueStr) => parseBVLiteral(valueStr)
     // example: (_ bv0 32)
-    case SExprNode(List(SExprLeaf("_"), SExprLeaf(value), SExprLeaf(width))) if value.startsWith("bv") =>
+    case SExprNode(Seq(SExprLeaf("_"), SExprLeaf(value), SExprLeaf(width))) if value.startsWith("bv") =>
       Some(BigInt(value.drop(2)))
-    case SExprNode(List(one)) => parseValue(one)
-    case _                    => throw new NotImplementedError(s"Unexpected response: $e")
+    case SExprNode(Seq(one)) => parseValue(one)
+    case _                   => throw new NotImplementedError(s"Unexpected response: $e")
   }
 
   type MemInit = Seq[(Option[BigInt], BigInt)]
 
   def parseMemValue(v: String): MemInit = {
     val tree = SExprParser.parse(v)
     tree match {
-      case SExprNode(List(SExprNode(List(_, value)))) => parseMem(value, Map())
-      case _                                          => throw new NotImplementedError(s"Unexpected response: $v")
+      case SExprNode(Seq(SExprNode(Seq(_, value)))) => parseMem(value, Map())
+      case _                                        => throw new NotImplementedError(s"Unexpected response: $v")
     }
   }
 
   private def parseMem(value: SExpr, ctx: Map[String, MemInit]): MemInit = value match {
-    case SExprNode(List(SExprNode(List(SExprLeaf("as"), SExprLeaf("const"), tpe)), value)) =>
+    case SExprNode(Seq(SExprNode(Seq(SExprLeaf("as"), SExprLeaf("const"), tpe)), value)) =>
       // initialize complete memory to value
-      List((None, parseValue(value).get))
-    case SExprNode(List(SExprLeaf("store"), array, indexExpr, valueExpr)) =>
+      Seq((None, parseValue(value).get))
+    case SExprNode(Seq(SExprLeaf("store"), array, indexExpr, valueExpr)) =>
       val (index, value) = (parseValue(indexExpr), parseValue(valueExpr))
       parseMem(array, ctx) :+ (Some(index.get), value.get)
-    case SExprNode(List(SExprLeaf("let"), SExprNode(List(SExprNode(List(SExprLeaf(variable), array0)))), array1)) =>
+    case SExprNode(Seq(SExprLeaf("let"), SExprNode(Seq(SExprNode(Seq(SExprLeaf(variable), array0)))), array1)) =>
       val newCtx = ctx ++ Seq(variable -> parseMem(array0, ctx))
       parseMem(array1, newCtx)
     case SExprLeaf(variable) =>
       assert(ctx.contains(variable), s"Undefined variable: $variable. " + ctx.keys.mkString(", "))
       ctx(variable)
     case SExprNode(
-          List(
+          Seq(
             SExprLeaf("lambda"),
-            SExprNode(List(SExprNode(List(SExprLeaf(v0), indexTpe)))),
-            SExprNode(List(SExprLeaf("="), SExprLeaf(v1), SExprLeaf(indexStr)))
+            SExprNode(Seq(SExprNode(Seq(SExprLeaf(v0), indexTpe)))),
+            SExprNode(Seq(SExprLeaf("="), SExprLeaf(v1), SExprLeaf(indexStr)))
           )
         ) if v0 == v1 =>
       // example: (lambda ((x!1 (_ BitVec 5))) (= x!1 #b00000))
-      List((None, BigInt(0)), (Some(parseBVLiteral(indexStr).get), BigInt(1)))
+      Seq((None, BigInt(0)), (Some(parseBVLiteral(indexStr).get), BigInt(1)))
     case other => throw new NotImplementedError(s"TODO implement parsing of SMT solver response: $other")
   }
 
@@ -72,49 +73,72 @@ private object SMTLibResponseParser {
   }
 }
 
-sealed trait SExpr
-case class SExprNode(children: List[SExpr]) extends SExpr {
+sealed trait SExpr {
+  def isEmpty: Boolean
+}
+case class SExprNode(children: Seq[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)
     }
   }
 
-  private def parseSExpr(tokens: List[String]): (SExpr, List[String]) = {
+  // tokenization with | as escape character
+  private def tokenize(line: String): Seq[String] = {
+    val tokens = mutable.ListBuffer.empty[String]
+    var inEscape = false
+    var tmp = ""
+    def finish(): Unit = {
+      if (tmp.nonEmpty) {
+        tokens += tmp
+        tmp = ""
+      }
+    }
+    line.foreach {
+      case '('                                   => finish(); tokens += "("
+      case ')'                                   => finish(); 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.toSeq
+  }
+
+  private def parseSExpr(tokens: Seq[String]): (SExpr, Seq[String]) = {
     var t = tokens
-    var elements = List[SExpr]()
+    val elements = mutable.ListBuffer.empty[SExpr]
     while (t.nonEmpty) {
       t.head match {
         case "(" =>
           val (child, nt) = parseSExpr(t.tail)
           t = nt
-          elements = elements :+ child
+          elements += child
         case ")" =>
-          return (SExprNode(elements), t.tail)
+          return (SExprNode(elements.toSeq), t.tail)
         case other =>
-          elements = elements :+ SExprLeaf(other)
+          elements += SExprLeaf(other)
           t = t.tail
       }
     }
-    (SExprNode(elements), List())
+    (SExprNode(elements.toSeq), Seq())
   }
 }