From 9688d5a2f808190d6fb1a4f5262a85c0b25cea2b Mon Sep 17 00:00:00 2001 From: Kevin Laeufer Date: Mon, 25 Jul 2022 11:44:05 -0400 Subject: [PATCH] formal: add bitwuzla backend --- .github/workflows/test.yml | 39 +++--- .../chiseltest/formal/backends/Maltese.scala | 27 +++- .../backends/smt/CompactSmtEncoding.scala | 67 ++++++++++ .../backends/smt/SMTLibResponseParser.scala | 43 +++++-- .../formal/backends/smt/SMTLibSolver.scala | 119 ++++++++++++++++-- .../formal/backends/smt/SMTModelChecker.scala | 84 +++---------- .../formal/backends/smt/Solver.scala | 7 +- .../backends/smt/UnrollSmtEncoding.scala | 94 ++++++++++++++ .../scala/chiseltest/formal/package.scala | 1 + .../formal/FormalBackendOption.scala | 3 + .../smt/SMTLibResponseParserSpec.scala | 12 ++ 11 files changed, 391 insertions(+), 105 deletions(-) create mode 100644 src/main/scala/chiseltest/formal/backends/smt/CompactSmtEncoding.scala create mode 100644 src/main/scala/chiseltest/formal/backends/smt/UnrollSmtEncoding.scala diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 4726195fa..b5beaf5a1 100644 --- a/.github/workflows/test.yml +++ b/.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,33 +132,23 @@ 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: @@ -166,6 +156,23 @@ jobs: - 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: adopt@1.11 + - 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! diff --git a/src/main/scala/chiseltest/formal/backends/Maltese.scala b/src/main/scala/chiseltest/formal/backends/Maltese.scala index 4bbee59c9..5f244b85c 100644 --- a/src/main/scala/chiseltest/formal/backends/Maltese.scala +++ b/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) } } diff --git a/src/main/scala/chiseltest/formal/backends/smt/CompactSmtEncoding.scala b/src/main/scala/chiseltest/formal/backends/smt/CompactSmtEncoding.scala new file mode 100644 index 000000000..2643e81b9 --- /dev/null +++ b/src/main/scala/chiseltest/formal/backends/smt/CompactSmtEncoding.scala @@ -0,0 +1,67 @@ +// SPDX-License-Identifier: Apache-2.0 +// Author: Kevin Laeufer + +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) + } +} diff --git a/src/main/scala/chiseltest/formal/backends/smt/SMTLibResponseParser.scala b/src/main/scala/chiseltest/formal/backends/smt/SMTLibResponseParser.scala index d1f5fffa9..bca28ff83 100644 --- a/src/main/scala/chiseltest/formal/backends/smt/SMTLibResponseParser.scala +++ b/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]() diff --git a/src/main/scala/chiseltest/formal/backends/smt/SMTLibSolver.scala b/src/main/scala/chiseltest/formal/backends/smt/SMTLibSolver.scala index 571ad90e9..d8c180ef5 100644 --- a/src/main/scala/chiseltest/formal/backends/smt/SMTLibSolver.scala +++ b/src/main/scala/chiseltest/formal/backends/smt/SMTLibSolver.scala @@ -4,14 +4,49 @@ package chiseltest.formal.backends.smt import firrtl.backends.experimental.smt._ +import scala.collection.mutable object Yices2SMTLib extends Solver { - private val cmd = List("yices-smt2", "--incremental") + private val cmd = List("yices-smt2", "--incremental", "--smt2-model-format") override def name = "yices2-smtlib" override def supportsConstArrays = false override def supportsUninterpretedFunctions = true + override def supportsUninterpretedSorts = true override def supportsQuantifiers = false - override def createContext(): SolverContext = new SMTLibSolverContext(cmd, this) + override def supportsSoftAssert = false + override def createContext(debugOn: Boolean = false): SolverContext = new SMTLibSolverContext(cmd, this, debugOn) +} + +object BoolectorSMTLib extends Solver { + private val cmd = List("boolector", "--smt2", "--incremental") + override def name = "boolector-smtlib" + override def supportsConstArrays = false + override def supportsUninterpretedFunctions = false + override def supportsUninterpretedSorts = false + override def supportsQuantifiers = false + override def supportsSoftAssert = false + override def createContext(debugOn: Boolean = false): SolverContext = { + val ctx = new SMTLibSolverContext(cmd, this, debugOn) + // wa always want to produce models + ctx.setOption("produce-models", "true") + ctx + } +} + +object BitwuzlaSMTLib extends Solver { + private val cmd = List("bitwuzla", "--smt2", "--incremental") + override def name = "bitwuzla-smtlib" + override def supportsConstArrays = false + override def supportsUninterpretedFunctions = false + override def supportsUninterpretedSorts = false + override def supportsQuantifiers = false + override def supportsSoftAssert = false + override def createContext(debugOn: Boolean = false): SolverContext = { + val ctx = new SMTLibSolverContext(cmd, this, debugOn) + // wa always want to produce models + ctx.setOption("produce-models", "true") + ctx + } } object CVC4SMTLib extends Solver { @@ -19,8 +54,10 @@ object CVC4SMTLib extends Solver { override def name = "cvc4-smtlib" override def supportsConstArrays = true override def supportsUninterpretedFunctions = true + override def supportsUninterpretedSorts = true override def supportsQuantifiers = true - override def createContext(): SolverContext = new SMTLibSolverContext(cmd, this) + override def supportsSoftAssert = false + override def createContext(debugOn: Boolean = false): SolverContext = new SMTLibSolverContext(cmd, this, debugOn) } object Z3SMTLib extends Solver { @@ -28,14 +65,62 @@ object Z3SMTLib extends Solver { override def name = "z3-smtlib" override def supportsConstArrays = true override def supportsUninterpretedFunctions = true + override def supportsUninterpretedSorts = true override def supportsQuantifiers = true - override def createContext(): SolverContext = new SMTLibSolverContext(cmd, this) + override def supportsSoftAssert = true + override def createContext(debugOn: Boolean = false): SolverContext = new SMTLibSolverContext(cmd, this, debugOn) } -/** provides basic facilities to interact with any SMT solver that supports a SMTLib base textual interface */ -private class SMTLibSolverContext(cmd: List[String], val solver: Solver) extends SolverContext { - protected val debug: Boolean = false +object OptiMathSatSMTLib extends Solver { + private val cmd = List("optimathsat", "-optimization=true", "-model_generation=true") + override def name = "opti-math-sat-smtlib" + override def supportsConstArrays = true + override def supportsUninterpretedFunctions = true + override def supportsUninterpretedSorts = true + override def supportsQuantifiers = true + override def supportsSoftAssert = true + override def createContext(debugOn: Boolean = false): SolverContext = new OptiMathSatContext(cmd, debugOn) +} + +private class OptiMathSatContext(cmd: List[String], debug: Boolean) + extends SMTLibSolverContext(cmd, OptiMathSatSMTLib, debug) { + + // tracks if we currently have any soft asserts + private val hasSoftAssert = mutable.Stack[Boolean]() + hasSoftAssert.push(false) + + override def push(): Unit = { + hasSoftAssert.push(false) + super.push() + } + + override def pop(): Unit = { + hasSoftAssert.pop() + super.pop() + } + + override def softAssert(expr: BVExpr, weight: Int): Unit = { + require(solver.supportsSoftAssert, s"${solver.name} does not support soft asserts!") + if (!hasSoftAssert.top) { + hasSoftAssert.pop(); hasSoftAssert.push(true) + } + super.softAssert(expr, weight) + } + override protected def doCheck(produceModel: Boolean): SolverResult = { + // optimathsat does not actually optimize anything unless we tell it to + // (this is different from how z3, our other optimizing solver works) + // by default all `assert-soft` command are added to objective `I` and thus it should be enough to tell optimathsat + // to minimize that objective + if (hasSoftAssert.contains(true)) { // only add the minimize command if we have at least one soft assert active + writeCommand("(minimize I)") + } + super.doCheck(produceModel) + } +} + +/** provides basic facilities to interact with any SMT solver that supports a SMTLib base textual interface */ +private class SMTLibSolverContext(cmd: List[String], val solver: Solver, debug: Boolean) extends SolverContext { private var _stackDepth: Int = 0 override def stackDepth: Int = _stackDepth override def push(): Unit = { @@ -82,12 +167,20 @@ private class SMTLibSolverContext(cmd: List[String], val solver: Solver) extends case c: DeclareUninterpretedSymbol => writeCommand(serialize(c)) } + override def setOption(name: String, value: String): Unit = { + writeCommand(s"(set-option :$name $value)") + } + /** releases all native resources */ override def close(): Unit = { writeCommand("(exit)") - proc.stdin.flush() - Thread.sleep(5) - proc.destroyForcibly() + try { + proc.stdin.flush() + } catch { case _: java.io.IOException => /* ignore any IO exceptions */ } + if (proc.isAlive()) { + Thread.sleep(5) + proc.destroyForcibly() + } } override protected def doSetLogic(logic: String): Unit = getLogic match { case None => writeCommand(serialize(SetLogic(logic))) @@ -130,7 +223,13 @@ private class SMTLibSolverContext(cmd: List[String], val solver: Solver) extends // 1. the solver will terminate its answer with '\n' // 2. the answer will contain a balanced number of parenthesis var r = proc.stdout.readLine() + if (r == null) { + return None // the pipe might be broken + } while (countParens(r) > 0) { + if (!proc.isAlive()) { // did the solver crash while trying to produce the result? + throw new RuntimeException(s"Solver ${solver.name} crashed while producing a response:\n$r") + } r = r + " " + proc.stdout.readLine() } if (debug) println(s"$r") diff --git a/src/main/scala/chiseltest/formal/backends/smt/SMTModelChecker.scala b/src/main/scala/chiseltest/formal/backends/smt/SMTModelChecker.scala index 57aac36fc..8ad58047e 100644 --- a/src/main/scala/chiseltest/formal/backends/smt/SMTModelChecker.scala +++ b/src/main/scala/chiseltest/formal/backends/smt/SMTModelChecker.scala @@ -6,8 +6,6 @@ package chiseltest.formal.backends.smt import chiseltest.formal.backends._ import firrtl.backends.experimental.smt._ -import scala.collection.mutable - case class SMTModelCheckerOptions(checkConstraints: Boolean, checkBadStatesIndividually: Boolean) object SMTModelCheckerOptions { val Default: SMTModelCheckerOptions = @@ -26,20 +24,28 @@ class SMTModelChecker( override val prefix: String = solver.name override val fileExtension: String = ".smt2" - override def check(sys: TransitionSystem, kMax: Int): ModelCheckResult = { + override def check( + sys: TransitionSystem, + kMax: Int + ): ModelCheckResult = { require(kMax > 0 && kMax <= 2000, s"unreasonable kMax=$kMax") val ctx = solver.createContext() // z3 only supports the non-standard as-const array syntax when the logic is set to ALL val logic = if (solver.name.contains("z3")) { "ALL" } - else { "QF_AUFBV" } + else if (solver.supportsUninterpretedSorts) { "QF_AUFBV" } + else { "QF_ABV" } ctx.setLogic(logic) // create new context ctx.push() // declare/define functions and encode the transition system - val enc = new CompactEncoding(sys) + val enc: TransitionSystemSmtEncoding = if (solver.supportsUninterpretedSorts) { + new CompactSmtEncoding(sys) + } else { + new UnrollSmtEncoding(sys) + } enc.defineHeader(ctx) enc.init(ctx) @@ -113,7 +119,7 @@ class SMTModelChecker( private def getWitness( ctx: SolverContext, sys: TransitionSystem, - enc: CompactEncoding, + enc: TransitionSystemSmtEncoding, kMax: Int, failedAssertion: Seq[String] = Seq() ): Witness = { @@ -143,62 +149,12 @@ class SMTModelChecker( } -class CompactEncoding(sys: TransitionSystem) { - 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) - } +trait TransitionSystemSmtEncoding { + def defineHeader(ctx: SolverContext): Unit + def init(ctx: SolverContext): Unit + def unroll(ctx: SolverContext): Unit + def getConstraint(name: String): BVExpr + def getAssertion(name: String): BVExpr + def getSignalAt(sym: BVSymbol, k: Int): BVExpr + def getSignalAt(sym: ArraySymbol, k: Int): ArrayExpr } diff --git a/src/main/scala/chiseltest/formal/backends/smt/Solver.scala b/src/main/scala/chiseltest/formal/backends/smt/Solver.scala index 4cfa7a001..c1a9f7633 100644 --- a/src/main/scala/chiseltest/formal/backends/smt/Solver.scala +++ b/src/main/scala/chiseltest/formal/backends/smt/Solver.scala @@ -12,8 +12,10 @@ private[chiseltest] trait Solver { /** Constant Arrays are not required by SMTLib: https://rise4fun.com/z3/tutorialcontent/guide */ def supportsConstArrays: Boolean def supportsUninterpretedFunctions: Boolean + def supportsSoftAssert: Boolean + def supportsUninterpretedSorts: Boolean - def createContext(): SolverContext + def createContext(debugOn: Boolean = false): SolverContext } private[chiseltest] trait SolverContext { @@ -42,7 +44,8 @@ private[chiseltest] trait SolverContext { def runCommand(cmd: SMTCommand): Unit def queryModel(e: BVSymbol): Option[BigInt] def getValue(e: BVExpr): Option[BigInt] - def getValue(e: ArrayExpr): Seq[(Option[BigInt], BigInt)] + def getValue(e: ArrayExpr): Seq[(Option[BigInt], BigInt)] + def setOption(name: String, value: String): Unit /** releases all native resources */ def close(): Unit diff --git a/src/main/scala/chiseltest/formal/backends/smt/UnrollSmtEncoding.scala b/src/main/scala/chiseltest/formal/backends/smt/UnrollSmtEncoding.scala new file mode 100644 index 000000000..c0a5d5eae --- /dev/null +++ b/src/main/scala/chiseltest/formal/backends/smt/UnrollSmtEncoding.scala @@ -0,0 +1,94 @@ +// SPDX-License-Identifier: Apache-2.0 +// Author: Kevin Laeufer + +package chiseltest.formal.backends.smt + +import firrtl.backends.experimental.smt._ + +class UnrollSmtEncoding(sys: TransitionSystem) extends TransitionSystemSmtEncoding { + private def at(sym: SMTSymbol, step: Int): SMTSymbol = sym.rename(s"${sym.name}@$step") + private def at(name: String, step: Int): String = s"$name@$step" + private var currentStep = -1 + private val isSignal = (sys.inputs.map(_.name) ++ sys.signals.map(_.name) ++ sys.states.map(_.name)).toSet + + override def defineHeader(ctx: SolverContext): Unit = { + // nothing to do in this encoding + } + + override def init(ctx: SolverContext): Unit = { + require(currentStep == -1) + currentStep = 0 + // declare initial states + sys.states.foreach { state => + state.init match { + case Some(value) => + ctx.runCommand(DefineFunction(at(state.name, 0), Seq(), signalsAndStatesAt(value, 0))) + case None => + ctx.runCommand(DeclareFunction(at(state.sym, 0), Seq())) + } + } + // define the inputs for the initial state and all signals derived from it + defineInputsAndSignals(ctx, currentStep) + } + + override def unroll(ctx: SolverContext): Unit = { + val (prevStep, nextStep) = (currentStep, currentStep + 1) + // define next state + sys.states.foreach { state => + state.next match { + case Some(value) => + ctx.runCommand(DefineFunction(at(state.name, nextStep), Seq(), signalsAndStatesAt(value, prevStep))) + case None => + ctx.runCommand(DeclareFunction(at(state.sym, nextStep), Seq())) + } + } + + // declare the inputs and all signals derived from the new state and inputs + defineInputsAndSignals(ctx, nextStep) + + // update step count + currentStep = nextStep + } + + private def defineInputsAndSignals(ctx: SolverContext, step: Int): Unit = { + // declare inputs + sys.inputs.foreach(input => ctx.runCommand(DeclareFunction(at(input, step), Seq()))) + + // define signals + sys.signals.foreach { signal => + ctx.runCommand(DefineFunction(at(signal.name, step), Seq(), signalsAndStatesAt(signal.e, step))) + } + } + + private def signalsAndStatesAt(expr: SMTExpr, step: Int): SMTExpr = expr match { + case sym: SMTSymbol if isSignal(sym.name) => at(sym, step) + case other => SMTExprMap.mapExpr(other, signalsAndStatesAt(_, step)) + } + + private val isConstraint = sys.signals.filter(_.lbl == IsConstraint).map(_.name).toSet + override def getConstraint(name: String): BVExpr = { + require(isConstraint(name)) + require(currentStep >= 0) + at(BVSymbol(name, 1), currentStep).asInstanceOf[BVExpr] + } + + private val isBad = sys.signals.filter(_.lbl == IsBad).map(_.name).toSet + override def getAssertion(name: String): BVExpr = { + require(isBad(name)) + require(currentStep >= 0) + // we need to invert because we are asked for the assertion, not for the bad state! + BVNot(at(BVSymbol(name, 1), currentStep).asInstanceOf[BVExpr]) + } + + override def getSignalAt(sym: BVSymbol, k: Int): BVExpr = { + require(isSignal(sym.name)) + require(k <= currentStep) + at(sym, k).asInstanceOf[BVExpr] + } + + override def getSignalAt(sym: ArraySymbol, k: Int): ArrayExpr = { + require(isSignal(sym.name)) + require(k <= currentStep) + at(sym, k).asInstanceOf[ArrayExpr] + } +} diff --git a/src/main/scala/chiseltest/formal/package.scala b/src/main/scala/chiseltest/formal/package.scala index a14236d43..4dfc86ddb 100644 --- a/src/main/scala/chiseltest/formal/package.scala +++ b/src/main/scala/chiseltest/formal/package.scala @@ -7,5 +7,6 @@ package object formal { val CVC4EngineAnnotation = backends.CVC4EngineAnnotation val Z3EngineAnnotation = backends.Z3EngineAnnotation val BtormcEngineAnnotation = backends.BtormcEngineAnnotation + val BitwuzlaEngineAnnotation = backends.BitwuzlaEngineAnnotation val MagicPacketTracker = vips.MagicPacketTracker } diff --git a/src/test/scala/chiseltest/formal/FormalBackendOption.scala b/src/test/scala/chiseltest/formal/FormalBackendOption.scala index 744ce276e..a7406410c 100644 --- a/src/test/scala/chiseltest/formal/FormalBackendOption.scala +++ b/src/test/scala/chiseltest/formal/FormalBackendOption.scala @@ -15,6 +15,9 @@ object FormalBackendOption { case Some("z3") => Z3EngineAnnotation case Some("cvc4") => CVC4EngineAnnotation case Some("btormc") => BtormcEngineAnnotation + 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 case Some(unknown) => throw new RuntimeException(s"Unknown formal engine: $unknown") // default case None => Z3EngineAnnotation diff --git a/src/test/scala/chiseltest/formal/backends/smt/SMTLibResponseParserSpec.scala b/src/test/scala/chiseltest/formal/backends/smt/SMTLibResponseParserSpec.scala index 2c5971a18..41add1b8e 100644 --- a/src/test/scala/chiseltest/formal/backends/smt/SMTLibResponseParserSpec.scala +++ b/src/test/scala/chiseltest/formal/backends/smt/SMTLibResponseParserSpec.scala @@ -69,4 +69,16 @@ class SMTLibResponseParserSpec extends AnyFlatSpec { val expected = Seq((None, BigInt(0)), (Some(BigInt(0)), BigInt(1))) assert(SMTLibResponseParser.parseMemValue(in(array)) == expected) } + + it should "parse memory value responses from boolector" taggedAs FormalTag in { + val array1 = "((((mem@0 #b11111111) #b00000000000000000000000000000000)))" + // TODO + val array2 = "((((dut_entries@0 #b10) #b00111111111111110000000000000000)))" + // TODO + } + + it should "parse empty memory value from boolector" taggedAs FormalTag in { + val array = "()" + // TODO + } }