[Libre-soc-bugs] [Bug 196] Formal correctness proof needed for the IEEE754 FPU

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Fri May 13 13:30:56 BST 2022


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

--- Comment #20 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
there is an advantage to using nmigen rather than explicit yosys:
nmigen acts as a "cut-off" point by which we can represent the
FP numbers in a stable format.

if written explicitly in the representation that yosys has (after
patching) and it gets rejected upstream in favour of an alternative
implementation we're screwed: hundreds to thousands of one-line
changes needed to conform to the new yosys representation.

if however it's hidden behind a nmigen abstraction then there's
just one place that would need updating: nmigen.

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


More information about the libre-soc-bugs mailing list