Thesis (M.Sc.) - Cairo University - Faculty of Engineering - Department of Electronics and Communication

Verification of floating point (FP) units is a difficult task to achieve, and the cost of post-production bugs is severe. This is due to dealing with a large bit stream of inputs; simulation based verification fails to cover all possible input combinations and hence does not guarantee a 100% bug free design. On the other hand, formal methods are efficient in verification of FP arithmetic, yet they require creating a formal model, they cannot work on an optimized version of a design and may fail with complex designs due to state space explosion. Our framework provides a new verification methodology that uses a constraint based random technique to generate test vectors for validating binary FP arithmetic instructions. The constraints used in our verification are written in system verilog (SV) language and can be solved with any SV constraint solver tool. For every arithmetic operation, the written constraints couple the operands, intermediate results, rounding direction and the result evaluation to comply with the FP IEEE standard (IEEE Std 754-2008). The new proposal is generic and can be used to verify any software or hardware binary FP design/library. Also, it proves feasibility and usefulness in finding bugs for various binary FP arithmetic operations for single and double precision formats

Issued also as CD