From 967c04de6c02bef349df579cddbfcac8cf262e6d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 22 Mar 2022 16:03:57 +0100 Subject: Introduce float_conversion_default_nan parameter for float-float conversions For RISC-V we need to return the canonical NaN value if the argument of a float32->float64 or float64->float32 conversion is any NaN. This is in line with 11.3 from the RISC-V manual, the description of the conversion operations as well as what the spike ISA simulator and qemu do. Other platforms convert the NaN payload (by truncation or expansion) in float32->float64 and float64->float32 conversions. Fixes: #428 --- x86_32/Archi.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'x86_32/Archi.v') diff --git a/x86_32/Archi.v b/x86_32/Archi.v index 0a7f365b..775bdd44 100644 --- a/x86_32/Archi.v +++ b/x86_32/Archi.v @@ -59,6 +59,8 @@ Definition fma_invalid_mul_is_nan := false. Definition float_of_single_preserves_sNaN := false. +Definition float_conversion_default_nan := false. + (** Which ABI to use. *) Parameter win64: bool. (* Always false in 32 bits *) @@ -66,5 +68,5 @@ Global Opaque ptr64 big_endian splitlong default_nan_64 choose_nan_64 default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan - float_of_single_preserves_sNaN. - + float_of_single_preserves_sNaN + float_conversion_default_nan. -- cgit