[Bug] VexRiscv FSGNJX.D Sign Bit Wrong

[canxin121]

VexRiscv FSGNJX.D Sign Bit Wrong

Reproduction

• Setup: RV32 + FD VexRiscv; run the same program on Spike for reference.
• Sequence:
  1. li x2, 0xe1f08df2; fmv.w.x f20, x2 → f20 = 0xffffffffe1f08df2 (sign = 1).
  2. li x2, 0xc051749b; fmv.w.x f25, x2 → f25 = 0xffffffffc051749b (sign = 1).
  3. fsgnjx.d f25, f25, f20.
  4. Store f25 to memory or read the register to check the result.

Issue

• Spike: f25 becomes 0x7fffffffc051749b; the sign bit is XORed to 0 as the spec requires.
• VexRiscv: f25 stays 0xffffffffc051749b; the sign bit does not flip, violating FSGNJX.D semantics.

[Dolu1990]

Hi,

This is by "design", see :
https://github.com/SpinalHDL/VexRiscv?tab=readme-ov-file#fpu

• Very specific, but SGNJ instruction will not mutate the value from/to F32/F64 (no NaN-boxing mutation)

It is related to Vexriscv internaly store floating point values into a recoded format.
While the behaviour isn't compliant, i do not expect it to create any practical issue. (?)