Browse Prior Art Database

Method for Computing Reference Results for Floating Point Operations

IP.com Disclosure Number: IPCOM000031133D
Original Publication Date: 2004-Sep-14
Included in the Prior Art Database: 2004-Sep-14
Document File: 3 page(s) / 63K

Publishing Venue

IBM

Abstract

The disclosed method describes an implementation of a Floating-Point reference model for multiply-and-add instructions, ensuring correctness by effectively computing the infinitely precise reference result as defined in the IEEE 754 standard. From this intermediate result the final result can be easily obtained.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 41% of the total text.

Page 1 of 3

Method for Computing Reference Results for Floating Point Operations

Floating-point units (FPU) are typically verified by comparing the FPU implementation against a reference model derived from the processor's architectural specification. The verification poses several challenges, one of which is the reliable computation of the reference result of a given floating point operation. The problem is complex because many different cases have to be considered, such as different overlap regions between the operands. For example, during an addition the operands may not overlap, may partly overlap, or they may fully overlap. In the first case, the smaller operand is only used as a so called sticky bit. In the second case, the two operands have to be added, but no massive cancellation is possible. In the third case, the operands are added and massive cancellation is possible, which then has to be taken into account during a normalization shift later on.

This leads to the problem that the development of the reference code is itself a complex and error-prone task. Furthermore, the reference code is, to some extent, related to/modeled after the implementation of the FPU under test, e.g. in the distinction of the various overlap cases. These factors together may result in a situation where there isn't much confidence in the correctness of the reference code itself.

When verifying the FPU using formal methods or underapproximate methods such as semi-formal techniques or simulation it is desirable to transform the reference model into a netlist for ease of application of these methods. This netlist is then compared to the netlist derived from the FPU under test. A reference FPU modeled in a programming language such as C cannot be easily transformed into a netlist.

This invention describes the modeling of a reference FPU such that it attempts to alleviate all of the drawbacks listed above. We propose a method to model the computation of the reference result in a manner that greatly simplifies the complexity, which in turn means that it is not as error-prone as the typical implementation in a programming language such as C. Additionally, the presented reference FPU can be easily implemented in a hardware description language, such as VHDL. Hence, the reference can be used for formal or semi-formal FPU verification much more effectively than compiled code reference model obtained from modeling it in a programming language. Since the reference FPU is implemented so simply it can be independently verified easily, either by code review by experts or subjecting the reference FPU to verification itself. The simplicity of the reference model also precludes the need to model it on the implementation in anyway thereby giving additional confidence in any verification of the FPU under test performed against it.

The method works by transforming the input numbers from floating point format into a fixed point format (which is much wider in terms of vector lengt...