Skip to content

[BUG] NaN-Boxing Violation in `fdiv.s`

Is there an existing CVA6 bug for this?

  • I have searched the existing bug issues

Bug Description

This bug tracks a divergence between CVA6 and reference implementations (Spike and Rocket) when executing a single-precision divide with round-toward-zero (fdiv.s ..., rtz). The assembly sequence that triggers the issue is reproduced below so the report remains self-contained:

li x2, 0xfa7d3198c1ddd216
fmv.d.x f17, x2
li x2, 0x7ce6e743bae084b4
fmv.d.x f23, x2
fdiv.s f21, f17, f23, rtz

What happens

  • The test loads raw 64-bit patterns into f17 and f23 using li + fmv.d.x.
  • These patterns are not NaN-boxed (their upper 32 bits are not all ones), so the operands should be treated as canonical NaNs in RV64 as mandated by the spec.
  • Spike and Rocket detect the missing NaN-boxing and retire f21 = 0xffffffff7fc00000.
  • CVA6 ignores the missing NaN-boxing, interprets the lower 32 bits directly, and returns f21 = 0xffffffff467cec8b.