FPU

Hello,

I found a discrepancy with soft float result for the following input vector : rmode = 0 op = 10 ( multiply) opa = 0xc1800300 opb = 0x00034000

The soft float result is 0x80340138 fpu100 result : 0x80068027

Please debug if this is still possible.

-JIang

I was able to formally verify the add operation, fpu100 is equivalent to the soft float 's float32_add.

-Jiang