Dadda Multiplier(en.wikipedia.org)
en.wikipedia.org
Dadda Multiplier
https://en.wikipedia.org/wiki/Dadda_multiplier
7 comments
Note that for really, really fast multiplication, you throw all sorts of synthesis techniques at the problem. The space (of possible multiplier implementations) is large, and people have been grinding away at the problem for a long time (note Dadda is from 1965—think about how many people have written papers about how to write slightly faster multipliers in the past 57 years). I’m sure that if you sat down and looked at the multiplier in a modern high-performance core that it would be nigh-incomprehensible to human eyes.
I always thought that proving a multiplier is correct is an interesting problem. Sure you can check an 8 bit one with all combos, and then scale up the algorithm to more bits, but proving a given implementation doesn't have a bug in one of the gates is more difficult. A 64 bit multiplier has 2^128 possible inputs, so cannot be exhaustively checked. Perhaps formal proof or logic equivalence and handle this, but I'd be interested in seeing how.
> I always thought that proving a multiplier is correct is an interesting problem.
Induction proofs work fine. And 3SAT can check that your logic is equivalent.
The bigger issue is that multipliers are subject to runtime errors just like memory--so how do you check for that? The answer is that you build a multiplier that works on a smaller field (modulus) and then you check that against the big multiplier's result. If they differ, you flag.
I seem to recall that only Hitachi and IBM had processors that did this.
Induction proofs work fine. And 3SAT can check that your logic is equivalent.
The bigger issue is that multipliers are subject to runtime errors just like memory--so how do you check for that? The answer is that you build a multiplier that works on a smaller field (modulus) and then you check that against the big multiplier's result. If they differ, you flag.
I seem to recall that only Hitachi and IBM had processors that did this.
It is an interesting problem to think about, for sure.
My suspicion is that this kind of verification is amenable to breaking down into stages, essentially by drawing boxes around highly-connected regions, proving those properties exhaustively, then treating the various interconnects as between two black boxes with those known properties.
I'm sure there's some deep literature on this subject, I don't even know where to begin looking for it however.
My suspicion is that this kind of verification is amenable to breaking down into stages, essentially by drawing boxes around highly-connected regions, proving those properties exhaustively, then treating the various interconnects as between two black boxes with those known properties.
I'm sure there's some deep literature on this subject, I don't even know where to begin looking for it however.
There is indeed research and literature about this. For example “Formal verification of multiplier circuits using computer algebra”,
Daniela Kaufmann, see https://danielakaufmann.at/publications/
These kinds of methods are used in EDA Formal Verification tools to check real multipliers, FMAs, dot-products etc in CPU & GPU designs.
These kinds of methods are used in EDA Formal Verification tools to check real multipliers, FMAs, dot-products etc in CPU & GPU designs.