Skip to content

Commit

Permalink
Use separate newtypes for floating registers
Browse files Browse the repository at this point in the history 
This required splitting many of the AST constructors.
  • Loading branch information
@nwf
nwf committed Dec 13, 2024
1 parent b96a5b5 commit 000a17c
Show file tree
Hide file tree
Showing 11 changed files with 586 additions and 757 deletions.
100 changes: 64 additions & 36 deletions model/riscv_fdext_regs.sail
View file
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 (regno(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 (regno(r) : regno) -> flenbits = {
fregval_from_freg(v)
}

function wF (regno(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 (regno(r) : regno, in_v : flenbits) -> unit = {
print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
}

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

function wF_bits(i: regidx, data: flenbits) -> unit = {
wF(regidx_to_regno(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((let regidx(i_bits) = i in i_bits)[0] == bitzero);
if i == zreg then zeros() else X(regidx_offset(i, 0b00001)) @ 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 ((let regidx(i_bits) = i in i_bits)[0] == bitzero);
if i != zreg then {
X(i) = data[31..0];
X(regidx_offset(i, 0b00001)) = 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 Down Expand Up @@ -346,13 +364,23 @@ mapping freg_name_raw : bits(5) <-> string = {
0b11111 <-> "ft11"
}

mapping freg_name : regidx <-> string = { regidx(i) <-> freg_name_raw(i) }

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
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}
Loading

0 comments on commit 000a17c

Please sign in to comment.