close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

Verify Floating-Point Hardware IP

Formal Verification of Floating-Point Hardware with Assertion-Based VIP


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.


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.

» Download the paper from DVCon US 2018


Get the OneSpin 360 DV-FPU App datasheet

For a technical description of the app, please read the OneSpin 360 DV-FPU App datasheet.


 I would like to recieve more technical information via mail.
By downloading this content, you comply with OneSpin's privacy policy and give your consent for the collection of the entered data. OneSpin Solutions will protect the information that is collected on this site as stated in the privacy policy. It will not be shared with, or sold to any third party. This declaration of consent is entirely voluntary and can be retrieved on our website and revoked at any time. Should you have any objections to the collection, processing and use of your personal data at a later stage, you can withdraw your declaration of consent at any time in the future, without giving any reasons, by writing to dpo@onespin.com.