To my knowledge, the function tuple<ui64, ui8> fdiv8.cpp(...) in fdiv8.cpp are the implemented CModel of 8-based SRTL algorithms
, which includes a 16/32/64 bit floating-point division implementation.
Note: In order to obtain the 32-bit division implementation CModel in fdiv8.cpp, I set the parameters of fmt, fz, dn, and rmode
in the fdiv8 function to 1, 0, 0, and 0, respectively.

SoftFloat-3e/source/f32_dediv. c is widely recognized as the gold standard for floating-point 32-bit division implementation CModel within the industry.
Note：The rounding mode of this CModel has been set to 0 by default.

So I used a formal verification tool to perform functional equivalence verification on the two CModels mentioned above (fdiv8.cpp and f32-div. c).
One of the counter-examples given is that when the input operands for division are 0x9 and 0x86, the division results of the two CModels(fdiv8.cpp and f32-div. c)
are 0x3D898D50 and 0x3D898D60, respectively.

The results provided by the above formal verification tools are consistent with those obtained by g++.

I would like to ask why there is such a difference between these two CModel models. Please help provide a reasonable explanation.
I look forward to your prompt response. Thank you very much!