Re: [PATCH] checks: Add additional carry checks

[Paulo César Pereira de Andrade]

Em ter., 30 de abr. de 2024 às 10:34, Paul Cercueil
<paul@crapouillou.net> escreveu:

  Hi Paul,

> A substraction that results in a value with a different sign than the
> operands is not necesarily an underflow / overflow.
>
> For instance, these two substractions don't cause any underflow /
> overflow:
>   0 - 2 == -2
>   -1 - -1 == 0
>
> Add two new checks to verify that the implementations are compliant.

  Thanks. For all ports it uses the CPU to detect overflow/underflow.
For CPUS that do not have some kind of carry flag the code uses
signed/unsigned comparisons.

  Last time a regression was found it was in qemu. Fixed in the next
qemu release after a bug report. Lightning commit that tells about it is:

http://git.savannah.gnu.org/cgit/lightning.git/commit/?id=13536344bfe50e4346c4441fb226073e540bf7b4

  If you are interested. Something that was left unfinished was mulx
(no initial code) and adx that I did only a small experiment with?
http://git.savannah.gnu.org/cgit/lightning.git/commit/?id=0077bd184e5e64f7c8b40dffb0b9b3854572c4db

to be useful it probably would require some matrix
multiplication/inversion or parallel bignum math, but some of it could
be useful in Lightning.

Thanks!
Paulo


> Signed-off-by: Paul Cercueil <paul@crapouillou.net>
> ---
>  check/carry.tst | 2 ++
>  1 file changed, 2 insertions(+)
>
> diff --git a/check/carry.tst b/check/carry.tst
> index 180d896..615d964 100644
> --- a/check/carry.tst
> +++ b/check/carry.tst
> @@ -136,6 +136,8 @@ ok:
>         fadd(__LINE__,   , r0, r1, x7fe, x1, x7f)
>         tsub(__LINE__,   , r0, r1, x80,  x1, x7f)
>         fsub(__LINE__,   , r0, r1, x7f,  x1, x7fe)
> +       fsub(__LINE__,   , r0, r1, x0,   x1, ff)
> +       fsub(__LINE__,   , r0, r1, ff,   ff, x0)
>         tadd(__LINE__, _u, r0, r1, ff,   x1, x0)
>         fadd(__LINE__, _u, r0, r1, x7f,  x1, x80)
>         tsub(__LINE__, _u, r0, r1, x0,   x1, ff)
> --
> 2.43.0
>