A Formal Model and Efficient Traversal Algorithm for Generating Testbenches for Verification of IEEE Standard Floating Point Division

We utilize a formal model of division for determining a testbench of p-bit (dividend, divisor) pairs whose output 2p-bit quotients have properties characterizing these instances as the most challenging for verifying any division algorithm design and implementation. Specifically, our test suites yield 2p-bit quotients where the leading p-bits traverse all or a pseudo-random sample of leading bit combinations, and the next p-bits comprise a round bit followed by (p-1) identical bits. These values are proven to be closest to the p-bit quotient rounding boundaries and shown to possess other desirable coverage properties. We introduce an efficient method of generating these testbenches. We also describe applications of these testbenches at the design simulation stage and the product evaluation stage