Berkeley HardFloat Release 1: Testing Using Verilog Simulation

John R. Hauser
2019 July 29

1. Introduction

2. Limitations

3. Acknowledgments and License

4. HardFloat Package Directory Structure

5. The finish_fail Verilog Macro

6. Specializing the HardFloat Modules to Test

7. Dependence on Berkeley TestFloat

8. Makefile Test Targets

8.1. Testing Conversions Between Standard and Recoded Floating-Point (fNToRecFN and recFNToFN)

8.2. Testing Conversions from Integer (iNToRecFN)

8.3. Testing Conversions to Integer (recFNToIN)

8.4. Testing Conversions Between Formats (recFNToRecFN)

8.5. Testing Addition and Subtraction (addRecFN)

8.6. Testing Multiplication (mulRecFN)

8.7. Testing Fused Multiply-Add (mulAddRecFN)

8.8. Testing Division and Square Root (divSqrtRecFN_small)

8.9. Testing Comparisons (compareRecFN)

8.10. Testing Multiple Functions

9. Interpreting the Test Output

10. Contact Information

1. Introduction

This document provides instructions for testing Berkeley HardFloat using a Verilog simulator and the test infrastructure supplied in the HardFloat package. Berkeley HardFloat is a hardware implementation of binary floating-point conforming to the IEEE Standard for Floating-Point Arithmetic. For basic documentation about HardFloat, see HardFloat-Verilog.html.

It is also possible to test HardFloat using Verilator, a free tool for converting a subset of synthesizable Verilog or SystemVerilog into C++ code. Test programs created using Verilator have been found to be much faster than some Verilog simulators. For equivalent instructions for testing HardFloat using Verilator, refer to HardFloat-test-Verilator.html.

The supplied tests for HardFloat depend on Berkeley TestFloat, which is not included in the HardFloat package. TestFloat in turn depends on Berkeley SoftFloat. The TestFloat and SoftFloat packages can be obtained from these Web pages:

http://www.jhauser.us/arithmetic/TestFloat.html
http://www.jhauser.us/arithmetic/SoftFloat.html

2. Limitations

The Verilog sources for HardFloat and its testbench are written to conform to the 2001 IEEE Standard for the Verilog language. The Verilog simulator must support this standard at a mimimum.

The supplied testbench can test only the common IEEE-defined formats supported by TestFloat, which are 16-bit half-precision, 32-bit single-precision, 64-bit double-precision, and 128-bit quadruple-precision.

The Makefile provided for running tests requires GNU make or a very close relative.

Adapting the testbench to overcome any of these limitations is possible but far from trivial.

3. Acknowledgments and License

The HardFloat package was written by me, John R. Hauser. The project was done in the employ of the University of California, Berkeley, within the Department of Electrical Engineering and Computer Sciences, first for the Parallel Computing Laboratory (Par Lab), then for the ASPIRE Lab, and lastly for the ADEPT Lab. The work was officially overseen by Prof. Krste Asanovic, with funding provided by these sources:

Par Lab: Microsoft (Award #024263), Intel (Award #024894), and U.C. Discovery (Award #DIG07-10227), with additional support from Par Lab affiliates Nokia, NVIDIA, Oracle, and Samsung.

ASPIRE Lab: DARPA PERFECT program (Award #HR0011-12-2-0016), with additional support from ASPIRE industrial sponsor Intel and ASPIRE affiliates Google, Nokia, NVIDIA, Oracle, and Samsung.

ADEPT Lab: ADEPT industrial sponsor Intel and ADEPT affiliates Google, Futurewei, Seagate, Siemens, and SK Hynix.

The following applies to the whole of HardFloat Release 1 as well as to each source file individually.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions, and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions, and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS “AS IS”, AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE, ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

4. HardFloat Package Directory Structure

The directory structure for the Verilog version of HardFloat is as follows:

doc
source
    8086-SSE
    ARM-VFPv2
    RISCV
test
    source
        Verilator
    build
        Verilator-GCC
        IcarusVerilog

The source files that define HardFloat’s modules are in the main source directory. The test directory has additional files used solely for testing. The test sources are of course all in test/source, while the test/build subdirectory contains a couple of example build targets. For testing using a Verilog simulator, the only example build target is for Icarus Verilog, an open-source Verilog simulator.

Although Icarus Verilog is a capable simulator for Verilog, as of 2019 it runs the HardFloat tests much slower than Verilator. If you have access to a faster Verilog simulator, the Icarus Verilog target can serve as an example for targeting the faster simulator. On the other hand, if Icarus Verilog is the fastest simulator available to you, Verilator is highly recommended instead. Instructions for running the supplied tests using Verilator are in HardFloat-test-Verilator.html.

As supplied, subdirectory IcarusVerilog contains only two files,

Makefile
config.make

used to build and execute all tests. The Makefile is written solely for GNU make. Another make variant is unlikely to work unless it is highly GNU-compatible.

5. The `finish_fail` Verilog Macro

The supplied testbench Makefile is designed to run a collection of floating-point tests and stop at the first one that fails. Stopping at the first failing test helps ensure that a failure will not go unnoticed amidst a sea of passing tests. To be aware that a test failed, the Makefile needs the Verilog simulator to return a failure exit status (usually a nonzero integer) if a test fails. Unfortunately, the 2001 Standard for Verilog does not define a standard way for Verilog code to influence a simulator’s exit status when a simulation ends.

HardFloat’s Verilog test sources have been written to invoke a macro called finish_fail when simulation should end with an exit status indicating failure. Executing

`finish_fail

is thus expected to act the same as

$finish

except that the Verilog simulator is expected to set its exit status to a failure value. This macro must be defined appropriately for the chosen Verilog simulator.

For Icarus Verilog, the Verilog sources have

`define finish_fail $stop

and then Icarus Verilog’s program for running a simulation, vvp, is given option -N, which makes $stop act as desired, exiting simulation with a status of 1, denoting failure.

If your Verilog simulator supports it, you can use the $fatal task defined by SystemVerilog:

`define finish_fail $fatal

However, it may be that your simulator doesn’t support $fatal or any equivalent mechanism. In the worst case, one can always fall back on

`define finish_fail $finish

and give up on the Makefile stopping on failures. Or use

`define finish_fail $stop

and allow failures to drop the user into the Verilog simulator’s interactive mode.

6. Specializing the HardFloat Modules to Test

To determine the particular HardFloat variant to test, the testbench requires that a Makefile macro, SPECIALIZE_TYPE, be defined with the name of a selected specialization subdirectory within HardFloat’s main source directory. As explained in HardFloat-Verilog.html, the HardFloat package includes these prepared specializations from which to choose:

8086-SSE
ARM-VFPv2
RISCV

Macro SPECIALIZE_TYPE can be defined either by editing the file config.make found in the IcarusVerilog directory alongside the Makefile, or by providing a definition for SPECIALIZE_TYPE among the arguments to the make command.

7. Dependence on Berkeley TestFloat

The HardFloat testbench depends on Berkeley TestFloat, which must be obtained and built separately. The latest version of TestFloat is available at Web page http://www.jhauser.us/arithmetic/TestFloat.html.

The testbench expects the reference floating-point used by TestFloat to exactly match the options chosen for building HardFloat. TestFloat’s reference floating-point is provided by the Berkeley SoftFloat library, which again must be obtained and built separately. The Web page for SoftFloat is http://www.jhauser.us/arithmetic/SoftFloat.html. To avoid spurious error reports for HardFloat, make sure that the SoftFloat library incorporated into TestFloat is built for exactly the same variant of IEEE floating-point as your HardFloat modules. In the documentation for both SoftFloat and HardFloat, this is referred to as specialization of the corresponding floating-point implementation.

The testbench Makefile requires that program testfloat_gen be directly executable by the make program. Usually this is achieved by modifying your PATH environment variable to include the directory containing testfloat_gen.

8. `Makefile` Test Targets

The Makefile in test/build/IcarusVerilog is the driver for building and executing tests. This Makefile supports a number of possible targets, each testing one or more HardFloat functions for all relevant rounding modes and other control parameters. In all cases, tests ultimately involve executing one or more commands of the form

testfloat_gen ... -prefix <control-args> <function> | vvp -N <compiled-Verilog-test-program>

The vertical bar (|) represents a pipe from the testfloat_gen program, which provides a sequence of test operands and expected results, to Icarus Verilog’s vvp, which executes a Verilog test program that was earlier “compiled” into a file with extension ‘.vvp’. The Verilog test program both invokes the specific module being tested and confirms that the module’s output matches what testfloat_gen expected.

The <control-args> are integers for extra module inputs such as control and roundingMode, depending on the module being tested. These get passed once from testfloat_gen to vvp ahead of the generated test cases, using the -prefix option of testfloat_gen. (Verilog’s “plusargs” could have been used instead, but the -prefix technique has the virtue of reducing the number of different Verilog features the tests depend on.)

Because testfloat_gen delivers floating-point values only in IEEE-standard form whereas the HardFloat modules require them to be in HardFloat’s recoded format, all tests must implicitly invoke module fNToRecFN to convert the IEEE-format values coming from testfloat_gen into their equivalent recoded forms. Hence, a HardFloat module is never really tested alone but rather together with fNToRecFN. It is always possible that a bug in the module being tested is masked by a countervailing bug in fNToRecFN. However, it is considered unlikely that any such bug in fNToRecFN would go undetected during the testing of all other HardFloat modules as well. In this respect, the testing of all modules serves collectively to test module fNToRecFN. Confidence in fNToRecFN then improves the likelihood that individual modules are correct independent of fNToRecFN.

Many Makefile targets are supported for running various sets of tests. The basic ones for testing individual HardFloat modules are these:

test-<level>-recFNToFN
test-<level>-iNToRecFN
test-<level>-recFNToIN
test-<level>-recFNToRecFN
test-<level>-addRecFN_add
test-<level>-addRecFN_sub
test-<level>-addRecFN
test-<level>-mulRecFN
test-<level>-mulAddRecFN
test-<level>-mulAddRecFN_add
test-<level>-mulAddRecFN_mul
test-<level>-divSqrtRecFN_small_div
test-<level>-divSqrtRecFN_small_sqrt
test-<level>-compareRecFN

where <level> is always either ‘level1’ or ‘level2’. The <level> component directly controls the -level option given to testfloat_gen, which determines the number and depth of tests performed. For example, the command to execute the complete set of “level 2” tests for module addRecFN is

make test-level2-addRecFN

Each test is performed for all formats supported by TestFloat (and for only those formats), which for floating-point is IEEE 16-bit half-precision, 32-bit single-precision, 64-bit double-precision, and 128-bit quadruple-precision. For each supported format, all relevant rounding modes and other control parameters are tested, as already mentioned.

The Makefile targets listed above are further dissected in subsections below.

Other targets are supported that automatically test more than one module in sequence:

test-<level>-all1
test-<level>-all2
test-<level>

For more about these, see subsection 8.10 below, Testing Multiple Functions.

The supplied tests all report status and error information in a common way. As it executes, each test writes status information to the standard error output, which should be the terminal screen by default. In order for this status to be displayed properly, the standard error stream should not be redirected to a file. Any discrepancies that are found are written to the standard output stream, which is easily redirected to a file if desired. Unless redirected, reported errors will appear intermixed with the ongoing status information in the output.

8.1. Testing Conversions Between Standard and Recoded Floating-Point (`fNToRecFN` and `recFNToFN`)

Makefile targets

test-<level>-recFNToFN

provide a means of testing round-trip conversions from an IEEE-standard floating-point format to the equivalent HardFloat recoded format and back again, through HardFloat modules fNToRecFN and recFNToFN.

That the target names reference only module recFNToFN and not fNToRecFN is consistent with all other tests. As explained at the head of this section, all tests with floating-point inputs implicitly invoke fNToRecFN to convert the IEEE-format values supplied by testfloat_gen into the recoded formats used by the HardFloat modules.

Testing can be restricted to a single TestFloat-supported format with one of these Makefile targets:

test-<level>-recF16ToF16
test-<level>-recF32ToF32
test-<level>-recF64ToF64
test-<level>-recF128ToF128

8.2. Testing Conversions from Integer (`iNToRecFN`)

Module iNToRecFN is tested by Makefile targets

test-<level>-iNToRecFN

Conversions from all source integer formats supported by TestFloat are tested, encompassing integers of sizes 32 bits and 64 bits, both unsigned and signed.

Testing can be restricted to a single integer size and a single floating-point destination format with one of these Makefile targets:

test-<level>-i32ToRecF16
test-<level>-i32ToRecF32
test-<level>-i32ToRecF64
test-<level>-i32ToRecF128
test-<level>-i64ToRecF16
test-<level>-i64ToRecF32
test-<level>-i64ToRecF64
test-<level>-i64ToRecF128

Each target tests conversions from both unsigned and signed integers of the specified size.

8.3. Testing Conversions to Integer (`recFNToIN`)

Module recFNToIN is tested by Makefile targets

test-<level>-recFNToIN

Conversions to all destination integer formats supported by TestFloat are tested, encompassing integers of sizes 32 bits and 64 bits, both unsigned and signed.

Testing can be restricted to a single floating-point source format and a single integer destination size with one of these Makefile targets:

test-<level>-recF16ToI32
test-<level>-recF16ToI64
test-<level>-recF32ToI32
test-<level>-recF32ToI64
test-<level>-recF64ToI32
test-<level>-recF64ToI64
test-<level>-recF128ToI32
test-<level>-recF128ToI64

Each target tests conversions to both unsigned and signed integers of the specified size.

8.4. Testing Conversions Between Formats (`recFNToRecFN`)

Makefile targets

test-<level>-recFNToRecFN

test module recFNToRecFN.

Testing can be restricted to a single source format and single destination format using one of these targets:

test-<level>-recF16ToRecF32
test-<level>-recF16ToRecF64
test-<level>-recF16ToRecF128
test-<level>-recF32ToRecF16
test-<level>-recF32ToRecF64
test-<level>-recF32ToRecF128
test-<level>-recF64ToRecF16
test-<level>-recF64ToRecF32
test-<level>-recF64ToRecF128
test-<level>-recF128ToRecF16
test-<level>-recF128ToRecF32
test-<level>-recF128ToRecF64

8.5. Testing Addition and Subtraction (`addRecFN`)

Makefile targets

test-<level>-addRecFN_add
test-<level>-addRecFN_sub

test module addRecFN, for input subOp = 0 and subOp = 1 respectively. Targets

test-<level>-addRecFN

combine both sets of tests (both addition and subtraction).

Testing can be restricted to a single TestFloat-supported format with one of these Makefile targets:

test-<level>-addRecF16_add
test-<level>-addRecF32_add
test-<level>-addRecF64_add
test-<level>-addRecF128_add

test-<level>-addRecF16_sub
test-<level>-addRecF32_sub
test-<level>-addRecF64_sub
test-<level>-addRecF128_sub

test-<level>-addRecF16
test-<level>-addRecF32
test-<level>-addRecF64
test-<level>-addRecF128

8.6. Testing Multiplication (`mulRecFN`)

Module mulRecFN is tested by Makefile targets

test-<level>-mulRecFN

Testing can be restricted to a single TestFloat-supported format with one of these targets:

test-<level>-mulRecF16
test-<level>-mulRecF32
test-<level>-mulRecF64
test-<level>-mulRecF128

8.7. Testing Fused Multiply-Add (`mulAddRecFN`)

Module mulAddRecFN is tested by Makefile targets

test-<level>-mulAddRecFN

However, testing is currently done only for input op = 0, because that is the only case for which testfloat_gen can supply test inputs.

Additional special targets,

test-<level>-mulAddRecFN_add
test-<level>-mulAddRecFN_mul

exist for testing mulAddRecFN in the roles of just addition (a × 1 + c) and just multiplication (a × b + 0). Used these ways, module mulAddRecFN is expected to behave the same as addRecFN and mulRecFN respectively (except possibly for specific NaN payload propagation in the case of addition).

Testing can be restricted to a single TestFloat-supported format with one of these targets:

test-<level>-mulAddRecF16
test-<level>-mulAddRecF32
test-<level>-mulAddRecF64
test-<level>-mulAddRecF128

test-<level>-mulAddRecF16_add
test-<level>-mulAddRecF32_add
test-<level>-mulAddRecF64_add
test-<level>-mulAddRecF128_add

test-<level>-mulAddRecF16_mul
test-<level>-mulAddRecF32_mul
test-<level>-mulAddRecF64_mul
test-<level>-mulAddRecF128_mul

8.8. Testing Division and Square Root (`divSqrtRecFN_small`)

Makefile targets

test-<level>-divSqrtRecFN_small_div
test-<level>-divSqrtRecFN_small_sqrt

test module divSqrtRecFN_small, for input sqrtOp = 0 and sqrtOp = 1 respectively.

Testing can be restricted to a single TestFloat-supported format with one of these targets:

test-<level>-divSqrtRecF16_small_div
test-<level>-divSqrtRecF32_small_div
test-<level>-divSqrtRecF64_small_div
test-<level>-divSqrtRecF128_small_div

test-<level>-divSqrtRecF16_small_sqrt
test-<level>-divSqrtRecF32_small_sqrt
test-<level>-divSqrtRecF64_small_sqrt
test-<level>-divSqrtRecF128_small_sqrt

8.9. Testing Comparisons (`compareRecFN`)

Module compareRecFN is tested by Makefile targets

test-<level>-compareRecFN

These targets test the module’s outputs against TestFloat’s comparison functions, lt, le, and eq.

Like all the others, testing can be restricted to a single format with one of these targets:

test-<level>-compareRecF16
test-<level>-compareRecF32
test-<level>-compareRecF64
test-<level>-compareRecF128

8.10. Testing Multiple Functions

A few Makefile targets combine larger collections of HardFloat functions. Targets named

test-<level>-all1

test all of the “one-operand” functions, the same as covered by these targets:

test-<level>-recFNToFN
test-<level>-iNToRecFN
test-<level>-recFNToIN
test-<level>-recFNToRecFN
test-<level>-divSqrtRecFN_small_sqrt

Likewise, the “two-operand” functions can all be tested using Makefile targets

test-<level>-all2

which combine these targets:

test-<level>-addRecFN
test-<level>-mulRecFN
test-<level>-mulAddRecFN_add
test-<level>-mulAddRecFN_mul
test-<level>-divSqrtRecFN_small_div
test-<level>-compareRecFN

Lastly, the simplest of Makefile targets,

test-<level>

encompass all defined tests at a given level, being a combination of:

test-<level>-all1
test-<level>-all2
test-<level>-mulAddRecFN

9. Interpreting the Test Output

The “errors” reported by the HardFloat tests may or may not really represent errors in HardFloat. For each test case tried, the results from HardFloat could differ from the expected results for several reasons:

The IEEE Floating-Point Standard allows for some variation in how conforming floating-point behaves. Two implementations can sometimes give different results without either being incorrect.
TestFloat’s trusted floating-point emulation could be faulty. This could be because there is a bug in the way the emulation is coded, or because a mistake was made when the code was compiled for the current system.
HardFloat’s Verilog testbench may not work properly, reporting differences that do not exist.
Lastly, HardFloat could actually be faulty.

It is the responsibility of the user to determine the causes for the discrepancies that are reported. Making this determination can require detailed knowledge about both the IEEE Standard and HardFloat’s recoded floating-point format. Assuming both TestFloat and the Verilog testbench are working properly, any differences found will be due to either the first or last of the reasons above.

For each reported error (or apparent error), a line of text is written to the default output. If a line would be longer than 79 characters, it is divided. The first part of each error line begins in the leftmost column, and any subsequent “continuation” lines are indented with a tab.

Each error reported is of the form:

<inputs>  => <observed-output>  expected <expected-output>

The <inputs> are the inputs to the operation. Each output (observed or expected) is shown as a pair: the result value first, followed by the exception flags.

For example, two typical error lines could be

140fffe00 180000100  => 041000000 03  expected 041000000 01
081000004 03ffffff8  => 041000000 03  expected 041000000 01

In the first line, the inputs are 140fffe00 and 180000100, and the observed result is 041000000 with flags 03. TestFloat’s result is the same but with different flags, 01. The two instances above were reported as errors because the exception flag results differ.

Each input and output value, including exception flags, is represented in raw hexadecimal. Floating-point inputs and outputs to HardFloat modules are usually encoded in HardFloat’s recoded form, so they appear in this form, not in a standard IEEE format. The only exceptions to this rule are the recFNToFN tests, for which the output is in a standard IEEE format.

10. Contact Information

At the time of this writing, the most up-to-date information about HardFloat and the latest release can be found at the Web page http://www.jhauser.us/arithmetic/HardFloat.html.

Par Lab:		Microsoft (Award #024263), Intel (Award #024894), and U.C. Discovery (Award #DIG07-10227), with additional support from Par Lab affiliates Nokia, NVIDIA, Oracle, and Samsung.
ASPIRE Lab:		DARPA PERFECT program (Award #HR0011-12-2-0016), with additional support from ASPIRE industrial sponsor Intel and ASPIRE affiliates Google, Nokia, NVIDIA, Oracle, and Samsung.
ADEPT Lab:		ADEPT industrial sponsor Intel and ADEPT affiliates Google, Futurewei, Seagate, Siemens, and SK Hynix.

Berkeley HardFloat Release 1: Testing Using Verilog Simulation

Contents

1. Introduction

2. Limitations

3. Acknowledgments and License

4. HardFloat Package Directory Structure

5. The finish_fail Verilog Macro

6. Specializing the HardFloat Modules to Test

7. Dependence on Berkeley TestFloat

8. Makefile Test Targets

8.1. Testing Conversions Between Standard and Recoded Floating-Point (fNToRecFN and recFNToFN)

8.2. Testing Conversions from Integer (iNToRecFN)

8.3. Testing Conversions to Integer (recFNToIN)

8.4. Testing Conversions Between Formats (recFNToRecFN)

8.5. Testing Addition and Subtraction (addRecFN)

8.6. Testing Multiplication (mulRecFN)

8.7. Testing Fused Multiply-Add (mulAddRecFN)

8.8. Testing Division and Square Root (divSqrtRecFN_small)

8.9. Testing Comparisons (compareRecFN)

8.10. Testing Multiple Functions

9. Interpreting the Test Output

10. Contact Information

5. The `finish_fail` Verilog Macro

8. `Makefile` Test Targets

8.1. Testing Conversions Between Standard and Recoded Floating-Point (`fNToRecFN` and `recFNToFN`)

8.2. Testing Conversions from Integer (`iNToRecFN`)

8.3. Testing Conversions to Integer (`recFNToIN`)

8.4. Testing Conversions Between Formats (`recFNToRecFN`)

8.5. Testing Addition and Subtraction (`addRecFN`)

8.6. Testing Multiplication (`mulRecFN`)

8.7. Testing Fused Multiply-Add (`mulAddRecFN`)

8.8. Testing Division and Square Root (`divSqrtRecFN_small`)

8.9. Testing Comparisons (`compareRecFN`)