[Libre-soc-dev] 2022-08-051 2nd stage grant questions

[lkcl]

On Wednesday, October 5, 2022, Jacob Lifshay <programmerjake at gmail.com>
wrote:

>> second set came in, just editing now
>> https://libre-soc.org/nlnet_2022_ongoing/discussion/
>
> full completion of all ieee754 formal proofs requires full exception
flags/traps handling, as well as correct rounding in all modes and
exception flags/traps for all fptrans instructions and formal correctness
proofs for all of fptrans (easily a year of work for fptrans formal
correctness, we'd have to develop and prove reference algorithms for nearly
all ops or just use a giant table lookup (limiting to f16 for unary and
f9-10 for binary ops) so we could have something to prove the hdl to be
equivalent to) -- infeasible in just a few months -- therefore I suggest
rephrasing the task to something like "additional progress on ieee754
formal proofs"

ok good catch.

> Jacob