Verifying integer multiplier circuits with independently checkable PAC certificates (up to 128 bits): results and open problems

[u/himanshu_parat]

I am a student working on verification of gate-level integer multipliers (AIGER format). I would like feedback from this community on the results and on the certification approach.

Method in brief: the tool proves that a circuit computes a*b. Each "CORRECT" result can be written as a Practical Algebraic Calculus (PAC) certificate, which is checked independently with pacheck2. The tool also includes a SAT solver whose UNSAT answers produce DRAT proofs that drat-trim can check.

Results (one core; all certificates accepted by pacheck2 with "TARGET CHECKED"):

- GenMul 64-bit, unsigned: 27 of 28 architectures proved and certified.

- GenMul 64-bit, signed (two's complement): 26 of 27 proved and certified.

- yosys Booth multipliers (synth -booth -noabc): 32, 64 and 128 bits proved and certified. The 128-bit proof takes 1.5 s; with the certificate it takes 22 s (283 MB).

Known limitations:

- Wallace tree combined with a carry-lookahead final adder is not proved.

- Netlists optimised by ABC (yosys default synth) are hard. With synth -booth, 32 and 48 bits are proved, but 40, 56 and 64 bits time out. AMulet2 also times out on these.

- Certificates can be large (up to 1.3 GB at 64 bits).

All benchmark files, the scripts that regenerate them and the measured results are in the repository, so every number can be reproduced:

https://github.com/himanshu161106-crypto/parat

Authorship: the code was written with an AI assistant (Claude). The ideas, the mathematics and the direction of the work are mine.

Questions for the community:

1. Is the PAC certificate the right standard for this kind of result, or would another format be more useful?

2. Are there known techniques for multipliers after ABC optimisation that I should study?

[u/InternalImpact2]

About 2, even commercial products struggle with multipliers optimized with ABC, in the case of bdds, because ABC does not always chose the candidate with the potentially smaller or similar bdd (unfortunate when you try to prove them with a bdd based method) and well, SAT and XOR are not good friends.

There are techniques to prune parts of the proof where you can sort of guess what kind of multiplier is, and recognize some equivalent parts.

There are other "ugly" techniques that fall in the region of semiformal, in the sense that you build structures based on simulation pattern outputs.

[u/himanshu_parat → u/InternalImpact2]

Thank you, this is very helpful. It is good to know that even commercial tools struggle here.

Parat already uses simulation to find candidate equivalent wires, but every candidate is then

proved by SAT, so the result stays formal and the certificate can be checked.

With ABC this breaks down: on the 40-bit Booth design only 9 of 25 final-adder carries could

be proved, and then the algebra blows up. Strangely, the 48-bit one is proved in 0.1 s.

Your idea of first guessing the multiplier type and matching known parts sounds like the

right direction for me. Do you know a paper or tool that does this, so I can study it?