verifying EDA and compiler optimizations once and for all
At CAV 2026 we'll be presenting our new solver called ParaBit, which proves the correctness of EDA and compiler transformations using the theory of parametric bitvectors.
EDA Optimizations
More often than not the goal of electronic design automation (EDA) tools is to optimize a given circuit design.
One of the key mechanisms they use is rewriting, namely searching for a smaller circuit within our given design that matches some specific strucutre and replacing it with a more efficient implementation.
A classic example is replacing x*2 by x << 1, as the shift circuit is much cheaper than a multiplication.
It is imperative that these rewrites, which are baked into the EDA tools source code, are correct. If the EDA tool contains an incorrect rewrite, it can silently introduce bugs into the circuit design it’s optimizing. Hardware bugs can be extremely costly so are best avoided otherwise you may have very unhappy tool users. What makes this problem tricky, is that EDA rewrites often manipulate bitvectors of parametric widths, meaning a rewrite can apply to 16-bit or 32-bit bitvectors as well as all the widths in-between.
Like all good researchers, the solution is a new solver called ParaBit, that automatically proves the correctness of the rewrites. ParaBit first encodes the problem in a custom language then turns to equality saturation to construct a proof. We’re not the first to tackle this problem. Zvika Berger and the CVC5 team made some great progress with the PBV project on these kind of rewrite verification problems, providing an admittedly more general purpose solution than us. Our work differs from theirs, in that they attach bitwidths to operators whereas we attach bitwidths to operands removing the need for excessive extension operations. This lets us solve a good chunk more problems as we’ll see later on.
In July 2026, Luigi will be presenting this work at CAV, but further details can be found in the version we submitted (official version will be linked when published and in this version we’ll have proofs for all the axioms).
An Example
Much of the motivation for this project came from my own frustrations in developing EDA tool rewrites for the Rover project. We’ll take a ROVER rewrite as an example.
\[(q\geq r) \Rightarrow \underbrace{(a_p + (b_p + c_p)_q)_r}_{\textrm{lhs}} \equiv \underbrace{((a_p + b_p)_q + c_p)_r}_{\textrm{rhs}} \hspace{0.5cm}\]This rewrite says that when our width parameters satisfy \(q\geq r\), we can safely replace the lhs by the rhs. Our goal is to prove that this is correct for all possible width parameters. We use the subscript notation to denote the width of a bitvector, namely \(a_p\) denotes a \(p\)-bit bitvector. Similarly, \((b_p + c_p)_q\) means we add up two \(p\)-bit bitvectors and store the result in a \(q\)-bit bitvector.
To construct a proof we’ll be composing axioms of modular arithmetic (which is what our notation is really a shorthand for). Crucial for this proof is the following, where we totally remove the inner width \(u\).
\[u\geq v \Rightarrow (x + y_u)_v \equiv (x + y)_v.\]This essentially says that when I add up two bitvectors, if I store the result in a width smaller than one of the addends, then it doesn’t matter what the width of the inner addend is. It’ll just get truncated after the addition.
Under the given assumption \(q\geq r\), this axiom applies to both the lhs and rhs of the rewrite:
\[lhs \equiv (a_p + (b_p + c_p)_q)_r \equiv %\text{\{~using \eqref{eqn:mod_arith_axiom} with condition $q\geq r$~\}} \\ (a_p + (b_p + c_p))_r \\\] \[rhs \equiv ((a_p + b_p)_q + c_p)_r \equiv ((a_p + b_p) + c_p)_r\]Having removed any dependencies on \(q\), the two resulting expressions can now be shown equivalent by associativity of integer addition. This constitutes a series of axiom applications (which we separately verify) that proves the correctness of the rewrite whenever it is applied.
Whilst this looks simple, when we get more complex rewrites and have more axioms to combine finding this proof becomes much more tricky. This is where we turn to e-graphs and equality saturation, a constructive rewriting procedure where the order in which axioms are applied is not important. We can see how the e-graph encodes the steps that were written out here.
The ParaBit Solver
ParaBit is implemented in roughly 2k lines of Rust and is built on-top of the egg equality saturation library. ParaBit contains 99 axioms, each of which is verified in the Isabelle theorem prover. ParaBit takes problems specified in our custom BWLang language and discovers a sequence of axioms that prove the correctness of the rewrite using equality saturation.
If ParaBit is able to construct a proof, then ParaBit generates an associated Isabelle certificate script that can be checked independently to verify that our ParaBit proof is valid. This gives users an extra level of confidence in ParaBit’s proofs, so hopefully some industry folks might be willing to try it out!
To test out whether ParaBit is any good we gathered a couple of benchmark sets. Two from the software compilers community (Alive and Hydra) and two from the hardware domain (Rover and Industry). We compared against the PBV work from the CVC5 team referenced earlier. We see that ParaBit isn’t able to handle quite as many problems as PBV, due to current language limitations, but on the supported subset ParaBit is much more capable across all benchmarks.
Out of the 144 problems solved by ParaBit, we were able to successfully verify 142 of the generated Isabelle certificates. For two problems the proof production step actually ran out of memory. When ParaBit fails to produce a proof it is usually because the equality saturation step either times out or hit a memory limit.
There is clearly further work to be done to ParaBit to handle a larger class of problems and to improve performance across the problem set. The submitted version of the paper (official version will be linked when published) contains far more details and Luigi, John and I will all be at CAV in Lisbon in July 2026, so do come along if you’ve got any questions! If any of this work sounds interesting and you’re looking to collaborate or for Masters projects then get in touch.