Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix RV64F compilation, simplify fmv implementation, and make nan boxing functions generic #594

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
+35 −71
Open

Fix RV64F compilation, simplify fmv implementation, and make nan boxing functions generic #594

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
c7902ae
Make nan boxing functions generic
Timmmm Oct 31, 2024
0b8ff1e
Fix and simplify fmv execute clauses
Timmmm Oct 31, 2024
cb4e1a1
Update model/riscv_insts_fext.sail
Timmmm Nov 1, 2024
e204f5e
Update model/riscv_fdext_regs.sail
Timmmm Nov 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 29 additions & 47 deletions model/riscv_fdext_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,55 +15,37 @@

/* **************************************************************** */
/* 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
Timmmm marked this conversation as resolved.
Show resolved Hide resolved

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 }
// For backwards compatibility with code that existed before the
// generic version above.
function canonical_NaN_H() -> bits(16) = canonical_NaN(16)
function canonical_NaN_S() -> bits(32) = canonical_NaN(32)
function canonical_NaN_D() -> bits(64) = canonical_NaN(64)
function canonical_NaN_Q() -> bits(128) = canonical_NaN(128)

// 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"
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
// - only if it is a valid boxed NaN. Otherwise a canonical NaN value is stored.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not just stored, using as an input to some computation sees the same thing, right? As in this is just a property of any read of a non-NaN-boxed value?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And in particular transfer instructions (FLn/FSn/FMV.n.X/FMV.X.n) don't do this, despite storing in a smaller register.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yeah you're right I didn't really describe it correctly (and I think the spec is not especially readable). How about this:

// Except for floating-point transfer instructions (FSn and FMV.n.X),
// n-bit reads of a >n-bit floating point register "unboxes" the value stored
// in the register. If the register does not contain a valid boxed value
// then a canonical NaN value is returned instead.

and

// n-bit writes to a >n-bit floating point register "boxes" the value
// by prepending 1s, which turn it into a qNaN.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(un)boxes should be (un)box as you have plural reads/writes, but yes that looks ok to me otherwise

// 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
12 changes: 4 additions & 8 deletions model/riscv_insts_dext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -934,18 +934,14 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = {
}

function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = {
assert(xlen >= 64);
let rs1_val_D = F(rs1)[63..0];
let rd_val_X : xlenbits = sign_extend(rs1_val_D);
X(rd) = rd_val_X;
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
assert(xlen >= 64 & flen >= 64);
X(rd) = sign_extend(F(rs1)[63..0]);
RETIRE_SUCCESS
}

function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = {
assert(xlen >= 64);
let rs1_val_X = X(rs1);
let rd_val_D = rs1_val_X [63..0];
F(rd) = rd_val_D;
assert(xlen >= 64 & flen >= 64);
F(rd) = nan_box(X(rs1)[63..0]);
RETIRE_SUCCESS
}

Expand Down
8 changes: 2 additions & 6 deletions model/riscv_insts_fext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1061,16 +1061,12 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = {
}

function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = {
let rs1_val_S = F(rs1)[31..0];
let rd_val_X : xlenbits = sign_extend(rs1_val_S);
X(rd) = rd_val_X;
X(rd) = sign_extend(F(rs1)[31 .. 0]);
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
RETIRE_SUCCESS
}

function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = {
let rs1_val_X = X(rs1);
let rd_val_S = rs1_val_X [31..0];
F(rd) = nan_box (rd_val_S);
F(rd) = nan_box(X(rs1)[31..0]);
RETIRE_SUCCESS
}

Expand Down
10 changes: 0 additions & 10 deletions model/riscv_insts_vext_fp_utils.sail
View file
Open in desktop
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
Loading