Verification of the floating-point unit presents a unique challenge in the field of processor verification. The particular complexity of this area stems from the vast test-space, which includes many corner cases that need to be targeted, and from the intricacies of the implementation of floating-point operations.
Main stream test generation tools, such as Genesys-Pro and AVPGEN, offer some control for FP test generation. However, their lack of focus and internal knowledge of the FP domain render them inadequate for providing a full solution to the FP verification problem. Test generation is supplemented by static legacy tests and by large quantities of purely random testing. Formal verification for floating-point units has also evolved significantly over the last decade. Formal verification techniques can be used to prove instruction correctness, but they require a significant investment of machine and manual work.
FPgen and the Floating-Point Generic Test-Plan (GTP) are built exactly for this purpose. They are the compilation of extensive knowledge and experience in the domain of floating-point verification.
FPgen's special purpose, XML-based input language gives users the power to define many interesting cases that may occur during the calculation of floating-point operations. With FPgen, users can create floating-point tests while forcing different attributes of the inputs, output, or intermediate results. Relations between the different operands are also supported and can be used to create special cases that are unlikely to be encountered when using pure random test generation (e.g., massive cancellation). For most cases, FPgen can generate dozens to hundreds of tests per second; this makes it possible to use FPgen in real time. The GTP gives the user a set of input files for FPgen, each covering a group of related interesting cases. This can save significant time in writing test-plans and in generating tests.