[libre-riscv-dev] [isa-dev] Re: FP transcendentals (trigonometry, root/exp/log) proposal

[Luke Kenneth Casson Leighton]

On Thu, Jan 16, 2020 at 10:21 AM Jacob Lifshay <programmerjake at gmail.com>
wrote:

> On Thu, Jan 16, 2020, 02:00 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
> wrote:
>


> > > Yes. you just compute the output to a few more bits where the output is
> > > known to always be within a certain distance of the correct output,
> >
> >
> > sorry to be sounding dumb: the question thus becomes, "how do you know
> when
> > the output is always within a cer... etc etc " :)
>
>
> when approximating a mathematical function, you get an approximate output
> xa and you know by error analysis that the true mathematical output x is
> within distance delta of xa: x is in [xa - delta, xa + delta]
>

ah HA!  ok now it makes sense.  the error analysis is also a mathematical
function, which can be implemented *in hardware* and the error-quantity
computed along-side the actual output.

bartek: this is why i mentioned discussing on-list, because it ties in with
what you (privately) described to me: a way to do formal mathematical
proofs based on the error analysis.  would be very interested to hear your
thoughts.

l.