Skip to content

Commit

Permalink
Simplify float by making F_or_X accessors generic
Browse files Browse the repository at this point in the history 
Similar to the `F_box` accessor, these can be generic. They just need a special case for xlen == 32 when reading/writing 64-bit floats which are split over two registers when using Zfinx.
  • Loading branch information
@Timmmm
Timmmm committed Apr 4, 2024
1 parent eb681d3 commit cf7553b
Show file tree
Hide file tree
Showing 5 changed files with 141 additions and 187 deletions.
64 changes: 11 additions & 53 deletions model/riscv_fdext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,76 +215,34 @@ overload F_box = { rF_box, wF_box }
// Access functions that access X registers if Zfinx (float in X) is enabled
// (mutually exclusive with the F/D extensions), otherwise F registers.

val rF_or_X_H : regidx -> bits(16)
function rF_or_X_H(i) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_box(i)
else X(i)[15..0]
}

val rF_or_X_S : regidx -> bits(32)
function rF_or_X_S(i) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_box(i)
else X(i)[31..0]
}

val rF_or_X_D : regidx -> bits(64)
function rF_or_X_D(i) = {
assert(sizeof(flen) >= 64);
val rF_or_X : forall 'n, 'n in {16, 32, 64} . (implicit('n), regidx) -> bits('n)
function rF_or_X(_n, i) = {
assert(sizeof(flen) >= 'n);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_box(i)
else if sizeof(xlen) >= 64
then X(i)[63..0]
else {
else if sizeof(xlen) == 32 & 'n == 64 then {
assert(i[0] == bitzero);
if i == zeros() then zeros() else X(i + 1) @ X(i)
}
} else X(i)['n - 1 .. 0]
}

val wF_or_X_H : (regidx, bits(16)) -> unit
function wF_or_X_H(i, data) = {
assert(sizeof(flen) >= 16);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_box(i) = data
else X(i) = sign_extend(data)
}

val wF_or_X_S : (regidx, bits(32)) -> unit
function wF_or_X_S(i, data) = {
assert(sizeof(flen) >= 32);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_box(i) = data
else X(i) = sign_extend(data)
}

val wF_or_X_D : (regidx, bits(64)) -> unit
function wF_or_X_D(i, data) = {
assert (sizeof(flen) >= 64);
val wF_or_X : forall 'n, 'n in {16, 32, 64} . (regidx, bits('n)) -> unit
function wF_or_X(i, data) = {
assert(sizeof(flen) >= 'n);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_box(i) = data
else if sizeof(xlen) >= 64
then X(i) = sign_extend(data)
else {
else if sizeof(xlen) == 32 & 'n == 64 then {
assert (i[0] == bitzero);
if i != zeros() then {
X(i) = data[31..0];
X(i + 1) = data[63..32];
}
}
} else X(i) = sign_extend(data)
}

overload F_or_X_H = { rF_or_X_H, wF_or_X_H }
overload F_or_X_S = { rF_or_X_S, wF_or_X_S }
overload F_or_X_D = { rF_or_X_D, wF_or_X_D }
overload F_or_X = { rF_or_X, wF_or_X }

/* register names */

Expand Down
86 changes: 43 additions & 43 deletions model/riscv_insts_dext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,9 +80,9 @@ mapping clause encdec =
/* Execution semantics ================================ */

function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
let rs1_val_64b = F_or_X_D(rs1);
let rs2_val_64b = F_or_X_D(rs2);
let rs3_val_64b = F_or_X_D(rs3);
let rs1_val_64b = F_or_X(64, rs1);
let rs2_val_64b = F_or_X(64, rs2);
let rs3_val_64b = F_or_X(64, rs3);

match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Expand All @@ -96,7 +96,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
FNMADD_D => riscv_f64MulAdd (rm_3b, f_negate (rs1_val_64b), rs2_val_64b, f_negate (rs3_val_64b))
};
accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_64b;
F_or_X(rd) = rd_val_64b;
RETIRE_SUCCESS
}
}
Expand Down Expand Up @@ -147,8 +147,8 @@ mapping clause encdec =
/* Execution semantics ================================ */

function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
let rs1_val_64b = F_or_X_D(rs1);
let rs2_val_64b = F_or_X_D(rs2);
let rs1_val_64b = F_or_X(64, rs1);
let rs2_val_64b = F_or_X(64, rs2);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
Expand All @@ -160,7 +160,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
FDIV_D => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b)
};
accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_64b;
F_or_X(rd) = rd_val_64b;
RETIRE_SUCCESS
}
}
Expand Down Expand Up @@ -240,22 +240,22 @@ mapping clause encdec =
/* Execution semantics ================================ */

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
let rm_3b = encdec_rounding_mode(rm');
let (fflags, rd_val_D) = riscv_f64Sqrt (rm_3b, rs1_val_D);

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
}

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
Expand All @@ -270,7 +270,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
}

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
Expand All @@ -293,7 +293,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = {
let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W);

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
Expand All @@ -308,45 +308,45 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = {
let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU);

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
}

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
let rm_3b = encdec_rounding_mode(rm');
let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D);

accrue_fflags(fflags);
F_or_X_S(rd) = rd_val_S;
F_or_X(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
}

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
let rs1_val_S = F_or_X_S(rs1);
let rs1_val_S = F_or_X(32, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
let rm_3b = encdec_rounding_mode(rm');
let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S);

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
}

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
assert(sizeof(xlen) >= 64);
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
Expand All @@ -362,7 +362,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {

function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
assert(sizeof(xlen) >= 64);
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
Expand All @@ -386,7 +386,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = {
let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L);

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
Expand All @@ -402,7 +402,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = {
let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU);

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
Expand Down Expand Up @@ -528,42 +528,42 @@ mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if hav
/* Execution semantics ================================ */

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);

let (s1, e1, m1) = fsplit (rs1_val_D);
let (s2, e2, m2) = fsplit (rs2_val_D);
let rd_val_D = fmake (s2, e1, m1);

F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);
let (s1, e1, m1) = fsplit (rs1_val_D);
let (s2, e2, m2) = fsplit (rs2_val_D);
let rd_val_D = fmake (0b1 ^ s2, e1, m1);

F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);
let (s1, e1, m1) = fsplit (rs1_val_D);
let (s2, e2, m2) = fsplit (rs2_val_D);
let rd_val_D = fmake (s1 ^ s2, e1, m1);

F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);

let is_quiet = true;
let (rs1_lt_rs2, fflags) = fle(rs1_val_D, rs2_val_D, is_quiet);
Expand All @@ -577,13 +577,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
else /* (not rs1_lt_rs2) */ rs2_val_D;

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}

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 rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);

let is_quiet = true;
let (rs2_lt_rs1, fflags) = fle(rs2_val_D, rs1_val_D, is_quiet);
Expand All @@ -597,13 +597,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
else /* (not rs2_lt_rs1) */ rs2_val_D;

accrue_fflags(fflags);
F_or_X_D(rd) = rd_val_D;
F_or_X(rd) = rd_val_D;
RETIRE_SUCCESS
}

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);

let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Eq (rs1_val_D, rs2_val_D);
Expand All @@ -614,8 +614,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
}

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);

let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Lt (rs1_val_D, rs2_val_D);
Expand All @@ -626,8 +626,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
}

function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let rs1_val_D = F_or_X(64, rs1);
let rs2_val_D = F_or_X(64, rs2);

let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Le (rs1_val_D, rs2_val_D);
Expand Down Expand Up @@ -719,7 +719,7 @@ mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if
/* Execution semantics ================================ */

function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs1_val_D = F_or_X(64, rs1);

let rd_val_10b : bits (10) =
if f_is_neg_inf (rs1_val_D) then 0b_00_0000_0001
Expand Down
Loading

0 comments on commit cf7553b

Please sign in to comment.