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

[Mitchalsup]

Mitch AlsupMitchAlsup at aol.com

-----Original Message-----
From: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
To: Libre-RISCV General Development <libre-riscv-dev at lists.libre-riscv.org>
Cc: MitchAlsup <mitchalsup at aol.com>
Sent: Thu, Jan 16, 2020 5:54 am
Subject: Re: [libre-riscv-dev] [isa-dev] Re: FP transcendentals (trigonometry, root/exp/log) proposal



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.
You could do this, but it is easier to simply recognize that with a given number of bits of "Known accuracy" (which HAS to be at least 3-bits larger than the fraction) you need to look for 3-patterns that have the potential of spanning a rounding-decision-break-point.
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.