Formal verification of IEEE 754 floating-point hardware
Floating-point arithmetic is key in many algorithms for scientific calculations, audio coding, digital filters, and computer graphics. In general, whenever input data covers a large dynamic range of values, floating-point arithmetic provides a level of precision that fixed-point arithmetic cannot offer. Hardware floating-point units (FPUs) are crucial to improve performances and reduce power consumption. FPU intellectual property (IP) blocks are often integrated in both ASIC and FPGA chips. They are present in safety-critical systems, for example for automotive applications, or instrumentation and process control in nuclear power plants (NPPs) and other industrial applications, but also in hardware for data centers and machine learning applications.
The FPU App verifies that the result of arithmetic operations, as computed by the hardware floating-point unit (FPU), accurately matches the IEEE 754 standard specification. All exception flags, invalid operation, division by zero, inexact result, underflow or tininess, and overflow, are also checked. All major operations are supported out of the box with the exclusion of division.
Flexibility and configurability are crucial in the solution to any complex verification challenge. The FPU App supports all four standard rounding modes: roundTowardZero, roundTiesToEven, roundTowardPositive, roundTowardNegative. Half, single or double precision formats can be selected at a flick of a switch. Less common precisions can be accommodated with limited additional effort. Users can also selectively disable checks, for example to ignore specific flags or entire operations not yet implemented in hardware. Should the hardware feature intended deviations from the IEEE 754 standard, a set of high-level functions enables an elegant customization of the checks that precisely match such deviations. Conversion functions between different floating-point formats as well as between signed integers and floating-point numbers are also provided.
OneSpin’s FPU App dramatically increases development speed and quality of IEEE 754 floating-point hardware. It is easy to setup and does not require formal expertise.
The FPU App is seamlessly integrated with the OneSpin 360 verification platform. Engineers can use all 360 DV advanced debug features. Additional dedicated debug capabilities are available, including a convenient high-level view of floating-point data types that considerably speed up the analysis and debug process. Complexity issues are mitigated through the automatic selection of OneSpin’s most appropriate, best-in-class proof engines and strategies.
Nicolae Tusinschi about Verification of Floating-Point Hardware Designs
Verification of floating-point hardware designs has long been considered a significant challenge for formal tools. FPUs combine the mathematical complexity of floating-point arithmetic with a wide range of special cases that require complex control paths.
Most successful applications of formal verification to FPUs have involved domain experts and hard-to-use specialized tools. In contrast, Nicolae’s talk presents a customer case study in which Xilinx verified a real-world floating-point design using OneSpin’s formal tools and a readable, easy-to-use SystemVerilog assertion-based verification library for the IEEE 754 standard. The talk includes examples of assertions, bugs found, and runtimes on the customer design.
Xilinx verifies Floating-Point Hardware IP with OneSpin FPU App
Complex arithmetic is a well-known challenge for formal verification. Nevertheless, Xilinx required a rigorous, exhaustive verification of its floating-point hardware, including the multiplication operation, something that simulation cannot achieve. Read more on how the Xilinx team deployed the OneSpin FPU App, the effort required, and the results they achieved.
Get the OneSpin 360 DV-FPU App datasheet
For a technical description of the app, please read the OneSpin 360 DV-FPU App datasheet.