[libre-riscv-dev] [Bug 274] Investigate how BSV performs Formal Verification and what can be Applied to FPUs

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=274

--- Comment #2 from Yehowshua <yimmanuel3 at gatech.edu> ---
The bsc source for generating a floating point adder is here:
https://github.com/B-Lang-org/bsc/blob/master/src/Libraries/Base3-Math/FloatingPoint.bsv#L1822

I'm not sure if it is formally verified.

-- 
You are receiving this mail because:
You are on the CC list for the bug.