When FLEN != XLEN there are some compilation issues in the fmv D instructions. Current code is:
function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = {
assert(sizeof(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;
RETIRE_SUCCESS
}
On RV64F the sizeof(xlen) >= 64) assertion passes, but then F(rs1)[63..0] can't compile because F(rs1) is only 32 bits. The fix is to add an assertion for flen too, since this function is only available when xlen==64 & flen==64.
Also the functions have a crazy level of intermediate variables and explicit type annotation. I'm using these much simpler versions:
function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = {
// A narrower n-bit transfer out of the floating-point registers will
// transfer the lower n bits of the register ignoring the upper FLEN-n bits.
X(rd) = sign_extend(F(rs1)[31 .. 0]);
RETIRE_SUCCESS
}
function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = {
// A narrower n-bit transfer, n<FLEN, into the f registers will create a valid
// NaN-boxed value.
F(rd) = nan_box(X(rs1)[31..0]);
RETIRE_SUCCESS
}
function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = {
assert(sizeof(xlen) >= 64 & sizeof(flen) >= 64);
X(rd) = F(rs1);
RETIRE_SUCCESS
}
function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = {
assert(sizeof(xlen) >= 64 & sizeof(flen) >= 64);
F(rd) = X(rs1);
RETIRE_SUCCESS
}
The spec for these for XLEN != FLEN is really hard to understand so it is nice to have concise Sail definitions.
When FLEN != XLEN there are some compilation issues in the
fmv
D instructions. Current code is:On RV64F the
sizeof(xlen) >= 64)
assertion passes, but thenF(rs1)[63..0]
can't compile becauseF(rs1)
is only 32 bits. The fix is to add an assertion forflen
too, since this function is only available when xlen==64 & flen==64.Also the functions have a crazy level of intermediate variables and explicit type annotation. I'm using these much simpler versions:
The spec for these for XLEN != FLEN is really hard to understand so it is nice to have concise Sail definitions.