The floating point code is full of copy/pasted functions for 16/32/64 bit values. This is unnecessary since Sail has amazing support for generic code that works on all sizes. For example instead of
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 (sizeof(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 (sizeof(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 (sizeof(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 (sizeof(flen) == 32)
then regval
else if regval [63..32] == 0x_FFFF_FFFF
then regval [31..0]
else canonical_NaN_S()
}
overload nan_box = { nan_box_H, nan_box_S }
overload nan_unbox = { nan_unbox_H, nan_unbox_S }
You can do this:
// Canonical NaNs when an invalid boxed value is unboxed.
val canonical_NaN : forall 'n, 'n in {16, 32, 64} . (implicit('n)) -> bits('n)
function canonical_NaN(_retbits) =
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),
}
// 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(_retbits, 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.
// Unfortunately this is more complicated than it could be. See https://github.com/rems-project/sail/issues/471
val nan_unbox : forall 'n 'm, 'm in {16, 32, 64} & 'n >= 'm . (implicit('m), bits('n)) -> bits('m)
function nan_unbox(_retbits, x) = if 'n == 'm then x else (
if x['n - 1 .. 'm] == ones() then x['m - 1 .. 0] else canonical_NaN()
)
Here's another example of the duplication that could be refactored into a single function:
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
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(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
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
else /* (not rs2_lt_rs1) */ rs2_val_D;
accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
...
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
let rs1_val_S = F_or_X_S(rs1);
let rs2_val_S = F_or_X_S(rs2);
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(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
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
else /* (not rs2_lt_rs1) */ rs2_val_S;
accrue_fflags(fflags);
F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
...
function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = {
let rs1_val_H = F_or_X_H(rs1);
let rs2_val_H = F_or_X_H(rs2);
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(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
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
else /* (not rs2_lt_rs1) */ rs2_val_H;
accrue_fflags(fflags);
F_or_X_H(rd) = rd_val_H;
RETIRE_SUCCESS
}
And again for register access:
val rF_H : bits(5) -> bits(16)
function rF_H(i) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
nan_unbox(F(i))
}
val wF_H : (bits(5), bits(16)) -> unit
function wF_H(i, data) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = nan_box(data)
}
val rF_S : bits(5) -> bits(32)
function rF_S(i) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
nan_unbox(F(i))
}
val wF_S : (bits(5), bits(32)) -> unit
function wF_S(i, data) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = nan_box(data)
}
val rF_D : bits(5) -> bits(64)
function rF_D(i) = {
assert(sizeof(flen) >= 64);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i)
}
val wF_D : (bits(5), bits(64)) -> unit
function wF_D(i, data) = {
assert(sizeof(flen) >= 64);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = data
}
As Sail is more widely used, and the ISA community is becoming more familiar with the language, we should move the model towards more type safety and less repetition.
The floating point code is full of copy/pasted functions for 16/32/64 bit values. This is unnecessary since Sail has amazing support for generic code that works on all sizes. For example instead of
You can do this:
Here's another example of the duplication that could be refactored into a single function:
And again for register access: