The problem with FDIV is that function was not verified fully. AMD used ACL2 for complete symbolic verification of their FPU and discovered that their 50 milli

The problem with FDIV is that function was not verified fully. AMD used ACL2 for complete symbolic verification of their FPU and discovered that their 50 million tests test suite still allowed for some bugs to pass. Here's the same problem - in their approach, a function is specified by some of input-output pairs and their algorithm discovers BDD representation of such function. These input-output pairs may be incomplete to specify function fully, giving the opportunity for something akin to FDIV bug.