sampsyo
commented
9 months ago This sounds VERY COOL; I can't wait to see how this turns out! Thanks for the detailed discussion of the evaluation plan.
@NgaiJustin and I had a chance to chat synchronously this morning, and we talked about what I think may be one of the most important issues here: having a test oracle. (That is, a way to check whether the interpreter is running correctly. By analogy, if you were doing a project to implement a Bril interpreter, you could check a set of programs/inputs against the behavior of the reference interpreter, brili.) Since there is no straightforward BTOR2 interpreter that exists yet, this will present a bit of a problem.
We talked about a few options:
- Maybe btorsim can be abused as an interpreter. But @NgaiJustin and I agree that this probably would entail actually hacking the interpreter (modifying the actual C++); the necessary interfaces to supply input are not currently present.
- Have the interpreter generate witnesses that btorsim then checks. This would require emitting the result of interpretation in BTOR2's official witness format.
- Since the motivation for this involves not just executing arbitrary BTOR2 programs but ones generated from Verilog, you could use Verilog simulation (Verilator or Icarus Verilog) as the test oracle. That is, given a test program $v$, run $\text{Verilator}(v) = \text{your-thing}(\text{yosys}(v))$. One possible problem here is defining what the "output" of a Verilog simulation is; this is probably not too hard for Calyx primitives but may be harder for PicoRV32 (for instance).
One more possible option occurs to me just now: abuse Boolector as an interpreter! It has a Python API. You could theoretically make an interpreter by loading up a BTOR file, adding constraints on the inputs, and then asking the solver what the outputs must be. Hypothetically!
What will you do? We plan to implement an interpreter for BTOR2 in Rust.
BTOR is a format for quantifier-free formulas involving bit-vectors and arrays with SMT-LIB semantics but also provides sequential extensions for specifying word-level model checking problems with registers and memories [1]. BTOR2 is an extension to BTOR that introduces explicit sort declarations and allows for explicit initialization of registers and memories. BTOR2 also extends sequential features, incorporating elements like witnesses, invariants, fairness constraints, and liveness properties [1].
The authors of the paper BTOR2 , BtorMC and Boolector 3.0 have released a series of tools (in this Github repo) among which contains a witness simulator, random simulator and a BTOR2 parser. However, to the best of our knowledge, as of today, there is no existing BTOR2 interpreter for specified inputs.
Additionally, the concise nature of BTOR2 presents fun opportunities. Given its compact syntax, we also intend to explore potential optimization opportunities!
How will you do it? We will learn the semantics of BTOR2 and learn about optimizations for interpreters by reading the reference Bril interpreter and the blog post for the fast Bril interpreter. We’ll incorporate the same techniques into our interpreter (and learn Rust along the way).
How will you empirically measure success? To empirically measure success, we will first benchmark our interpreter on random inputs and compare it against the already existing random simulator to see how it compares. We will also write a naive version of the interpreter without the optimizations we add and compute how much of an improvement each individual optimization has over the baseline naive interpreter. We will use wall-clock time on one standardized machine as the metric to compare each version of the interpreter against, and we will also need to generate a robust benchmark suite of programs to test on. As one of the intentions for the project is to be later integrated into the Calyx ecosystem to serve as a drop-in replacement for the current Calyx interpreter, we will be using the generated BTOR2 primitives as a target to measure performance. If this suite of BTOR2 files turns out to be too small we will look to simulate on the translation of the real-world (System) Verilog designs from various open source projects (ZipCPU, PicoRV32, PonyLink, riscv-formal) as mentioned in the paper [1].
References: [1] Niemetz, A., Preiner, M., Wolf, C., & Biere, A. (2018). Btor2 , BtorMC and Boolector 3.0. International Conference on Computer Aided Verification.
Team members: @NgaiJustin @SanjitBasker @obhalerao