Systems & Design

Formal Verification Of Floating-Point Hardware With Assertion-Based VIP

An alternative floating-point hardware verification approach based on a reusable, IEEE 754 compliant SystemVerilog arithmetic library.


Hardware for integer or fixed-point arithmetic is relatively simple to design, at least at the register-transfer level. If the range of values and precision that can be represented with these formats is not sufficient for the target application, floating-point hardware might be required. Unfortunately, floating-point units are complex to design, and notoriously challenging to verify. Since the famous 1994 Intel Pentium bug, many companies have investigated and successfully applied formal methods to this task. However, solutions often rely on a mix of the following: hard-to-use formal tools; highly specialized engineering skills; availability of a suitable executable model of the hardware; and significant, design-specific engineering effort. In this paper, we present an alternative floating-point hardware verification approach based on a reusable, IEEE 754 compliant SystemVerilog arithmetic library. While not addressing all verification challenges, this method enables engineers to set up a formal testbench and uncover deep corner-case bugs with minimal effort. Results from industrial applications are reported.

Click here to continue reading.


Mark Curry says:

Sigh, the first sentence in the paper states (a too common) misconception: “Floating-point (FP) representations of real numbers have significant advantages over fixed-point, particularly as, given a certain bit-width for their binary encoding, they may cover a much wider range of values WITHOUT LOSING PRECISION.”

This is simply not true. Given a number of bits, converting from fixed point to floating point SACRIFICES precision in order to gain range. For a given number of bits one cannot attain the same precision in floating point while also gaining range. You can’t get something for nothing.

This sacrifice of precision in order to gain range also comes at the cost of significant complexity. This complexity is part of the paper’s goal – how to verify this complex logic (which is a very valid goal).

But requirements for floating point in SystemVerilog designs is the very rare exception, not the rule.

Sergio Marchese says:

Thank you for your comment Mark. Indeed, the statement in the paper does not take into account specific conversion scenarios from fixed-point numbers.
I am glad you agree that FPU hardware is complex and requires careful verification. As you have noted, the focus of the article is about how to address the verification challenge.
I also agree that many applications do not require floating-point hardware. Having said that, OneSpin has several customers developing FPU hardware (RTL).

Leave a Reply

(Note: This name will be displayed publicly)