From 71cb5e6d66d480f736497a99faa41f11deac9e07 Mon Sep 17 00:00:00 2001 From: XinlaiWan Date: Tue, 29 Aug 2023 20:33:53 +0800 Subject: [PATCH] Fix NaN boxing issue and add notes for RVV configuration TODOs --- .gitignore | 3 --- model/riscv_fdext_regs.sail | 10 ++-------- model/riscv_insts_vext_fp.sail | 6 +++++- model/riscv_insts_vext_utils.sail | 30 +++++------------------------- model/riscv_insts_vext_vset.sail | 19 +++++++++++++++++-- model/riscv_sys_control.sail | 10 +++++++++- model/riscv_sys_regs.sail | 1 - model/riscv_vlen.sail | 4 ++++ 8 files changed, 42 insertions(+), 41 deletions(-) diff --git a/.gitignore b/.gitignore index 7442c9d3f..224b1595b 100644 --- a/.gitignore +++ b/.gitignore @@ -6,6 +6,3 @@ _build/ _sbuild/ *.o *.a -c_emulator/riscv_sim_* -ocaml_emulator/riscv_ocaml_sim_* -z3_problems diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 465514ab9..f2e0fb33c 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -536,12 +536,8 @@ function ext_write_fcsr (frm, fflags) = { val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape} function write_fflags(fflags) = { if fcsr.FFLAGS() != fflags - then { - fcsr->FFLAGS() = fflags; - dirty_fd_context_if_present(); - if get_config_print_reg() - then print("fcsr.FFLAGS <- " ^ BitStr(fflags)) - } + then dirty_fd_context_if_present(); + fcsr->FFLAGS() = fflags; } /* called for non-softfloat paths (softfloat flags need updating) */ @@ -553,7 +549,5 @@ function accrue_fflags(flags) = { fcsr->FFLAGS() = f; update_softfloat_fflags(f); dirty_fd_context_if_present(); - if get_config_print_reg() - then print("fcsr.FFLAGS <- " ^ BitStr(flags)) } } diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 7b1251c00..fbf85afd4 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -861,7 +861,11 @@ function clause execute(VFMVFS(vs2, rd)) = { let 'm = SEW; let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); - F(rd) = nan_box_vector(vs2_val[0]); + match 'm { + 16 => F_H(rd) = vs2_val[0], + 32 => F_S(rd) = vs2_val[0], + 64 => F_D(rd) = vs2_val[0] + }; vstart = zeros(); RETIRE_SUCCESS diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index d832c6cc0..1148ea78e 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -478,25 +478,6 @@ function canonical_NaN('m) = { } } -/* Floating point NaN boxing / unboxing that support 16-bit to 64-bit types */ -val nan_box_vector : forall 'm, ('m in {16, 32, 64} & 'm <= flen). bits('m) -> flenbits -function nan_box_vector(unboxed) = { - match 'm { - 16 => nan_box(unboxed), - 32 => nan_box(unboxed), - 64 => unboxed - } -} - -val nan_unbox_vector : forall 'm, ('m in {16, 32, 64} & 'm <= flen). (flenbits, int('m)) -> bits('m) -function nan_unbox_vector(regval, 'm) = { - match 'm { - 16 => nan_unbox(regval), - 32 => nan_unbox(regval), - 64 => regval - } -} - /* 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) = { @@ -600,12 +581,11 @@ function f_is_NaN(xf) = { /* Scalar register shaping for floating point operations */ val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) effect {escape, rreg} function get_scalar_fp(rs1, SEW) = { - if sizeof(flen) >= SEW then { - /* Least significant SEW bits */ - nan_unbox_vector(F(rs1), SEW) - } else { - assert(false, "invalid vector floating-point type width: FLEN < SEW"); - zeros() + assert(sizeof(flen) >= SEW, "invalid vector floating-point type width: FLEN < SEW"); + match SEW { + 16 => F_H(rs1), + 32 => F_S(rs1), + 64 => F_D(rs1) } } diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 7ad2fbdd6..e869c6e90 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -104,6 +104,9 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { let LMUL_pow_new = get_lmul_pow(); let SEW_pow_new = get_sew_pow(); if SEW_pow_new > LMUL_pow_new + ELEN_pow then { + /* Note: Implementations can set vill or trap if the vtype setting is not supported. + * TODO: configuration support for both solutions + */ vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); @@ -117,8 +120,11 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { let rs1_val = X(rs1); let AVL = unsigned(rs1_val); vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) /* ceil(AVL / 2) ≤ vl ≤ VLMAX */ + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) else to_bits(sizeof(xlen), VLMAX); + /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX) + * TODO: configuration support for either using ceil(AVL / 2) or VLMAX + */ X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); @@ -128,6 +134,9 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { let AVL = unsigned(vl); let ratio_pow_new = SEW_pow_new - LMUL_pow_new; if (ratio_pow_new != ratio_pow_ori) then { + /* Note: Implementations can set vill or trap if the vtype setting is not supported. + * TODO: configuration support for both solutions + */ vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); } @@ -170,6 +179,9 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { let LMUL_pow_new = get_lmul_pow(); let SEW_pow_new = get_sew_pow(); if SEW_pow_new > LMUL_pow_new + ELEN_pow then { + /* Note: Implementations can set vill or trap if the vtype setting is not supported. + * TODO: configuration support for both solutions + */ vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); @@ -181,8 +193,11 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { /* set vl according to VLMAX and AVL */ vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) /* ceil(AVL / 2) ≤ vl ≤ VLMAX */ + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) else to_bits(sizeof(xlen), VLMAX); + /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX) + * TODO: configuration support for either using ceil(AVL / 2) or VLMAX + */ X(rd) = vl; print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); print_reg("CSR vl <- " ^ BitStr(vl)); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 789b9822f..47c20160b 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -600,6 +600,15 @@ function init_sys() -> unit = { minstret_increment = true; /* initialize vector csrs */ + elen = 0b1; /* ELEN=64 as default value */ + /* vlen = ...; + * VLEN needs to be manually speficied currently. + * See riscv_vlen.sail for details. + */ + vlenb = zero_extend(0b0); + /* The value of vlenb is not used currently. + * It should be assigned as 2 ^ (get_vlen_pow() - 3) after vlen is speficied. + */ vstart = zero_extend(0b0); vxsat = 0b0; vxrm = 0b00; @@ -612,7 +621,6 @@ function init_sys() -> unit = { vtype->vta() = 0b0; vtype->vsew() = 0b000; vtype->vlmul() = 0b000; - vlenb = zero_extend(0b0); init_pmp(); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 2fecd5bc7..6307e727c 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -211,7 +211,6 @@ function haveZknd() -> bool = true function haveZmmul() -> bool = true function haveRVV() -> bool = misa.V() == 0b1 -/* see below for F and D extension tests */ /* Zicond extension support */ function haveZicond() -> bool = true diff --git a/model/riscv_vlen.sail b/model/riscv_vlen.sail index 55f18eac5..c123048d8 100644 --- a/model/riscv_vlen.sail +++ b/model/riscv_vlen.sail @@ -44,6 +44,10 @@ function get_elen_pow() = match elen { 0b0 => 5, 0b1 => 6 } +/* Note: ELEN=32 requires a different encoding of the CSR vtype. + * The current version of vtype implementation corresponds to the ELEN=64 configuration. + * TODO: the configurarion of ELEN and its corresponding vtype implementations. + */ register vlen : bits(4)