[bsder]

> 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.