512-bit multiplication · 2.61 million AND gates · 26.71 seconds · Independently checked 512-bit PAC certificate
In my previous post, I shared Parat v1.3 and its independently checkable proof for a 256-bit Yosys Booth multiplier. Since then, I have tested larger multiplier circuits and expanded the SAT benchmark suite.
512-bit multiplier: 26.71 seconds
I generated an unsigned 512×512-bit multiplier using carry-save compression followed by a final ripple adder.
The generated circuit contains:
- 2,614,272 AND gates
- 1,024 primary inputs and 1,024 output bits
- An approximately 59 MB ASCII AIGER file
Parat returned CORRECT MULTIPLIER in 26.71 seconds, with approximately 2.27 GB peak resident memory.
An independent bit-parallel simulator checked 64 operand pairs against exact integer multiplication. Every output bit matched.
A separate 512-bit Wallace multiplier: PAC certificate
I also have results from a separate 512-bit Wallace multiplier circuit, containing approximately 2.63 million AND gates.
For that circuit:
- PAC certificate generation took approximately 5–5.5 minutes.
- Independent verification with
pacheck2 took approximately 2.5 minutes.
- The recorded proof file was approximately 2.18 GB, with about 122 MB of polynomial data and 43 MB of specification data.
These are separate circuit experiments: the 26.71-second result above is for the carry-save/ripple architecture, while the independently checked PAC certificate belongs to the Wallace-circuit experiment.
Fault-injection testing
I modified individual gates in copies of the 512-bit carry-save/ripple circuit.
Three tested mutations—including an output-bit mutation, an early partial-product gate mutation and a near-final gate mutation—were detected as incorrect.
One middle-compressor-gate mutation did not produce a verdict within approximately 120 seconds. That case remains unresolved; the original correct circuit did return CORRECT MULTIPLIER.
Broader SAT benchmarks
On the tested Linux build:
| Benchmark |
Result |
| UF50 |
1,000/1,000 SAT models independently validated |
| UF250 |
100/100 SAT models independently validated |
| BMS |
500/500 SAT models independently validated |
| flat200 |
100/100 SAT models independently validated |
| SW100 |
1/1 SAT model independently validated |
| Generated regression suite |
115 expected-result checks passed; 6 exploratory cases inconclusive |
I also tested 176 SAT Competition 2005 industrial instances with a 10-second limit per instance. 142 SAT models were independently validated; 34 instances timed out.
For the UUF sets, reported UNSAT statuses matched expected results, but those results have not all been independently checked with proof certificates.
Limitations
The 26.71-second result applies to one generated circuit, not every multiplier architecture. One middle-gate mutation remains unresolved, and 34 industrial cases exceeded the time limit. Results from separate circuits should not be treated as if they came from one identical netlist.
Repository: https://github.com/himanshu161106-crypto/parat
The code was written by AI under my direction. The project ideas, mathematical approach, experiment design and testing were mine.
I'd appreciate technical feedback on improving the difficult middle-gate case and on additional large multiplier architectures worth testing.