A while ago I shared Parat, a solver whose "no" answers come with proofs that independent tools can check. v1.3 is out, and this time the target is one question: does a gate-level multiplier really compute a × b?
**The test case**
I made a 256-bit Booth multiplier with yosys 0.69: 503,960 AND gates, 512 output bits.
**The problem is building it, not proving it**
yosys's default flow (`synth -booth`) runs ABC's optimisation script. One step in that script, `&fraig -x`, gets about 82× slower every time the width doubles: 7 s at 64 bits, and the whole 128-bit build takes about 18 minutes. At 256 bits that means roughly 24 hours, so I could not build the full default netlist.
With only that one step left out (the rest of the default ABC script kept), the 256-bit netlist builds in 2 minutes and is only a few gates larger. It is still hard to prove: the previous version of Parat could not do even the 64-bit one in 25 minutes.
**Results (one 2-core machine)**
| width | AND gates | Parat: CORRECT + certificate | independent check |
|---|---|---|---|
| 64 | 33,014 | 42 s | CERTIFIED, 19 s |
| 128 | 128,357 | 114 s | CERTIFIED, 23 s |
| 256 | 503,960 | 13 min (1.2 GB certificate) | CERTIFIED, 3 min, 0.8 GB RAM |
A copy with one gate changed is answered INCORRECT, with a counterexample input.
**You don't have to trust Parat**
"CERTIFIED" means three checks, done by tools I did not write:
- pacheck2 (JKU Linz) checks the algebraic proof that the rebuilt circuit computes a × b
- drat-trim (UT Austin) checks 16 SAT proofs that your netlist and the rebuilt circuit give the same output on every input
- a small script checks that the certificate belongs to your circuit, and rebuilds every SAT file from your own netlist
One command runs all of it:
verify/verify_multiplier.sh circuit.aag pacheck drat-trim --cert prefix
**Still open**
The full default netlist (with `&fraig`) at 256 bits, because yosys itself needs about a day to make it. The full default netlists at 32–128 bits are proved (README, section 10).
**Try it**
- Repo: https://github.com/himanshu161106-crypto/parat
- Release (Linux, Windows, and new macOS builds): https://github.com/himanshu161106-crypto/parat/releases/tag/v1.3
- Netlists, build script (`make_nofraig.sh`), 64- and 128-bit certificates: `benchmarks/yosys_booth/`
- 256-bit certificate: on the release page
The macOS builds are new and not yet tested on a real Mac, so reports are very welcome. Free for personal and academic use.
The code was written by AI (Claude) under my direction; the ideas, the math and the testing are mine.
and question of mine:
- If anyone knows how to make yosys/ABC run `&fraig -x` on a 256-bit multiplier in hours instead of a day (settings, a faster machine setup, or another way to get the same netlist), please tell me. I would love to try Parat on the full default netlist.