Why uniform randomized testing might not be the best idea for validating that your base b = 2^64 arbitrary-precision long division implementation has properly implemented the correction step of quotient digit estimation:
I guess the "glass half full" angle on this is that in a non-adversarial situation, you might be able to get away with it. I encourage you to build mass-market divider circuits based on randomized testing; that worked well for Intel.
@TomF Right, I was just confused by your comment. It didn't work out for them in that instance and it's usually cited as the origin story of Intel's embrace of formal verification for at least parts of the processor.
Add comment