Zfinx_verif.adoc

Zfinx verification

This document shows how to convert from tests for the F, D extensions to tests for Z[fd]inx

The same principles apply to any floating point extension.

NaN-boxing

If the instruction issued reads narrower source operands than FLEN there there is no NaN-boxing check.

For the cases covered by this document, then there is no NaN-boxing check for F*.S instructions issued on a Zdinx core.

This gives a difference in behaviour compared to a RV32D/RV64D core.

RV32D/RV64D:

//+1 correctly NaN-boxed
f2 = 0xffffffff3f800000
f3 = 0xffffffff3f800000

FADD.S f4, f3, f2

//returns the value 2, NaN-boxed
f4 = 0xffffffff40000000

//+1 incorrectly NaN-boxed
f2 = 0x000000003f800000
f3 = 0x000000003f800000

FADD.S f4, f3, f2

//returns the value sNaN, NaN-boxed
f4 = 0xffffffff7fc00000

The behaviour for RV32_Zdinx is as follows.

RV64_Zdinx:

//+1 correctly NaN-boxed
x2 = 0x3f800000
x3 = 0xffffffff // this register is not read
x4 = 0x3f800000
x5 = 0xffffffff // this register is not read

FADD.S x6, x2, x4

//returns the value 2, not NaN-boxed
x6 = 0x40000000

//+1 incorrectly NaN-boxed
x2 = 0x3f800000
x3 = 0x00000000
x4 = 0x3f800000
x5 = 0x00000000

FADD.S x6, x2, x4

//returns the value 2, not NaN-boxed - x7 is not written
x6 = 0x40000000

The behaviour for RV64_Zdinx is as follows.

RV32_Zdinx:

//+1 correctly NaN-boxed
x2 = 0xffffffff3f800000
x3 = 0xffffffff3f800000

FADD.S x4, x2, x3

//returns the value 2, NaN-boxed
x4 = 0xffffffff40000000

//+1 incorrectly NaN-boxed
x2 = 0x000000003f800000
x3 = 0x000000003f800000

FADD.S x4, x2, x3

//returns the value 2, NaN-boxed
x4 = 0xffffffff40000000

This behaviour needs checking for all instructions.

Note	Incorrect NaN-boxing means that the upper 32-bits are not 0xffffffff, so different patterns should be checked.

X0 handling

X0 reads as zero, and so results written to it are discarded. Exceptions are written to FFLAGS are still written even if the target is x0.

Register Pair handling

For RV32_Zdinx the source registers are read as register pairs for F*.D instructions.

If any register specifiers are odd then take an illegal instruction exception.

If a source/destination are x0 then the entire 64-bit source is read as zero, and the entire 64-bit destination is discarded - x1 is neither read nor written.

Deleted instructions

All deleted instructions cause illegal instruction exceptions - they are shown here for F and here for D.

Zfinx / non-Zfinx

Zfinx is a hardcoded architectural choice, it is not possible to enable or disable it. Therefore the tests must be generated / assembled / stored separately from the non-Zfinx tests.