From b5cd0264732801ba5c9b6f475d5969dd5f9b420b Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Mon, 28 Oct 2024 13:23:50 +0000 Subject: [PATCH] Make nan boxing functions generic This simplifies the code and allows easily supporting the Q extension. --- model/riscv_fdext_regs.sail | 69 +++++++++------------------- model/riscv_insts_dext.sail | 4 +- model/riscv_insts_fext.sail | 4 +- model/riscv_insts_vext_fp_utils.sail | 10 ---- model/riscv_insts_zfa.sail | 18 ++++---- model/riscv_insts_zfh.sail | 4 +- 6 files changed, 37 insertions(+), 72 deletions(-) diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index bb6860121..ce6893a41 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -15,55 +15,30 @@ /* **************************************************************** */ /* NaN boxing/unboxing. */ -/* When 16-bit floats (half-precision) are stored in 32/64-bit regs */ -/* they must be 'NaN boxed'. */ -/* When 16-bit floats (half-precision) are read from 32/64-bit regs */ -/* they must be 'NaN unboxed'. */ -/* When 32-bit floats (single-precision) are stored in 64-bit regs */ -/* they must be 'NaN boxed' (upper 32b all ones). */ -/* When 32-bit floats (single-precision) are read from 64-bit regs */ -/* they must be 'NaN unboxed'. */ - -function canonical_NaN_H() -> bits(16) = 0x_7e00 -function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000 -function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000 - -val nan_box_H : bits(16) -> flenbits -function nan_box_H val_16b = - if (flen == 32) - then 0x_FFFF @ val_16b - else 0x_FFFF_FFFF_FFFF @ val_16b - -val nan_unbox_H : flenbits -> bits(16) -function nan_unbox_H regval = - if (flen == 32) - then if regval [31..16] == 0x_FFFF - then regval [15..0] - else canonical_NaN_H() - else if regval [63..16] == 0x_FFFF_FFFF_FFFF - then regval [15..0] - else canonical_NaN_H() - -val nan_box_S : bits(32) -> flenbits -function nan_box_S val_32b = { - assert(sys_enable_fdext()); - if (flen == 32) - then val_32b - else 0x_FFFF_FFFF @ val_32b -} -val nan_unbox_S : flenbits -> bits(32) -function nan_unbox_S regval = { - assert(sys_enable_fdext()); - if (flen == 32) - then regval - else if regval [63..32] == 0x_FFFF_FFFF - then regval [31..0] - else canonical_NaN_S() -} +// Canonical NaNs are used when an invalid boxed value is unboxed. +val canonical_NaN : forall 'n, 'n in {16, 32, 64, 128} . (implicit('n)) -> bits('n) +function canonical_NaN(n) = + match 'n { + // sign exponent significand + 16 => 0b0 @ ones(5) @ 0b1 @ zeros(9), + 32 => 0b0 @ ones(8) @ 0b1 @ zeros(22), + 64 => 0b0 @ ones(11) @ 0b1 @ zeros(51), + 128 => 0b0 @ ones(15) @ 0b1 @ zeros(111), + } -overload nan_box = { nan_box_H, nan_box_S } -overload nan_unbox = { nan_unbox_H, nan_unbox_S } +// When an n-bit float is stored in a larger m-bit register it is "boxed" +// by prepending 1s, which make it appear as a qNaN. +val nan_box : forall 'n 'm, 'n <= 'm . (implicit('m), bits('n)) -> bits('m) +function nan_box(n, x) = ones('m - 'n) @ x + +// When an n-bit float is stored ina smaller m-bit register it is "unboxed" +// - only if it is a valid boxed NaN. Otherwise a canonical NaN value is stored. +// TODO: Use right-open interval when available. See https://github.com/rems-project/sail/issues/471 +val nan_unbox : forall 'n 'm, 'm in {16, 32, 64, 128} & 'n >= 'm . (implicit('m), bits('n)) -> bits('m) +function nan_unbox(m, x) = if 'n == 'm then x else ( + if x['n - 1 .. 'm] == ones() then x['m - 1 .. 0] else canonical_NaN() +) /* **************************************************************** */ /* Floating point register file */ diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index c89e9f33b..40284831d 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -763,7 +763,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) & f_is_NaN_D(rs2_val_D)) then canonical_NaN_D() + let rd_val_D = if (f_is_NaN_D(rs1_val_D) & f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) else if f_is_NaN_D(rs1_val_D) then rs2_val_D else if f_is_NaN_D(rs2_val_D) then rs1_val_D else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D @@ -783,7 +783,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) & f_is_NaN_D(rs2_val_D)) then canonical_NaN_D() + let rd_val_D = if (f_is_NaN_D(rs1_val_D) & f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) else if f_is_NaN_D(rs1_val_D) then rs2_val_D else if f_is_NaN_D(rs2_val_D) then rs1_val_D else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index d74e8217a..c0d994d48 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -887,7 +887,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() + let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) else if f_is_NaN_S(rs1_val_S) then rs2_val_S else if f_is_NaN_S(rs2_val_S) then rs1_val_S else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S @@ -907,7 +907,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() + let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) else if f_is_NaN_S(rs1_val_S) then rs2_val_S else if f_is_NaN_S(rs2_val_S) then rs1_val_S else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S diff --git a/model/riscv_insts_vext_fp_utils.sail b/model/riscv_insts_vext_fp_utils.sail index d8e10d2e7..931e457c2 100755 --- a/model/riscv_insts_vext_fp_utils.sail +++ b/model/riscv_insts_vext_fp_utils.sail @@ -60,16 +60,6 @@ function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = { not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) } -/* Floating point canonical NaN for 16-bit, 32-bit and 64-bit types */ -val canonical_NaN : forall 'm, 'm in {16, 32, 64}. int('m) -> bits('m) -function canonical_NaN('m) = { - match 'm { - 16 => canonical_NaN_H(), - 32 => canonical_NaN_S(), - 64 => canonical_NaN_D() - } -} - /* Floating point classification functions */ val f_is_neg_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool function f_is_neg_inf(xf) = { diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 2b1f7c50f..3b56e01ea 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -52,7 +52,7 @@ function clause execute (RISCV_FLI_H(constantidx, rd)) = { 0b11100 => { 0x7800 }, /* 2^15 */ 0b11101 => { 0x7c00 }, /* 2^16 */ 0b11110 => { 0x7c00 }, /* +inf */ - 0b11111 => { canonical_NaN_H() }, + 0b11111 => { canonical_NaN(16) }, }; F_H(rd) = bits; RETIRE_SUCCESS @@ -101,7 +101,7 @@ function clause execute (RISCV_FLI_S(constantidx, rd)) = { 0b11100 => { 0x47000000 }, /* 2^15 */ 0b11101 => { 0x47800000 }, /* 2^16 */ 0b11110 => { 0x7f800000 }, /* +inf */ - 0b11111 => { canonical_NaN_S() }, + 0b11111 => { canonical_NaN(32) }, }; F_S(rd) = bits; RETIRE_SUCCESS @@ -150,7 +150,7 @@ function clause execute (RISCV_FLI_D(constantidx, rd)) = { 0b11100 => { 0x40e0000000000000 }, /* 2^15 */ 0b11101 => { 0x40f0000000000000 }, /* 2^16 */ 0b11110 => { 0x7ff0000000000000 }, /* +inf */ - 0b11111 => { canonical_NaN_D() }, + 0b11111 => { canonical_NaN(64) }, }; F_D(rd) = bits; RETIRE_SUCCESS @@ -175,7 +175,7 @@ function clause execute (RISCV_FMINM_H(rs2, rs1, rd)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN_H() + let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs1_val_H else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs2_val_H else if rs1_lt_rs2 then rs1_val_H @@ -205,7 +205,7 @@ function clause execute (RISCV_FMAXM_H(rs2, rs1, rd)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN_H() + let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs2_val_H else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs1_val_H else if rs2_lt_rs1 then rs1_val_H @@ -235,7 +235,7 @@ function clause execute (RISCV_FMINM_S(rs2, rs1, rd)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() + let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S else if rs1_lt_rs2 then rs1_val_S @@ -265,7 +265,7 @@ function clause execute (RISCV_FMAXM_S(rs2, rs1, rd)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); - let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() + let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN(32) else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S else if rs2_lt_rs1 then rs1_val_S @@ -295,7 +295,7 @@ function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN_D() + let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs2_val_D else if rs1_lt_rs2 then rs1_val_D @@ -325,7 +325,7 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); - let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN_D() + let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN(64) else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs1_val_D else if rs2_lt_rs1 then rs1_val_D diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index e484b4577..5422b46f8 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -378,7 +378,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = { let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) & f_is_NaN_H(rs2_val_H)) then canonical_NaN_H() + let rd_val_H = if (f_is_NaN_H(rs1_val_H) & f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) else if f_is_NaN_H(rs1_val_H) then rs2_val_H else if f_is_NaN_H(rs2_val_H) then rs1_val_H else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs1_val_H @@ -398,7 +398,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = { let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); - let rd_val_H = if (f_is_NaN_H(rs1_val_H) & f_is_NaN_H(rs2_val_H)) then canonical_NaN_H() + let rd_val_H = if (f_is_NaN_H(rs1_val_H) & f_is_NaN_H(rs2_val_H)) then canonical_NaN(16) else if f_is_NaN_H(rs1_val_H) then rs2_val_H else if f_is_NaN_H(rs2_val_H) then rs1_val_H else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs2_val_H