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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #15 from Jacob Lifshay <programmerjake at gmail.com> ---
i researched how smtlib2 real and fp support could be added to yosys:
it'll likely be a huge amount of work if we try to add signals of real/fp types
since yosys assumes everything is only ever a list of bits.

therefore, I think the best route is to instead add a new built-in cell type,
where all inputs/outputs are still bitvectors/bools but internally it can do
real/fp ops. it would have a parameter with the expression to evaluate
(probably as a string). all of yosys would treat it as a black box, except for
the smtlib2 backend which would put the expression in the appropriate place in
the generated output.

nmigen could be extended with helper classes/functions to make it easier to
generate those expression cells, though that's not technically necessary.

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