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

Use newtypes for register indices and numbers #617

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Use newtypes for register indices and numbers #617

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
087f33f
Use newtypes for regidx and regno
nwf Nov 15, 2024
b96a5b5
Use separate newtypes for vector registers
nwf Nov 16, 2024
000a17c
Use separate newtypes for floating registers
nwf Nov 15, 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
101 changes: 65 additions & 36 deletions model/riscv_fdext_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,22 @@ function nan_unbox(m, x) = if 'n == 'm then x else (
/* **************************************************************** */
/* Floating point register file */

newtype fregidx = fregidx : bits(5)
newtype fregno = fregno : range(0, 31)
function fregidx_to_fregno (fregidx(b) : fregidx) -> fregno = fregno(unsigned(b))
function fregidx_offset(fregidx(r) : fregidx, o : bits(5)) -> fregidx = fregidx(r + o)

function cregidx_to_fregidx (cregidx(b) : cregidx) -> fregidx = fregidx(0b01 @ b)

/*
* TODO: This is not quite right for having both Zfinx and E, but at least it
* marks the places we need to consider it
*/
function fregidx_to_regidx (fregidx(b) : fregidx) -> regidx =
regidx(truncate(b, let regidx(zreg_bits) = zreg in length(zreg_bits)))

mapping encdec_freg : fregidx <-> bits(5) = { fregidx(r) <-> r }

register f0 : fregtype
register f1 : fregtype
register f2 : fregtype
Expand Down Expand Up @@ -96,7 +112,7 @@ function dirty_fd_context_if_present() -> unit = {
if sys_enable_fdext() then dirty_fd_context()
}

function rF (r : regno) -> flenbits = {
function rF (fregno(r) : fregno) -> flenbits = {
assert(sys_enable_fdext());
let v : fregtype =
match r {
Expand Down Expand Up @@ -137,7 +153,7 @@ function rF (r : regno) -> flenbits = {
fregval_from_freg(v)
}

function wF (r : regno, in_v : flenbits) -> unit = {
function wF (fregno(r) : fregno, in_v : flenbits) -> unit = {
assert(sys_enable_fdext());
let v = fregval_into_freg(in_v);
match r {
Expand Down Expand Up @@ -184,50 +200,50 @@ function wF (r : regno, in_v : flenbits) -> unit = {
print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
}

function rF_bits(i: regidx) -> flenbits = rF(unsigned(i))
function rF_bits(i: fregidx) -> flenbits = rF(fregidx_to_fregno(i))

function wF_bits(i: regidx, data: flenbits) -> unit = {
wF(unsigned(i)) = data
function wF_bits(i: fregidx, data: flenbits) -> unit = {
wF(fregidx_to_fregno(i)) = data
}

overload F = {rF_bits, wF_bits, rF, wF}

val rF_H : regidx -> bits(16)
val rF_H : fregidx -> bits(16)
function rF_H(i) = {
assert(flen >= 16);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
nan_unbox(F(i))
}

val wF_H : (regidx, bits(16)) -> unit
val wF_H : (fregidx, bits(16)) -> unit
function wF_H(i, data) = {
assert(flen >= 16);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = nan_box(data)
}

val rF_S : regidx -> bits(32)
val rF_S : fregidx -> bits(32)
function rF_S(i) = {
assert(flen >= 32);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
nan_unbox(F(i))
}

val wF_S : (regidx, bits(32)) -> unit
val wF_S : (fregidx, bits(32)) -> unit
function wF_S(i, data) = {
assert(flen >= 32);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i) = nan_box(data)
}

val rF_D : regidx -> bits(64)
val rF_D : fregidx -> bits(64)
function rF_D(i) = {
assert(flen >= 64);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
F(i)
}

val wF_D : (regidx, bits(64)) -> unit
val wF_D : (fregidx, bits(64)) -> unit
function wF_D(i, data) = {
assert(flen >= 64);
assert(sys_enable_fdext() & not(sys_enable_zfinx()));
Expand All @@ -238,69 +254,71 @@ overload F_H = { rF_H, wF_H }
overload F_S = { rF_S, wF_S }
overload F_D = { rF_D, wF_D }

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

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

val rF_or_X_D : regidx -> bits(64)
val rF_or_X_D : fregidx -> bits(64)
function rF_or_X_D(i) = {
assert(flen >= 64);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_D(i)
else if xlen >= 64
then X(i)[63..0]
then X(fregidx_to_regidx(i))[63..0]
else {
assert(i[0] == bitzero);
if i == zeros() then zeros() else X(i + 1) @ X(i)
let ridx = fregidx_to_regidx(i);
assert((let regidx(i_bits) = ridx in i_bits)[0] == bitzero);
if ridx == zreg then zeros() else X(regidx_offset(ridx, 0b00001)) @ X(ridx)
}
}

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

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

val wF_or_X_D : (regidx, bits(64)) -> unit
val wF_or_X_D : (fregidx, bits(64)) -> unit
function wF_or_X_D(i, data) = {
assert (flen >= 64);
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_D(i) = data
else if xlen >= 64
then X(i) = sign_extend(data)
then X(fregidx_to_regidx(i)) = sign_extend(data)
else {
assert (i[0] == bitzero);
if i != zeros() then {
X(i) = data[31..0];
X(i + 1) = data[63..32];
let ridx = fregidx_to_regidx(i);
assert ((let regidx(i_bits) = ridx in i_bits)[0] == bitzero);
if ridx != zreg then {
X(ridx) = data[31..0];
X(regidx_offset(ridx, 0b00001)) = data[63..32];
}
}
}
Expand All @@ -311,8 +329,7 @@ overload F_or_X_D = { rF_or_X_D, wF_or_X_D }

/* mappings for assembly */

val freg_name : regidx <-> string
mapping freg_name = {
mapping freg_name_raw : bits(5) <-> string = {
0b00000 <-> "ft0",
0b00001 <-> "ft1",
0b00010 <-> "ft2",
Expand Down Expand Up @@ -347,11 +364,23 @@ mapping freg_name = {
0b11111 <-> "ft11"
}

val freg_or_reg_name : regidx <-> string
mapping freg_or_reg_name = {
reg if sys_enable_fdext() <-> freg_name(reg) if sys_enable_fdext(),
reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx()
}
mapping freg_name : fregidx <-> string = { fregidx(i) <-> freg_name_raw(i) }

val freg_or_reg_name : fregidx <-> string
function freg_or_reg_name_forwards_matches(_ : fregidx) -> bool = true
function freg_or_reg_name_forwards(f : fregidx) -> string =
if sys_enable_fdext() then freg_name(f)
else if sys_enable_zfinx() then reg_name(fregidx_to_regidx(f))
else ""
function freg_or_reg_name_backwards_matches(s : string) -> bool =
if sys_enable_fdext() then freg_name_backwards_matches(s)
else if sys_enable_zfinx() then reg_name_backwards_matches(s)
else false
function freg_or_reg_name_backwards(s : string) -> fregidx =
if sys_enable_fdext() then freg_name_backwards(s)
else if sys_enable_zfinx() then
let regidx(i) = reg_name_backwards(s) in fregidx(zero_extend(i))
else { assert(false, "Bad register name"); fregidx(0b00000) }

val init_fdext_regs : unit -> unit
function init_fdext_regs () = {
Expand Down
55 changes: 40 additions & 15 deletions model/riscv_freg_type.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,36 +37,61 @@ enum f_madd_op_H = {FMADD_H, FMSUB_H, FNMSUB_H, FNMADD_H}

enum f_bin_rm_op_H = {FADD_H, FSUB_H, FMUL_H, FDIV_H}

enum f_un_rm_op_H = {FSQRT_H, FCVT_W_H, FCVT_WU_H, FCVT_H_W, FCVT_H_WU, // RV32 and RV64
FCVT_H_S, FCVT_H_D, FCVT_S_H, FCVT_D_H,
FCVT_L_H, FCVT_LU_H, FCVT_H_L, FCVT_H_LU} // RV64 only
enum f_un_rm_ff_op_H = {FSQRT_H, FCVT_H_S, FCVT_H_D, FCVT_S_H, FCVT_D_H}

enum f_un_op_H = {FCLASS_H, FMV_X_H, FMV_H_X} /* RV32 and RV64 */
enum f_un_rm_fx_op_H = { FCVT_W_H, FCVT_WU_H, // RV32 and RV64
FCVT_L_H, FCVT_LU_H} // RV64 only

enum f_bin_op_H = {FSGNJ_H, FSGNJN_H, FSGNJX_H, FMIN_H, FMAX_H, FEQ_H, FLT_H, FLE_H}
enum f_un_rm_xf_op_H = { FCVT_H_W, FCVT_H_WU, // RV32 and RV64
FCVT_H_L, FCVT_H_LU} // RV64 only

enum f_un_x_op_H = {FCLASS_H, FMV_X_H}

enum f_un_f_op_H = {FMV_H_X}

enum f_bin_f_op_H = {FSGNJ_H, FSGNJN_H, FSGNJX_H, FMIN_H, FMAX_H}

enum f_bin_x_op_H = {FEQ_H, FLT_H, FLE_H}

enum rounding_mode = {RM_RNE, RM_RTZ, RM_RDN, RM_RUP, RM_RMM, RM_DYN}

enum f_madd_op_S = {FMADD_S, FMSUB_S, FNMSUB_S, FNMADD_S}

enum f_bin_rm_op_S = {FADD_S, FSUB_S, FMUL_S, FDIV_S}

enum f_un_rm_op_S = {FSQRT_S, FCVT_W_S, FCVT_WU_S, FCVT_S_W, FCVT_S_WU, // RV32 and RV64
FCVT_L_S, FCVT_LU_S, FCVT_S_L, FCVT_S_LU} // RV64 only
enum f_un_rm_ff_op_S = {FSQRT_S}

enum f_un_rm_fx_op_S = { FCVT_W_S, FCVT_WU_S, // RV32 and RV64
FCVT_L_S, FCVT_LU_S } // RV64 only

enum f_un_rm_xf_op_S = { FCVT_S_W, FCVT_S_WU, // RV32 and RV64
FCVT_S_L, FCVT_S_LU } // RV64 only

enum f_un_op_S = {FCLASS_S, FMV_X_W, FMV_W_X} /* RV32 and RV64 */
enum f_un_op_f_S = {FMV_W_X} /* RV32 and RV64 */

enum f_bin_op_S = {FSGNJ_S, FSGNJN_S, FSGNJX_S, FMIN_S, FMAX_S, FEQ_S, FLT_S, FLE_S}
enum f_un_op_x_S = {FCLASS_S, FMV_X_W} /* RV32 and RV64 */

enum f_bin_op_f_S = {FSGNJ_S, FSGNJN_S, FSGNJX_S, FMIN_S, FMAX_S}

enum f_bin_op_x_S = {FEQ_S, FLT_S, FLE_S}

enum f_madd_op_D = {FMADD_D, FMSUB_D, FNMSUB_D, FNMADD_D}

enum f_bin_rm_op_D = {FADD_D, FSUB_D, FMUL_D, FDIV_D}

enum f_un_rm_op_D = {FSQRT_D, FCVT_W_D, FCVT_WU_D, FCVT_D_W, FCVT_D_WU, // RV32 and RV64
FCVT_S_D, FCVT_D_S,
FCVT_L_D, FCVT_LU_D, FCVT_D_L, FCVT_D_LU} // RV64 only
enum f_un_rm_ff_op_D = {FSQRT_D, FCVT_S_D, FCVT_D_S}

enum f_un_rm_fx_op_D = {FCVT_W_D, FCVT_WU_D, // RV32 and RV64
FCVT_L_D, FCVT_LU_D} // RV64 only

enum f_un_rm_xf_op_D = {FCVT_D_W, FCVT_D_WU, // RV32 and RV64
FCVT_D_L, FCVT_D_LU} // RV64 only

enum f_bin_f_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D}

enum f_bin_x_op_D = {FEQ_D, FLT_D, FLE_D}

enum f_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FLE_D}
enum f_un_x_op_D = {FCLASS_D, /* RV32 and RV64 */
FMV_X_D} /* RV64 only */

enum f_un_op_D = {FCLASS_D, /* RV32 and RV64 */
FMV_X_D, FMV_D_X} /* RV64 only */
enum f_un_f_op_D = {FMV_D_X}
12 changes: 6 additions & 6 deletions model/riscv_insts_aext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ function clause extensionEnabled(Ext_Zalrsc) = misa[A] == 0b1

union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)

mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ encdec_reg(rs1) @ 0b0 @ size_enc(size) @ encdec_reg(rd) @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)

/* We could set load-reservations on physical or virtual addresses.
* However most chips (especially multi-core) will use physical addresses.
Expand Down Expand Up @@ -106,8 +106,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
/* ****************************************************************** */
union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)

mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ encdec_reg(rs2) @ encdec_reg(rs1) @ 0b0 @ size_enc(size) @ encdec_reg(rd) @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)

/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
Expand Down Expand Up @@ -185,8 +185,8 @@ mapping encdec_amoop : amoop <-> bits(5) = {
AMOMAXU <-> 0b11100
}

mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zaamo) & amo_width_valid(size)
<-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zaamo) & amo_width_valid(size)
mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zaamo) & amo_width_valid(size)
<-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ encdec_reg(rs2) @ encdec_reg(rs1) @ 0b0 @ size_enc(size) @ encdec_reg(rd) @ 0b0101111 if extensionEnabled(Ext_Zaamo) & amo_width_valid(size)

/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
Expand Down
Loading
Loading