Skip to content

Commit

Permalink
Make nan boxing functions generic
Browse files Browse the repository at this point in the history 
This simplifies the code and allows easily supporting the Q extension.
  • Loading branch information
@Timmmm
Timmmm committed Oct 28, 2024
1 parent 1559013 commit b5cd026
Show file tree
Hide file tree
Showing 6 changed files with 37 additions and 72 deletions.
69 changes: 22 additions & 47 deletions model/riscv_fdext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_dext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
10 changes: 0 additions & 10 deletions model/riscv_insts_vext_fp_utils.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) = {
Expand Down
18 changes: 9 additions & 9 deletions model/riscv_insts_zfa.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_zfh.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit b5cd026

Please sign in to comment.