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

[Jacob Lifshay]

On Wed, Oct 5, 2022, 09:00 lkcl <luke.leighton at gmail.com> wrote:

>
>
> On Wednesday, October 5, 2022, Jacob Lifshay <programmerjake at gmail.com>
> wrote:
> > On Wed, Oct 5, 2022, 03:58 lkcl via Libre-soc-dev <
> libre-soc-dev at lists.libre-soc.org> wrote:
> >>
> >> at https://libre-soc.org/nlnet_2022_opf_isa_wg/discussion/
> >>
> >> answers are needed extremely rapidly, they are under quite a high
> >> workload.
> >
> > I read through it, all the answers look fine to me, so imho all that's
> left is sending them to nlnet.
>
> magic. will give it another day.
>
> 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"

Jacob