Underflow flag not set at subnormal/normal boundary

[gregdavill]

Background

I've been running functional tests/validation on this fpu, by running test vectors generated by testfloat. http://www.jhauser.us/arithmetic/TestFloat.html

I've noticed a class of bugs around the underflow flag. Here are some errors produced by testfloat:

Errors found in f32_mul, rounding near_even:
+01.000000  +7E.7FFFFF  => +01.000000 ....x  expected +01.000000 ...ux
+01.000000  -7E.7FFFFF  => -01.000000 ....x  expected -01.000000 ...ux
+01.7FFFFF  +7E.000000  => +01.000000 ....x  expected +01.000000 ...ux
 
Errors found in f32_mulAdd, rounding min:
+54.61FFFE  -02.70001F  -00.7FFFFF
=> -01.000000 ....x  expected -01.000000 ...ux
+00.000001  -7D.7FBFFF  -00.7FFFFF
=> -01.000000 ....x  expected -01.000000 ...ux

This effects the FMA operations using the Multiply operation, (MUL, F[N]MADD, F[N]MSUB). And the DIV operation (Using t-head div/sqrt)
This bug shows up for all rounding modes except RTZ.

Issue

The fact that this does not effect the RTZ rounding mode led me to this statement in the spec:

This bug is the corner case, where the final result is +/-b^emin, but the unbounded exponent range lies strictly between +/-b^emin. In this case it appears that the underflow flag should be set, which is what happens in softfloat, but not happening in the FMA or t-head DIV unit.

In RTZ mode you can never hit the case where you round from a subnormal result into a normal result.

[pascalgouedo]

Hi @gregdavill

Thanks for reporting this.
The FMADD/FMUL bugs was found by Formal Verification of CV32E40Pv2 as well and reported here.

For FDIV, I submitted an issue in T-Head-Semi/opene906 github repo #5.

[gregdavill]

Hey @pascalgouedo, Thanks for confirming. 👍

I was planning on opening a ticket upstream too, but figured I'd submit the PR here first and get input. and since you already have in repo patches applied to the opene906 div/sqrt unit.

[pascalgouedo]

Ah ok. Sorry to have "bypassed" you.
Formal Verification tool can not deal with those long sequential FDIV/FSQRT instructions.
So to confirm the bug and fix, we have to create a test in our CV32E40P verification environment.

[pascalgouedo]

By the way as you look familiar with all those Floating-Point stuff (who I am not), I wanted to let you know about another bug it seems your test suite didn't find:
#727 and #83

[gregdavill]

Ohh. That was detected by testfloat (http://www.jhauser.us/arithmetic/TestFloat-3/doc/TestFloat-general.html). But I didn't mention it in this issue as it's already been reported.

testfloat reports it like so:

Errors found in f32_to_i32_rx_minMag:
--
-9E.000000  => 80000000 v....  expected 80000000 .....

Thanks for the reminder, I was meaning to open a PR with a fix #97

[pascalgouedo]

Great. I am going to launch formal verification on it and will let you know.

[stmach]

I'm not sure I understand the issue correctly. RISC-V mandates detecting tininess after rounding, while your TestFloat results appear to indicate the detection of tininess before rounding. After rounding, the result is exactly $b^{emin}$, which is not strictly (i.e. $<$ not $\leq$) between $\pm b^{emin}$. Thus after rounding, there is no underflow.

This boundary case where an infinitely precise subnormal result is rounded to the smallest normal value is the only difference between detecting tininess before or after rounding - in the former case it will raise the flag while in the latter (and RISC-V) it won't.

[zarubaf]

@gregdavill did you run testfloat with the -tininessafter flag?

[gregdavill]

Thanks for you comments @stmach, this was picked up with testfloat/softfloat configured with tininessafter to match the riscv-spec.

I'm not an expert at the floating point standard, so I may have misinterpreted the spec, and how softfloat handles this.

I'm basing this issue and the fix on the wording in the spec, which specifically mentions an unbounded exponent range for detecting tininess before rounding.
Whereas when detecting before rounding you examine both the unbounded exponent range and the unbounded mantissa.

7.5 Underflow
-------------
The underflow exception shall be signaled when a tiny non-zero result is detected. For binary formats, this
shall be either:

a) after rounding—when a non-zero result computed as though the exponent range were unbounded
would lie strictly between ±b_(emin), or
b) before rounding—when a non-zero result computed as though both the exponent range and the
precision were unbounded would lie strictly between ±b_(emin).

This is the lines in softfloat responsible for flagging underflow. It checks this case, if the significant would overflow resulting in a normal result, the rounding bits flag an underflow.
https://github.com/ucb-bar/berkeley-softfloat-3/blob/master/source/s_roundPackToF32.c#L74

[pascalgouedo]

Hi,
I am not at all a Floating-Point expert either but to help to understand the pb, I wanted to mention that additionally to Berkeley float test suite, this FPU "error" has been reported by 2 other sources: Imperas Reference model and Siemens RISC-V Processor app.

[stmach]

All right, after some more thought and single-stepping through the SoftFloat execution, I see my error. I have been conflating "rounding" which strictly only concerns limiting precision to $p$ bits, to also include the further loss in precision caused by encoding subnormal values (which technically is induced by limiting exponent range - probably also because in HW we do the subnormal handling before caring about "rounding").

Since the infinitely precise results in the examples would not overflow into the normal range from rounding to 24 bits of precision alone, they are indeed still considered tiny after this rounding step, despite later being flushed into the normal range after losing a bit of precision due to being subnormal.

Sorry @gregdavill for causing a stir, the devil is (as always with FP) in the details😅

[gregdavill]

No worries, I was also confused when I first saw this error reported by softfloat, because I had the same connection of rounding as you, covering both precision and exponent bits.

Thanks for your expertise and taking a further look into this.

[zarubaf]

Fixed with release v0.8.1.