diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rwxr-xr-x | model/riscv_insts_vext_fp_red.sail | 127 | ||||
| -rwxr-xr-x | model/riscv_insts_vext_fp_utils.sail | 663 | ||||
| -rwxr-xr-x | model/riscv_insts_vext_fp_vm.sail | 142 | ||||
| -rwxr-xr-x | model/riscv_insts_vext_red.sail | 115 | ||||
| -rwxr-xr-x | model/riscv_insts_vext_utils.sail | 660 | ||||
| -rwxr-xr-x | model/riscv_insts_vext_vm.sail | 132 |
7 files changed, 940 insertions, 902 deletions
@@ -50,13 +50,16 @@ SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail +SAIL_DEFAULT_INST += riscv_insts_vext_fp_utils.sail SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail SAIL_DEFAULT_INST += riscv_insts_vext_arith.sail SAIL_DEFAULT_INST += riscv_insts_vext_fp.sail SAIL_DEFAULT_INST += riscv_insts_vext_mem.sail SAIL_DEFAULT_INST += riscv_insts_vext_mask.sail SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail +SAIL_DEFAULT_INST += riscv_insts_vext_fp_vm.sail SAIL_DEFAULT_INST += riscv_insts_vext_red.sail +SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail diff --git a/model/riscv_insts_vext_fp_red.sail b/model/riscv_insts_vext_fp_red.sail new file mode 100755 index 0000000..9d4220d --- /dev/null +++ b/model/riscv_insts_vext_fp_red.sail @@ -0,0 +1,127 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* ******************************************************************************* */ +/* This file implements part of the vector extension. */ +/* Chapter 14: Vector Reduction Instructions */ +/* ******************************************************************************* */ + +/* ********************** OPFVV (Floating-Point Reduction) *********************** */ +union clause ast = RFVVTYPE : (rfvvfunct6, bits(1), regidx, regidx, regidx) + +mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = { + FVV_VFREDOSUM <-> 0b000011, + FVV_VFREDUSUM <-> 0b000001, + FVV_VFREDMAX <-> 0b000111, + FVV_VFREDMIN <-> 0b000101, + FVV_VFWREDOSUM <-> 0b110011, + FVV_VFWREDUSUM <-> 0b110001 +} + +mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) + +val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired +function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { + let rm_3b = fcsr[FRM]; + let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ + + if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + assert(SEW != 8); + + if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ + + let 'n = num_elem_vs; + let 'd = num_elem_vd; + let 'm = SEW; + + let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vd_val : vector('d, dec, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); + let mask : vector('n, dec, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + + sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ + foreach (i from 0 to (num_elem_vs - 1)) { + if mask[i] then { + sum = match funct6 { + /* currently ordered/unordered sum reductions do the same operations */ + FVV_VFREDOSUM => fp_add(rm_3b, sum, vs2_val[i]), + FVV_VFREDUSUM => fp_add(rm_3b, sum, vs2_val[i]), + FVV_VFREDMAX => fp_max(sum, vs2_val[i]), + FVV_VFREDMIN => fp_min(sum, vs2_val[i]), + _ => internal_error(__FILE__, __LINE__, "Widening op unexpected") + } + } + }; + + write_single_element(SEW, 0, vd, sum); + /* other elements in vd are treated as tail elements, currently remain unchanged */ + /* TODO: configuration support for agnostic behavior */ + vstart = zeros(); + RETIRE_SUCCESS +} + +val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired +function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { + let rm_3b = fcsr[FRM]; + let SEW_widen = SEW * 2; + let LMUL_pow_widen = LMUL_pow + 1; + let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ + + if illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; + assert(SEW >= 16 & SEW_widen <= 64); + + if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ + + let 'n = num_elem_vs; + let 'd = num_elem_vd; + let 'm = SEW; + let 'o = SEW_widen; + + let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vd_val : vector('d, dec, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); + let mask : vector('n, dec, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + + sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */ + foreach (i from 0 to (num_elem_vs - 1)) { + if mask[i] then { + /* currently ordered/unordered sum reductions do the same operations */ + sum = fp_add(rm_3b, sum, fp_widen(vs2_val[i])) + } + }; + + write_single_element(SEW_widen, 0, vd, sum); + /* other elements in vd are treated as tail elements, currently remain unchanged */ + /* TODO: configuration support for agnostic behavior */ + vstart = zeros(); + RETIRE_SUCCESS +} + +function clause execute(RFVVTYPE(funct6, vm, vs2, vs1, vd)) = { + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem_vs = get_num_elem(LMUL_pow, SEW); + + if funct6 == FVV_VFWREDOSUM | funct6 == FVV_VFWREDUSUM then + process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) + else + process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) +} + +mapping rfvvtype_mnemonic : rfvvfunct6 <-> string = { + FVV_VFREDOSUM <-> "vfredosum.vs", + FVV_VFREDUSUM <-> "vfredusum.vs", + FVV_VFREDMAX <-> "vfredmax.vs", + FVV_VFREDMIN <-> "vfredmin.vs", + FVV_VFWREDOSUM <-> "vfwredosum.vs", + FVV_VFWREDUSUM <-> "vfwredusum.vs" +} + +mapping clause assembly = RFVVTYPE(funct6, vm, vs2, vs1, vd) + <-> rfvvtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm) diff --git a/model/riscv_insts_vext_fp_utils.sail b/model/riscv_insts_vext_fp_utils.sail new file mode 100755 index 0000000..2abbe5f --- /dev/null +++ b/model/riscv_insts_vext_fp_utils.sail @@ -0,0 +1,663 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* ******************************************************************************* */ +/* This file implements functions used by vector instructions. */ +/* ******************************************************************************* */ + +/* Check for valid floating-point operation types + * 1. Valid element width of floating-point numbers + * 2. Valid floating-point rounding mode + */ +val valid_fp_op : ({8, 16, 32, 64}, bits(3)) -> bool +function valid_fp_op(SEW, rm_3b) = { + /* 128-bit floating-point values will be supported in future extensions */ + let valid_sew = (SEW >= 16 & SEW <= 128); + let valid_rm = not(rm_3b == 0b101 | rm_3b == 0b110 | rm_3b == 0b111); + valid_sew & valid_rm +} + +/* a. Normal check for floating-point instructions */ +val illegal_fp_normal : (regidx, bits(1), {8, 16, 32, 64}, bits(3)) -> bool +function illegal_fp_normal(vd, vm, SEW, rm_3b) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) +} + +/* b. Masked check for floating-point instructions encoded with vm = 0 */ +val illegal_fp_vd_masked : (regidx, {8, 16, 32, 64}, bits(3)) -> bool +function illegal_fp_vd_masked(vd, SEW, rm_3b) = { + not(valid_vtype()) | vd == 0b00000 | not(valid_fp_op(SEW, rm_3b)) +} + +/* c. Unmasked check for floating-point instructions encoded with vm = 1 */ +val illegal_fp_vd_unmasked : ({8, 16, 32, 64}, bits(3)) -> bool +function illegal_fp_vd_unmasked(SEW, rm_3b) = { + not(valid_vtype()) | not(valid_fp_op(SEW, rm_3b)) +} + +/* d. Variable width check for floating-point widening/narrowing instructions */ +val illegal_fp_variable_width : (regidx, bits(1), {8, 16, 32, 64}, bits(3), int, int) -> bool +function illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_new, LMUL_pow_new) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | + not(valid_eew_emul(SEW_new, LMUL_pow_new)) +} + +/* e. Normal check for floating-point reduction instructions */ +val illegal_fp_reduction : ({8, 16, 32, 64}, bits(3)) -> bool +function illegal_fp_reduction(SEW, rm_3b) = { + not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) +} + +/* f. Variable width check for floating-point widening reduction instructions */ +val illegal_fp_reduction_widen : ({8, 16, 32, 64}, bits(3), int, int) -> bool +function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = { + not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) | + not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) +} + +/* Floating point canonical NaN for 16-bit, 32-bit and 64-bit types */ +val canonical_NaN : forall 'm, 'm in {16, 32, 64}. int('m) -> bits('m) +function canonical_NaN('m) = { + match 'm { + 16 => canonical_NaN_H(), + 32 => canonical_NaN_S(), + 64 => canonical_NaN_D() + } +} + +/* 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) = { + match 'm { + 16 => f_is_neg_inf_H(xf), + 32 => f_is_neg_inf_S(xf), + 64 => f_is_neg_inf_D(xf) + } +} + +val f_is_neg_norm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_neg_norm(xf) = { + match 'm { + 16 => f_is_neg_norm_H(xf), + 32 => f_is_neg_norm_S(xf), + 64 => f_is_neg_norm_D(xf) + } +} + +val f_is_neg_subnorm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_neg_subnorm(xf) = { + match 'm { + 16 => f_is_neg_subnorm_H(xf), + 32 => f_is_neg_subnorm_S(xf), + 64 => f_is_neg_subnorm_D(xf) + } +} + +val f_is_neg_zero : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_neg_zero(xf) = { + match 'm { + 16 => f_is_neg_zero_H(xf), + 32 => f_is_neg_zero_S(xf), + 64 => f_is_neg_zero_D(xf) + } +} + +val f_is_pos_zero : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_pos_zero(xf) = { + match 'm { + 16 => f_is_pos_zero_H(xf), + 32 => f_is_pos_zero_S(xf), + 64 => f_is_pos_zero_D(xf) + } +} + +val f_is_pos_subnorm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_pos_subnorm(xf) = { + match 'm { + 16 => f_is_pos_subnorm_H(xf), + 32 => f_is_pos_subnorm_S(xf), + 64 => f_is_pos_subnorm_D(xf) + } +} + +val f_is_pos_norm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_pos_norm(xf) = { + match 'm { + 16 => f_is_pos_norm_H(xf), + 32 => f_is_pos_norm_S(xf), + 64 => f_is_pos_norm_D(xf) + } +} + +val f_is_pos_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_pos_inf(xf) = { + match 'm { + 16 => f_is_pos_inf_H(xf), + 32 => f_is_pos_inf_S(xf), + 64 => f_is_pos_inf_D(xf) + } +} + +val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_SNaN(xf) = { + match 'm { + 16 => f_is_SNaN_H(xf), + 32 => f_is_SNaN_S(xf), + 64 => f_is_SNaN_D(xf) + } +} + +val f_is_QNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_QNaN(xf) = { + match 'm { + 16 => f_is_QNaN_H(xf), + 32 => f_is_QNaN_S(xf), + 64 => f_is_QNaN_D(xf) + } +} + +val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool +function f_is_NaN(xf) = { + match 'm { + 16 => f_is_NaN_H(xf), + 32 => f_is_NaN_S(xf), + 64 => f_is_NaN_D(xf) + } +} + +/* Scalar register shaping for floating point operations */ +val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) +function get_scalar_fp(rs1, SEW) = { + 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) + } +} + +/* Get the floating point rounding mode from csr fcsr */ +val get_fp_rounding_mode : unit -> rounding_mode +function get_fp_rounding_mode() = encdec_rounding_mode(fcsr[FRM]) + +/* Negate a floating point number */ +val negate_fp : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m) +function negate_fp(xf) = { + match 'm { + 16 => negate_H(xf), + 32 => negate_S(xf), + 64 => negate_D(xf) + } +} + +/* Floating point functions using softfloat interface */ +val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) +function fp_add(rm_3b, op1, op2) = { + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16Add(rm_3b, op1, op2), + 32 => riscv_f32Add(rm_3b, op1, op2), + 64 => riscv_f64Add(rm_3b, op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_sub: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) +function fp_sub(rm_3b, op1, op2) = { + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16Sub(rm_3b, op1, op2), + 32 => riscv_f32Sub(rm_3b, op1, op2), + 64 => riscv_f64Sub(rm_3b, op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_min : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) +function fp_min(op1, op2) = { + let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Lt_quiet(op1, op2), + 32 => riscv_f32Lt_quiet(op1, op2), + 64 => riscv_f64Lt_quiet(op1, op2) + }; + + let result_val = if (f_is_NaN(op1) & f_is_NaN(op2)) then canonical_NaN('m) + else if f_is_NaN(op1) then op2 + else if f_is_NaN(op2) then op1 + else if (f_is_neg_zero(op1) & f_is_pos_zero(op2)) then op1 + else if (f_is_neg_zero(op2) & f_is_pos_zero(op1)) then op2 + else if op1_lt_op2 then op1 + else op2; + accrue_fflags(fflags); + result_val +} + +val fp_max : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) +function fp_max(op1, op2) = { + let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Lt_quiet(op1, op2), + 32 => riscv_f32Lt_quiet(op1, op2), + 64 => riscv_f64Lt_quiet(op1, op2) + }; + + let result_val = if (f_is_NaN(op1) & f_is_NaN(op2)) then canonical_NaN('m) + else if f_is_NaN(op1) then op2 + else if f_is_NaN(op2) then op1 + else if (f_is_neg_zero(op1) & f_is_pos_zero(op2)) then op2 + else if (f_is_neg_zero(op2) & f_is_pos_zero(op1)) then op1 + else if op1_lt_op2 then op2 + else op1; + accrue_fflags(fflags); + result_val +} + +val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function fp_eq(op1, op2) = { + let (fflags, result_val) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Eq(op1, op2), + 32 => riscv_f32Eq(op1, op2), + 64 => riscv_f64Eq(op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function fp_gt(op1, op2) = { + let (fflags, temp_val) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Le(op1, op2), + 32 => riscv_f32Le(op1, op2), + 64 => riscv_f64Le(op1, op2) + }; + let result_val = (if fflags == 0b10000 then false else not(temp_val)); + accrue_fflags(fflags); + result_val +} + +val fp_ge : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function fp_ge(op1, op2) = { + let (fflags, temp_val) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Lt(op1, op2), + 32 => riscv_f32Lt(op1, op2), + 64 => riscv_f64Lt(op1, op2) + }; + let result_val = (if fflags == 0b10000 then false else not(temp_val)); + accrue_fflags(fflags); + result_val +} + +val fp_lt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function fp_lt(op1, op2) = { + let (fflags, result_val) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Lt(op1, op2), + 32 => riscv_f32Lt(op1, op2), + 64 => riscv_f64Lt(op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_le : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool +function fp_le(op1, op2) = { + let (fflags, result_val) : (bits_fflags, bool) = match 'm { + 16 => riscv_f16Le(op1, op2), + 32 => riscv_f32Le(op1, op2), + 64 => riscv_f64Le(op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_mul : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) +function fp_mul(rm_3b, op1, op2) = { + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16Mul(rm_3b, op1, op2), + 32 => riscv_f32Mul(rm_3b, op1, op2), + 64 => riscv_f64Mul(rm_3b, op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_div : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) +function fp_div(rm_3b, op1, op2) = { + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16Div(rm_3b, op1, op2), + 32 => riscv_f32Div(rm_3b, op1, op2), + 64 => riscv_f64Div(rm_3b, op1, op2) + }; + accrue_fflags(fflags); + result_val +} + +val fp_muladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) +function fp_muladd(rm_3b, op1, op2, opadd) = { + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16MulAdd(rm_3b, op1, op2, opadd), + 32 => riscv_f32MulAdd(rm_3b, op1, op2, opadd), + 64 => riscv_f64MulAdd(rm_3b, op1, op2, opadd) + }; + accrue_fflags(fflags); + result_val +} + +val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) +function fp_nmuladd(rm_3b, op1, op2, opadd) = { + let op1 = negate_fp(op1); + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16MulAdd(rm_3b, op1, op2, opadd), + 32 => riscv_f32MulAdd(rm_3b, op1, op2, opadd), + 64 => riscv_f64MulAdd(rm_3b, op1, op2, opadd) + }; + accrue_fflags(fflags); + result_val +} + +val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) +function fp_mulsub(rm_3b, op1, op2, opsub) = { + let opsub = negate_fp(opsub); + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16MulAdd(rm_3b, op1, op2, opsub), + 32 => riscv_f32MulAdd(rm_3b, op1, op2, opsub), + 64 => riscv_f64MulAdd(rm_3b, op1, op2, opsub) + }; + accrue_fflags(fflags); + result_val +} + +val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) +function fp_nmulsub(rm_3b, op1, op2, opsub) = { + let opsub = negate_fp(opsub); + let op1 = negate_fp(op1); + let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { + 16 => riscv_f16MulAdd(rm_3b, op1, op2, opsub), + 32 => riscv_f32MulAdd(rm_3b, op1, op2, opsub), + 64 => riscv_f64MulAdd(rm_3b, op1, op2, opsub) + }; + accrue_fflags(fflags); + result_val +} + +val fp_class : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m) +function fp_class(xf) = { + let result_val_10b : bits(10) = + if f_is_neg_inf(xf) then 0b_00_0000_0001 + else if f_is_neg_norm(xf) then 0b_00_0000_0010 + else if f_is_neg_subnorm(xf) then 0b_00_0000_0100 + else if f_is_neg_zero(xf) then 0b_00_0000_1000 + else if f_is_pos_zero(xf) then 0b_00_0001_0000 + else if f_is_pos_subnorm(xf) then 0b_00_0010_0000 + else if f_is_pos_norm(xf) then 0b_00_0100_0000 + else if f_is_pos_inf(xf) then 0b_00_1000_0000 + else if f_is_SNaN(xf) then 0b_01_0000_0000 + else if f_is_QNaN(xf) then 0b_10_0000_0000 + else zeros(); + + zero_extend(result_val_10b) +} + +val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) +function fp_widen(nval) = { + let rm_3b = fcsr[FRM]; + let (fflags, wval) : (bits_fflags, bits('m * 2)) = match 'm { + 16 => riscv_f16ToF32(rm_3b, nval), + 32 => riscv_f32ToF64(rm_3b, nval) + }; + accrue_fflags(fflags); + wval +} + +/* Floating point functions without softfloat support */ +val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) +function riscv_f16ToI16 (rm, v) = { + let (_, sig32) = riscv_f16ToI32(rm, v); + if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) + else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag(), 0b1 @ zeros(15)) + else (zeros(5), sig32[15 .. 0]); +} + +val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) +function riscv_f16ToI8 (rm, v) = { + let (_, sig32) = riscv_f16ToI32(rm, v); + if signed(sig32) > signed(0b0 @ ones(7)) then (nvFlag(), 0b0 @ ones(7)) + else if signed(sig32) < signed(0b1 @ zeros(7)) then (nvFlag(), 0b1 @ zeros(7)) + else (zeros(5), sig32[7 .. 0]); +} + +val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) +function riscv_f32ToI16 (rm, v) = { + let (_, sig32) = riscv_f32ToI32(rm, v); + if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) + else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag(), 0b1 @ zeros(15)) + else (zeros(5), sig32[15 .. 0]); +} + +val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) +function riscv_f16ToUi16 (rm, v) = { + let (_, sig32) = riscv_f16ToUi32(rm, v); + if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) + else (zeros(5), sig32[15 .. 0]); +} + +val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) +function riscv_f16ToUi8 (rm, v) = { + let (_, sig32) = riscv_f16ToUi32(rm, v); + if unsigned(sig32) > unsigned(ones(8)) then (nvFlag(), ones(8)) + else (zeros(5), sig32[7 .. 0]); +} + +val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) +function riscv_f32ToUi16 (rm, v) = { + let (_, sig32) = riscv_f32ToUi32(rm, v); + if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) + else (zeros(5), sig32[15 .. 0]); +} + +val rsqrt7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bool) -> bits_D +function rsqrt7 (v, sub) = { + let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm { + 16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10), + 32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23), + 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) + }; + assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); + let table : vector(128, dec, int) = [ + 52, 51, 50, 48, 47, 46, 44, 43, + 42, 41, 40, 39, 38, 36, 35, 34, + 33, 32, 31, 30, 30, 29, 28, 27, + 26, 25, 24, 23, 23, 22, 21, 20, + 19, 19, 18, 17, 16, 16, 15, 14, + 14, 13, 12, 12, 11, 10, 10, 9, + 9, 8, 7, 7, 6, 6, 5, 4, + 4, 3, 3, 2, 2, 1, 1, 0, + 127, 125, 123, 121, 119, 118, 116, 114, + 113, 111, 109, 108, 106, 105, 103, 102, + 100, 99, 97, 96, 95, 93, 92, 91, + 90, 88, 87, 86, 85, 84, 83, 82, + 80, 79, 78, 77, 76, 75, 74, 73, + 72, 71, 70, 70, 69, 68, 67, 66, + 65, 64, 63, 63, 62, 61, 60, 59, + 59, 58, 57, 56, 56, 55, 54, 53]; + + let (normalized_exp, normalized_sig) = + if sub then { + let nr_leadingzeros = count_leadingzeros(sig, s); + assert(nr_leadingzeros >= 0); + (to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) + } else { + (exp, sig) + }; + + let idx : nat = match 'm { + 16 => unsigned([normalized_exp[0]] @ normalized_sig[9 .. 4]), + 32 => unsigned([normalized_exp[0]] @ normalized_sig[22 .. 17]), + 64 => unsigned([normalized_exp[0]] @ normalized_sig[51 .. 46]) + }; + assert(idx >= 0 & idx < 128); + let out_sig = to_bits(s, table[(127 - idx)]) << (s - 7); + let out_exp = to_bits(e, (3 * (2^(e - 1) - 1) - 1 - signed(normalized_exp)) / 2); + zero_extend(64, sign @ out_exp @ out_sig) +} + +val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) +function riscv_f16Rsqrte7 (rm, v) = { + match fp_class(v) { + 0x0001 => (nvFlag(), 0x7e00), + 0x0002 => (nvFlag(), 0x7e00), + 0x0004 => (nvFlag(), 0x7e00), + 0x0100 => (nvFlag(), 0x7e00), + 0x0200 => (zeros(5), 0x7e00), + 0x0008 => (dzFlag(), 0xfc00), + 0x0010 => (dzFlag(), 0x7c00), + 0x0080 => (zeros(5), 0x0000), + 0x0020 => (zeros(5), rsqrt7(v, true)[15 .. 0]), + _ => (zeros(5), rsqrt7(v, false)[15 .. 0]) + } +} + +val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) +function riscv_f32Rsqrte7 (rm, v) = { + match fp_class(v)[15 .. 0] { + 0x0001 => (nvFlag(), 0x7fc00000), + 0x0002 => (nvFlag(), 0x7fc00000), + 0x0004 => (nvFlag(), 0x7fc00000), + 0x0100 => (nvFlag(), 0x7fc00000), + 0x0200 => (zeros(5), 0x7fc00000), + 0x0008 => (dzFlag(), 0xff800000), + 0x0010 => (dzFlag(), 0x7f800000), + 0x0080 => (zeros(5), 0x00000000), + 0x0020 => (zeros(5), rsqrt7(v, true)[31 .. 0]), + _ => (zeros(5), rsqrt7(v, false)[31 .. 0]) + } +} + +val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) +function riscv_f64Rsqrte7 (rm, v) = { + match fp_class(v)[15 .. 0] { + 0x0001 => (nvFlag(), 0x7ff8000000000000), + 0x0002 => (nvFlag(), 0x7ff8000000000000), + 0x0004 => (nvFlag(), 0x7ff8000000000000), + 0x0100 => (nvFlag(), 0x7ff8000000000000), + 0x0200 => (zeros(5), 0x7ff8000000000000), + 0x0008 => (dzFlag(), 0xfff0000000000000), + 0x0010 => (dzFlag(), 0x7ff0000000000000), + 0x0080 => (zeros(5), zeros(64)), + 0x0020 => (zeros(5), rsqrt7(v, true)[63 .. 0]), + _ => (zeros(5), rsqrt7(v, false)[63 .. 0]) + } +} + +val recip7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bits(3), bool) -> (bool, bits_D) +function recip7 (v, rm_3b, sub) = { + let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm { + 16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10), + 32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23), + 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) + }; + assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); + let table : vector(128, dec, int) = [ + 127, 125, 123, 121, 119, 117, 116, 114, + 112, 110, 109, 107, 105, 104, 102, 100, + 99, 97, 96, 94, 93, 91, 90, 88, + 87, 85, 84, 83, 81, 80, 79, 77, + 76, 75, 74, 72, 71, 70, 69, 68, + 66, 65, 64, 63, 62, 61, 60, 59, + 58, 57, 56, 55, 54, 53, 52, 51, + 50, 49, 48, 47, 46, 45, 44, 43, + 42, 41, 40, 40, 39, 38, 37, 36, + 35, 35, 34, 33, 32, 31, 31, 30, + 29, 28, 28, 27, 26, 25, 25, 24, + 23, 23, 22, 21, 21, 20, 19, 19, + 18, 17, 17, 16, 15, 15, 14, 14, + 13, 12, 12, 11, 11, 10, 9, 9, + 8, 8, 7, 7, 6, 5, 5, 4, + 4, 3, 3, 2, 2, 1, 1, 0]; + + let nr_leadingzeros = count_leadingzeros(sig, s); + assert(nr_leadingzeros >= 0); + let (normalized_exp, normalized_sig) = + if sub then { + (to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) + } else { + (exp, sig) + }; + + let idx : nat = match 'm { + 16 => unsigned(normalized_sig[9 .. 3]), + 32 => unsigned(normalized_sig[22 .. 16]), + 64 => unsigned(normalized_sig[51 .. 45]) + }; + assert(idx >= 0 & idx < 128); + let mid_exp = to_bits(e, 2 * (2^(e - 1) - 1) - 1 - signed(normalized_exp)); + let mid_sig = to_bits(s, table[(127 - idx)]) << (s - 7); + + let (out_exp, out_sig)= + if mid_exp == zeros(e) then { + (mid_exp, mid_sig >> 1 | 0b1 @ zeros(s - 1)) + } else if mid_exp == ones(e) then { + (zeros(e), mid_sig >> 2 | 0b01 @ zeros(s - 2)) + } else (mid_exp, mid_sig); + + if sub & nr_leadingzeros > 1 then { + if (rm_3b == 0b001 | rm_3b == 0b010 & sign == 0b0 | rm_3b == 0b011 & sign == 0b1) then { + (true, zero_extend(64, sign @ ones(e - 1) @ 0b0 @ ones(s))) + } + else (true, zero_extend(64, sign @ ones(e) @ zeros(s))) + } else (false, zero_extend(64, sign @ out_exp @ out_sig)) +} + +val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) +function riscv_f16Recip7 (rm, v) = { + let (round_abnormal_true, res_true) = recip7(v, rm, true); + let (round_abnormal_false, res_false) = recip7(v, rm, false); + match fp_class(v) { + 0x0001 => (zeros(5), 0x8000), + 0x0080 => (zeros(5), 0x0000), + 0x0008 => (dzFlag(), 0xfc00), + 0x0010 => (dzFlag(), 0x7c00), + 0x0100 => (nvFlag(), 0x7e00), + 0x0200 => (zeros(5), 0x7e00), + 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), + 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), + _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[15 .. 0]) else (zeros(5), res_false[15 .. 0]) + } +} + +val riscv_f32Recip7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) +function riscv_f32Recip7 (rm, v) = { + let (round_abnormal_true, res_true) = recip7(v, rm, true); + let (round_abnormal_false, res_false) = recip7(v, rm, false); + match fp_class(v)[15 .. 0] { + 0x0001 => (zeros(5), 0x80000000), + 0x0080 => (zeros(5), 0x00000000), + 0x0008 => (dzFlag(), 0xff800000), + 0x0010 => (dzFlag(), 0x7f800000), + 0x0100 => (nvFlag(), 0x7fc00000), + 0x0200 => (zeros(5), 0x7fc00000), + 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), + 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), + _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[31 .. 0]) else (zeros(5), res_false[31 .. 0]) + } +} + +val riscv_f64Recip7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) +function riscv_f64Recip7 (rm, v) = { + let (round_abnormal_true, res_true) = recip7(v, rm, true); + let (round_abnormal_false, res_false) = recip7(v, rm, false); + match fp_class(v)[15 .. 0] { + 0x0001 => (zeros(5), 0x8000000000000000), + 0x0080 => (zeros(5), 0x0000000000000000), + 0x0008 => (dzFlag(), 0xfff0000000000000), + 0x0010 => (dzFlag(), 0x7ff0000000000000), + 0x0100 => (nvFlag(), 0x7ff8000000000000), + 0x0200 => (zeros(5), 0x7ff8000000000000), + 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), + 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), + _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[63 .. 0]) else (zeros(5), res_false[63 .. 0]) + } +} diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail new file mode 100755 index 0000000..55592c4 --- /dev/null +++ b/model/riscv_insts_vext_fp_vm.sail @@ -0,0 +1,142 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* ******************************************************************************* */ +/* This file implements part of the vector extension. */ +/* Mask instructions from Chap 13 (floating-point) */ +/* ******************************************************************************* */ + +/* ******************************* OPFVV (VVMTYPE) ******************************* */ +/* FVVM instructions' destination is a mask register */ +union clause ast = FVVMTYPE : (fvvmfunct6, bits(1), regidx, regidx, regidx) + +mapping encdec_fvvmfunct6 : fvvmfunct6 <-> bits(6) = { + FVVM_VMFEQ <-> 0b011000, + FVVM_VMFLE <-> 0b011001, + FVVM_VMFLT <-> 0b011011, + FVVM_VMFNE <-> 0b011100 +} + +mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) + +function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { + let rm_3b = fcsr[FRM]; + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + assert(SEW != 8); + + let 'n = num_elem; + let 'm = SEW; + + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); + result : vector('n, dec, bool) = undefined; + mask : vector('n, dec, bool) = undefined; + + (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + let res : bool = match funct6 { + FVVM_VMFEQ => fp_eq(vs2_val[i], vs1_val[i]), + FVVM_VMFNE => ~(fp_eq(vs2_val[i], vs1_val[i])), + FVVM_VMFLE => fp_le(vs2_val[i], vs1_val[i]), + FVVM_VMFLT => fp_lt(vs2_val[i], vs1_val[i]) + }; + result[i] = res + } + }; + + write_vmask(num_elem, vd, result); + vstart = zeros(); + RETIRE_SUCCESS +} + +mapping fvvmtype_mnemonic : fvvmfunct6 <-> string = { + FVVM_VMFEQ <-> "vmfeq.vv", + FVVM_VMFLE <-> "vmfle.vv", + FVVM_VMFLT <-> "vmflt.vv", + FVVM_VMFNE <-> "vmfne.vv" +} + +mapping clause assembly = FVVMTYPE(funct6, vm, vs2, vs1, vd) + <-> fvvmtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm) + +/* ******************************* OPFVF (VFMTYPE) ******************************* */ +/* VFM instructions' destination is a mask register */ +union clause ast = FVFMTYPE : (fvfmfunct6, bits(1), regidx, regidx, regidx) + +mapping encdec_fvfmfunct6 : fvfmfunct6 <-> bits(6) = { + VFM_VMFEQ <-> 0b011000, + VFM_VMFLE <-> 0b011001, + VFM_VMFLT <-> 0b011011, + VFM_VMFNE <-> 0b011100, + VFM_VMFGT <-> 0b011101, + VFM_VMFGE <-> 0b011111 +} + +mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) + +function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { + let rm_3b = fcsr[FRM]; + let SEW = get_sew(); + let LMUL_pow = get_lmul_pow(); + let num_elem = get_num_elem(LMUL_pow, SEW); + + if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; + assert(SEW != 8); + + let 'n = num_elem; + let 'm = SEW; + + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); + let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); + result : vector('n, dec, bool) = undefined; + mask : vector('n, dec, bool) = undefined; + + (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); + + foreach (i from 0 to (num_elem - 1)) { + if mask[i] then { + let res : bool = match funct6 { + VFM_VMFEQ => fp_eq(vs2_val[i], rs1_val), + VFM_VMFNE => ~(fp_eq(vs2_val[i], rs1_val)), + VFM_VMFLE => fp_le(vs2_val[i], rs1_val), + VFM_VMFLT => fp_lt(vs2_val[i], rs1_val), + VFM_VMFGE => fp_ge(vs2_val[i], rs1_val), + VFM_VMFGT => fp_gt(vs2_val[i], rs1_val) + }; + result[i] = res + } + }; + + write_vmask(num_elem, vd, result); + vstart = zeros(); + RETIRE_SUCCESS +} + +mapping fvfmtype_mnemonic : fvfmfunct6 <-> string = { + VFM_VMFEQ <-> "vmfeq.vf", + VFM_VMFLE <-> "vmfle.vf", + VFM_VMFLT <-> "vmflt.vf", + VFM_VMFNE <-> "vmfne.vf", + VFM_VMFGT <-> "vmfgt.vf", + VFM_VMFGE <-> "vmfge.vf" +} + +mapping clause assembly = FVFMTYPE(funct6, vm, vs2, rs1, vd) + <-> fvfmtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ maybe_vmask(vm) diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 1bd7657..2ce2f2c 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -142,118 +142,3 @@ mapping rmvvtype_mnemonic : rmvvfunct6 <-> string = { mapping clause assembly = RMVVTYPE(funct6, vm, vs2, vs1, vd) <-> rmvvtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm) - -/* ********************** OPFVV (Floating-Point Reduction) *********************** */ -union clause ast = RFVVTYPE : (rfvvfunct6, bits(1), regidx, regidx, regidx) - -mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = { - FVV_VFREDOSUM <-> 0b000011, - FVV_VFREDUSUM <-> 0b000001, - FVV_VFREDMAX <-> 0b000111, - FVV_VFREDMIN <-> 0b000101, - FVV_VFWREDOSUM <-> 0b110011, - FVV_VFWREDUSUM <-> 0b110001 -} - -mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) - <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) - -val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired -function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { - let rm_3b = fcsr[FRM]; - let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ - - if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; - assert(SEW != 8); - - if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ - - let 'n = num_elem_vs; - let 'd = num_elem_vd; - let 'm = SEW; - - let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); - let vd_val : vector('d, dec, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : vector('n, dec, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); - - sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ - foreach (i from 0 to (num_elem_vs - 1)) { - if mask[i] then { - sum = match funct6 { - /* currently ordered/unordered sum reductions do the same operations */ - FVV_VFREDOSUM => fp_add(rm_3b, sum, vs2_val[i]), - FVV_VFREDUSUM => fp_add(rm_3b, sum, vs2_val[i]), - FVV_VFREDMAX => fp_max(sum, vs2_val[i]), - FVV_VFREDMIN => fp_min(sum, vs2_val[i]), - _ => internal_error(__FILE__, __LINE__, "Widening op unexpected") - } - } - }; - - write_single_element(SEW, 0, vd, sum); - /* other elements in vd are treated as tail elements, currently remain unchanged */ - /* TODO: configuration support for agnostic behavior */ - vstart = zeros(); - RETIRE_SUCCESS -} - -val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired -function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { - let rm_3b = fcsr[FRM]; - let SEW_widen = SEW * 2; - let LMUL_pow_widen = LMUL_pow + 1; - let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */ - - if illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; - assert(SEW >= 16 & SEW_widen <= 64); - - if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */ - - let 'n = num_elem_vs; - let 'd = num_elem_vd; - let 'm = SEW; - let 'o = SEW_widen; - - let vm_val : vector('n, dec, bool) = read_vmask(num_elem_vs, vm, 0b00000); - let vd_val : vector('d, dec, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : vector('n, dec, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); - - sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */ - foreach (i from 0 to (num_elem_vs - 1)) { - if mask[i] then { - /* currently ordered/unordered sum reductions do the same operations */ - sum = fp_add(rm_3b, sum, fp_widen(vs2_val[i])) - } - }; - - write_single_element(SEW_widen, 0, vd, sum); - /* other elements in vd are treated as tail elements, currently remain unchanged */ - /* TODO: configuration support for agnostic behavior */ - vstart = zeros(); - RETIRE_SUCCESS -} - -function clause execute(RFVVTYPE(funct6, vm, vs2, vs1, vd)) = { - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let num_elem_vs = get_num_elem(LMUL_pow, SEW); - - if funct6 == FVV_VFWREDOSUM | funct6 == FVV_VFWREDUSUM then - process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) - else - process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) -} - -mapping rfvvtype_mnemonic : rfvvfunct6 <-> string = { - FVV_VFREDOSUM <-> "vfredosum.vs", - FVV_VFREDUSUM <-> "vfredusum.vs", - FVV_VFREDMAX <-> "vfredmax.vs", - FVV_VFREDMIN <-> "vfredmin.vs", - FVV_VFWREDOSUM <-> "vfwredosum.vs", - FVV_VFWREDUSUM <-> "vfwredusum.vs" -} - -mapping clause assembly = RFVVTYPE(funct6, vm, vs2, vs1, vd) - <-> rfvvtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm) diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 6796060..99d575b 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -41,18 +41,6 @@ function assert_vstart(i) = { unsigned(vstart) == i } -/* Check for valid floating-point operation types - * 1. Valid element width of floating-point numbers - * 2. Valid floating-point rounding mode - */ -val valid_fp_op : ({8, 16, 32, 64}, bits(3)) -> bool -function valid_fp_op(SEW, rm_3b) = { - /* 128-bit floating-point values will be supported in future extensions */ - let valid_sew = (SEW >= 16 & SEW <= 128); - let valid_rm = not(rm_3b == 0b101 | rm_3b == 0b110 | rm_3b == 0b111); - valid_sew & valid_rm -} - /* Check for valid destination register when vector masking is enabled: * The destination vector register group for a masked vector instruction * cannot overlap the source mask register (v0), @@ -145,65 +133,27 @@ function illegal_reduction_widen(SEW_widen, LMUL_pow_widen) = { not(valid_vtype()) | not(assert_vstart(0)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) } -/* g. Normal check for floating-point instructions */ -val illegal_fp_normal : (regidx, bits(1), {8, 16, 32, 64}, bits(3)) -> bool -function illegal_fp_normal(vd, vm, SEW, rm_3b) = { - not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) -} - -/* h. Masked check for floating-point instructions encoded with vm = 0 */ -val illegal_fp_vd_masked : (regidx, {8, 16, 32, 64}, bits(3)) -> bool -function illegal_fp_vd_masked(vd, SEW, rm_3b) = { - not(valid_vtype()) | vd == 0b00000 | not(valid_fp_op(SEW, rm_3b)) -} - -/* i. Unmasked check for floating-point instructions encoded with vm = 1 */ -val illegal_fp_vd_unmasked : ({8, 16, 32, 64}, bits(3)) -> bool -function illegal_fp_vd_unmasked(SEW, rm_3b) = { - not(valid_vtype()) | not(valid_fp_op(SEW, rm_3b)) -} - -/* j. Variable width check for floating-point widening/narrowing instructions */ -val illegal_fp_variable_width : (regidx, bits(1), {8, 16, 32, 64}, bits(3), int, int) -> bool -function illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_new, LMUL_pow_new) = { - not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | - not(valid_eew_emul(SEW_new, LMUL_pow_new)) -} - -/* k. Normal check for floating-point reduction instructions */ -val illegal_fp_reduction : ({8, 16, 32, 64}, bits(3)) -> bool -function illegal_fp_reduction(SEW, rm_3b) = { - not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) -} - -/* l. Variable width check for floating-point widening reduction instructions */ -val illegal_fp_reduction_widen : ({8, 16, 32, 64}, bits(3), int, int) -> bool -function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = { - not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) -} - -/* m. Non-indexed load instruction check */ +/* g. Non-indexed load instruction check */ val illegal_load : (regidx, bits(1), int, int, int) -> bool function illegal_load(vd, vm, nf, EEW, EMUL_pow) = { not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(EEW, EMUL_pow)) | not(valid_segment(nf, EMUL_pow)) } -/* n. Non-indexed store instruction check (with vs3 rather than vd) */ +/* h. Non-indexed store instruction check (with vs3 rather than vd) */ val illegal_store : (int, int, int) -> bool function illegal_store(nf, EEW, EMUL_pow) = { not(valid_vtype()) | not(valid_eew_emul(EEW, EMUL_pow)) | not(valid_segment(nf, EMUL_pow)) } -/* o. Indexed load instruction check */ +/* i. Indexed load instruction check */ val illegal_indexed_load : (regidx, bits(1), int, int, int, int) -> bool function illegal_indexed_load(vd, vm, nf, EEW_index, EMUL_pow_index, EMUL_pow_data) = { not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(EEW_index, EMUL_pow_index)) | not(valid_segment(nf, EMUL_pow_data)) } -/* p. Indexed store instruction check (with vs3 rather than vd) */ +/* j. Indexed store instruction check (with vs3 rather than vd) */ val illegal_indexed_store : (int, int, int, int) -> bool function illegal_indexed_store(nf, EEW_index, EMUL_pow_index, EMUL_pow_data) = { not(valid_vtype()) | not(valid_eew_emul(EEW_index, EMUL_pow_index)) | @@ -437,127 +387,6 @@ function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { result } -/* Floating point canonical NaN for 16-bit, 32-bit and 64-bit types */ -val canonical_NaN : forall 'm, 'm in {16, 32, 64}. int('m) -> bits('m) -function canonical_NaN('m) = { - match 'm { - 16 => canonical_NaN_H(), - 32 => canonical_NaN_S(), - 64 => canonical_NaN_D() - } -} - -/* 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) = { - match 'm { - 16 => f_is_neg_inf_H(xf), - 32 => f_is_neg_inf_S(xf), - 64 => f_is_neg_inf_D(xf) - } -} - -val f_is_neg_norm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_norm(xf) = { - match 'm { - 16 => f_is_neg_norm_H(xf), - 32 => f_is_neg_norm_S(xf), - 64 => f_is_neg_norm_D(xf) - } -} - -val f_is_neg_subnorm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_subnorm(xf) = { - match 'm { - 16 => f_is_neg_subnorm_H(xf), - 32 => f_is_neg_subnorm_S(xf), - 64 => f_is_neg_subnorm_D(xf) - } -} - -val f_is_neg_zero : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_neg_zero(xf) = { - match 'm { - 16 => f_is_neg_zero_H(xf), - 32 => f_is_neg_zero_S(xf), - 64 => f_is_neg_zero_D(xf) - } -} - -val f_is_pos_zero : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_zero(xf) = { - match 'm { - 16 => f_is_pos_zero_H(xf), - 32 => f_is_pos_zero_S(xf), - 64 => f_is_pos_zero_D(xf) - } -} - -val f_is_pos_subnorm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_subnorm(xf) = { - match 'm { - 16 => f_is_pos_subnorm_H(xf), - 32 => f_is_pos_subnorm_S(xf), - 64 => f_is_pos_subnorm_D(xf) - } -} - -val f_is_pos_norm : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_norm(xf) = { - match 'm { - 16 => f_is_pos_norm_H(xf), - 32 => f_is_pos_norm_S(xf), - 64 => f_is_pos_norm_D(xf) - } -} - -val f_is_pos_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_pos_inf(xf) = { - match 'm { - 16 => f_is_pos_inf_H(xf), - 32 => f_is_pos_inf_S(xf), - 64 => f_is_pos_inf_D(xf) - } -} - -val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_SNaN(xf) = { - match 'm { - 16 => f_is_SNaN_H(xf), - 32 => f_is_SNaN_S(xf), - 64 => f_is_SNaN_D(xf) - } -} - -val f_is_QNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_QNaN(xf) = { - match 'm { - 16 => f_is_QNaN_H(xf), - 32 => f_is_QNaN_S(xf), - 64 => f_is_QNaN_D(xf) - } -} - -val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool -function f_is_NaN(xf) = { - match 'm { - 16 => f_is_NaN_H(xf), - 32 => f_is_NaN_S(xf), - 64 => f_is_NaN_D(xf) - } -} - -/* Scalar register shaping for floating point operations */ -val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) -function get_scalar_fp(rs1, SEW) = { - 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) - } -} - /* Shift amounts */ val get_shift_amount : forall 'n 'm, 0 <= 'n & 'm in {8, 16, 32, 64}. (bits('n), int('m)) -> nat function get_shift_amount(bit_val, SEW) = { @@ -610,283 +439,6 @@ function signed_saturation(len, elem) = { }; } -/* Get the floating point rounding mode from csr fcsr */ -val get_fp_rounding_mode : unit -> rounding_mode -function get_fp_rounding_mode() = encdec_rounding_mode(fcsr[FRM]) - -/* Negate a floating point number */ -val negate_fp : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m) -function negate_fp(xf) = { - match 'm { - 16 => negate_H(xf), - 32 => negate_S(xf), - 64 => negate_D(xf) - } -} - -/* Floating point functions using softfloat interface */ -val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) -function fp_add(rm_3b, op1, op2) = { - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16Add(rm_3b, op1, op2), - 32 => riscv_f32Add(rm_3b, op1, op2), - 64 => riscv_f64Add(rm_3b, op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_sub: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) -function fp_sub(rm_3b, op1, op2) = { - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16Sub(rm_3b, op1, op2), - 32 => riscv_f32Sub(rm_3b, op1, op2), - 64 => riscv_f64Sub(rm_3b, op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_min : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) -function fp_min(op1, op2) = { - let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Lt_quiet(op1, op2), - 32 => riscv_f32Lt_quiet(op1, op2), - 64 => riscv_f64Lt_quiet(op1, op2) - }; - - let result_val = if (f_is_NaN(op1) & f_is_NaN(op2)) then canonical_NaN('m) - else if f_is_NaN(op1) then op2 - else if f_is_NaN(op2) then op1 - else if (f_is_neg_zero(op1) & f_is_pos_zero(op2)) then op1 - else if (f_is_neg_zero(op2) & f_is_pos_zero(op1)) then op2 - else if op1_lt_op2 then op1 - else op2; - accrue_fflags(fflags); - result_val -} - -val fp_max : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) -function fp_max(op1, op2) = { - let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Lt_quiet(op1, op2), - 32 => riscv_f32Lt_quiet(op1, op2), - 64 => riscv_f64Lt_quiet(op1, op2) - }; - - let result_val = if (f_is_NaN(op1) & f_is_NaN(op2)) then canonical_NaN('m) - else if f_is_NaN(op1) then op2 - else if f_is_NaN(op2) then op1 - else if (f_is_neg_zero(op1) & f_is_pos_zero(op2)) then op2 - else if (f_is_neg_zero(op2) & f_is_pos_zero(op1)) then op1 - else if op1_lt_op2 then op2 - else op1; - accrue_fflags(fflags); - result_val -} - -val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function fp_eq(op1, op2) = { - let (fflags, result_val) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Eq(op1, op2), - 32 => riscv_f32Eq(op1, op2), - 64 => riscv_f64Eq(op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function fp_gt(op1, op2) = { - let (fflags, temp_val) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Le(op1, op2), - 32 => riscv_f32Le(op1, op2), - 64 => riscv_f64Le(op1, op2) - }; - let result_val = (if fflags == 0b10000 then false else not(temp_val)); - accrue_fflags(fflags); - result_val -} - -val fp_ge : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function fp_ge(op1, op2) = { - let (fflags, temp_val) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Lt(op1, op2), - 32 => riscv_f32Lt(op1, op2), - 64 => riscv_f64Lt(op1, op2) - }; - let result_val = (if fflags == 0b10000 then false else not(temp_val)); - accrue_fflags(fflags); - result_val -} - -val fp_lt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function fp_lt(op1, op2) = { - let (fflags, result_val) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Lt(op1, op2), - 32 => riscv_f32Lt(op1, op2), - 64 => riscv_f64Lt(op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_le : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool -function fp_le(op1, op2) = { - let (fflags, result_val) : (bits_fflags, bool) = match 'm { - 16 => riscv_f16Le(op1, op2), - 32 => riscv_f32Le(op1, op2), - 64 => riscv_f64Le(op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_mul : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) -function fp_mul(rm_3b, op1, op2) = { - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16Mul(rm_3b, op1, op2), - 32 => riscv_f32Mul(rm_3b, op1, op2), - 64 => riscv_f64Mul(rm_3b, op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_div : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) -function fp_div(rm_3b, op1, op2) = { - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16Div(rm_3b, op1, op2), - 32 => riscv_f32Div(rm_3b, op1, op2), - 64 => riscv_f64Div(rm_3b, op1, op2) - }; - accrue_fflags(fflags); - result_val -} - -val fp_muladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) -function fp_muladd(rm_3b, op1, op2, opadd) = { - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16MulAdd(rm_3b, op1, op2, opadd), - 32 => riscv_f32MulAdd(rm_3b, op1, op2, opadd), - 64 => riscv_f64MulAdd(rm_3b, op1, op2, opadd) - }; - accrue_fflags(fflags); - result_val -} - -val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) -function fp_nmuladd(rm_3b, op1, op2, opadd) = { - let op1 = negate_fp(op1); - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16MulAdd(rm_3b, op1, op2, opadd), - 32 => riscv_f32MulAdd(rm_3b, op1, op2, opadd), - 64 => riscv_f64MulAdd(rm_3b, op1, op2, opadd) - }; - accrue_fflags(fflags); - result_val -} - -val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) -function fp_mulsub(rm_3b, op1, op2, opsub) = { - let opsub = negate_fp(opsub); - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16MulAdd(rm_3b, op1, op2, opsub), - 32 => riscv_f32MulAdd(rm_3b, op1, op2, opsub), - 64 => riscv_f64MulAdd(rm_3b, op1, op2, opsub) - }; - accrue_fflags(fflags); - result_val -} - -val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) -function fp_nmulsub(rm_3b, op1, op2, opsub) = { - let opsub = negate_fp(opsub); - let op1 = negate_fp(op1); - let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_f16MulAdd(rm_3b, op1, op2, opsub), - 32 => riscv_f32MulAdd(rm_3b, op1, op2, opsub), - 64 => riscv_f64MulAdd(rm_3b, op1, op2, opsub) - }; - accrue_fflags(fflags); - result_val -} - -val fp_class : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m) -function fp_class(xf) = { - let result_val_10b : bits(10) = - if f_is_neg_inf(xf) then 0b_00_0000_0001 - else if f_is_neg_norm(xf) then 0b_00_0000_0010 - else if f_is_neg_subnorm(xf) then 0b_00_0000_0100 - else if f_is_neg_zero(xf) then 0b_00_0000_1000 - else if f_is_pos_zero(xf) then 0b_00_0001_0000 - else if f_is_pos_subnorm(xf) then 0b_00_0010_0000 - else if f_is_pos_norm(xf) then 0b_00_0100_0000 - else if f_is_pos_inf(xf) then 0b_00_1000_0000 - else if f_is_SNaN(xf) then 0b_01_0000_0000 - else if f_is_QNaN(xf) then 0b_10_0000_0000 - else zeros(); - - zero_extend(result_val_10b) -} - -val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) -function fp_widen(nval) = { - let rm_3b = fcsr[FRM]; - let (fflags, wval) : (bits_fflags, bits('m * 2)) = match 'm { - 16 => riscv_f16ToF32(rm_3b, nval), - 32 => riscv_f32ToF64(rm_3b, nval) - }; - accrue_fflags(fflags); - wval -} - -/* Floating point functions without softfloat support */ -val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) -function riscv_f16ToI16 (rm, v) = { - let (_, sig32) = riscv_f16ToI32(rm, v); - if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) - else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag(), 0b1 @ zeros(15)) - else (zeros(5), sig32[15 .. 0]); -} - -val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) -function riscv_f16ToI8 (rm, v) = { - let (_, sig32) = riscv_f16ToI32(rm, v); - if signed(sig32) > signed(0b0 @ ones(7)) then (nvFlag(), 0b0 @ ones(7)) - else if signed(sig32) < signed(0b1 @ zeros(7)) then (nvFlag(), 0b1 @ zeros(7)) - else (zeros(5), sig32[7 .. 0]); -} - -val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) -function riscv_f32ToI16 (rm, v) = { - let (_, sig32) = riscv_f32ToI32(rm, v); - if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15)) - else if signed(sig32) < signed(0b1 @ zeros(15)) then (nvFlag(), 0b1 @ zeros(15)) - else (zeros(5), sig32[15 .. 0]); -} - -val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) -function riscv_f16ToUi16 (rm, v) = { - let (_, sig32) = riscv_f16ToUi32(rm, v); - if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) - else (zeros(5), sig32[15 .. 0]); -} - -val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) -function riscv_f16ToUi8 (rm, v) = { - let (_, sig32) = riscv_f16ToUi32(rm, v); - if unsigned(sig32) > unsigned(ones(8)) then (nvFlag(), ones(8)) - else (zeros(5), sig32[7 .. 0]); -} - -val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) -function riscv_f32ToUi16 (rm, v) = { - let (_, sig32) = riscv_f32ToUi32(rm, v); - if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16)) - else (zeros(5), sig32[15 .. 0]); -} - val count_leadingzeros : (bits(64), int) -> int function count_leadingzeros (sig, len) = { idx : int = -1; @@ -896,207 +448,3 @@ function count_leadingzeros (sig, len) = { }; len - idx - 1 } - -val rsqrt7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bool) -> bits_D -function rsqrt7 (v, sub) = { - let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm { - 16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10), - 32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23), - 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) - }; - assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); - let table : vector(128, dec, int) = [ - 52, 51, 50, 48, 47, 46, 44, 43, - 42, 41, 40, 39, 38, 36, 35, 34, - 33, 32, 31, 30, 30, 29, 28, 27, - 26, 25, 24, 23, 23, 22, 21, 20, - 19, 19, 18, 17, 16, 16, 15, 14, - 14, 13, 12, 12, 11, 10, 10, 9, - 9, 8, 7, 7, 6, 6, 5, 4, - 4, 3, 3, 2, 2, 1, 1, 0, - 127, 125, 123, 121, 119, 118, 116, 114, - 113, 111, 109, 108, 106, 105, 103, 102, - 100, 99, 97, 96, 95, 93, 92, 91, - 90, 88, 87, 86, 85, 84, 83, 82, - 80, 79, 78, 77, 76, 75, 74, 73, - 72, 71, 70, 70, 69, 68, 67, 66, - 65, 64, 63, 63, 62, 61, 60, 59, - 59, 58, 57, 56, 56, 55, 54, 53]; - - let (normalized_exp, normalized_sig) = - if sub then { - let nr_leadingzeros = count_leadingzeros(sig, s); - assert(nr_leadingzeros >= 0); - (to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) - } else { - (exp, sig) - }; - - let idx : nat = match 'm { - 16 => unsigned([normalized_exp[0]] @ normalized_sig[9 .. 4]), - 32 => unsigned([normalized_exp[0]] @ normalized_sig[22 .. 17]), - 64 => unsigned([normalized_exp[0]] @ normalized_sig[51 .. 46]) - }; - assert(idx >= 0 & idx < 128); - let out_sig = to_bits(s, table[(127 - idx)]) << (s - 7); - let out_exp = to_bits(e, (3 * (2^(e - 1) - 1) - 1 - signed(normalized_exp)) / 2); - zero_extend(64, sign @ out_exp @ out_sig) -} - -val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) -function riscv_f16Rsqrte7 (rm, v) = { - match fp_class(v) { - 0x0001 => (nvFlag(), 0x7e00), - 0x0002 => (nvFlag(), 0x7e00), - 0x0004 => (nvFlag(), 0x7e00), - 0x0100 => (nvFlag(), 0x7e00), - 0x0200 => (zeros(5), 0x7e00), - 0x0008 => (dzFlag(), 0xfc00), - 0x0010 => (dzFlag(), 0x7c00), - 0x0080 => (zeros(5), 0x0000), - 0x0020 => (zeros(5), rsqrt7(v, true)[15 .. 0]), - _ => (zeros(5), rsqrt7(v, false)[15 .. 0]) - } -} - -val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Rsqrte7 (rm, v) = { - match fp_class(v)[15 .. 0] { - 0x0001 => (nvFlag(), 0x7fc00000), - 0x0002 => (nvFlag(), 0x7fc00000), - 0x0004 => (nvFlag(), 0x7fc00000), - 0x0100 => (nvFlag(), 0x7fc00000), - 0x0200 => (zeros(5), 0x7fc00000), - 0x0008 => (dzFlag(), 0xff800000), - 0x0010 => (dzFlag(), 0x7f800000), - 0x0080 => (zeros(5), 0x00000000), - 0x0020 => (zeros(5), rsqrt7(v, true)[31 .. 0]), - _ => (zeros(5), rsqrt7(v, false)[31 .. 0]) - } -} - -val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Rsqrte7 (rm, v) = { - match fp_class(v)[15 .. 0] { - 0x0001 => (nvFlag(), 0x7ff8000000000000), - 0x0002 => (nvFlag(), 0x7ff8000000000000), - 0x0004 => (nvFlag(), 0x7ff8000000000000), - 0x0100 => (nvFlag(), 0x7ff8000000000000), - 0x0200 => (zeros(5), 0x7ff8000000000000), - 0x0008 => (dzFlag(), 0xfff0000000000000), - 0x0010 => (dzFlag(), 0x7ff0000000000000), - 0x0080 => (zeros(5), zeros(64)), - 0x0020 => (zeros(5), rsqrt7(v, true)[63 .. 0]), - _ => (zeros(5), rsqrt7(v, false)[63 .. 0]) - } -} - -val recip7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bits(3), bool) -> (bool, bits_D) -function recip7 (v, rm_3b, sub) = { - let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm { - 16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10), - 32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23), - 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) - }; - assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); - let table : vector(128, dec, int) = [ - 127, 125, 123, 121, 119, 117, 116, 114, - 112, 110, 109, 107, 105, 104, 102, 100, - 99, 97, 96, 94, 93, 91, 90, 88, - 87, 85, 84, 83, 81, 80, 79, 77, - 76, 75, 74, 72, 71, 70, 69, 68, - 66, 65, 64, 63, 62, 61, 60, 59, - 58, 57, 56, 55, 54, 53, 52, 51, - 50, 49, 48, 47, 46, 45, 44, 43, - 42, 41, 40, 40, 39, 38, 37, 36, - 35, 35, 34, 33, 32, 31, 31, 30, - 29, 28, 28, 27, 26, 25, 25, 24, - 23, 23, 22, 21, 21, 20, 19, 19, - 18, 17, 17, 16, 15, 15, 14, 14, - 13, 12, 12, 11, 11, 10, 9, 9, - 8, 8, 7, 7, 6, 5, 5, 4, - 4, 3, 3, 2, 2, 1, 1, 0]; - - let nr_leadingzeros = count_leadingzeros(sig, s); - assert(nr_leadingzeros >= 0); - let (normalized_exp, normalized_sig) = - if sub then { - (to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) - } else { - (exp, sig) - }; - - let idx : nat = match 'm { - 16 => unsigned(normalized_sig[9 .. 3]), - 32 => unsigned(normalized_sig[22 .. 16]), - 64 => unsigned(normalized_sig[51 .. 45]) - }; - assert(idx >= 0 & idx < 128); - let mid_exp = to_bits(e, 2 * (2^(e - 1) - 1) - 1 - signed(normalized_exp)); - let mid_sig = to_bits(s, table[(127 - idx)]) << (s - 7); - - let (out_exp, out_sig)= - if mid_exp == zeros(e) then { - (mid_exp, mid_sig >> 1 | 0b1 @ zeros(s - 1)) - } else if mid_exp == ones(e) then { - (zeros(e), mid_sig >> 2 | 0b01 @ zeros(s - 2)) - } else (mid_exp, mid_sig); - - if sub & nr_leadingzeros > 1 then { - if (rm_3b == 0b001 | rm_3b == 0b010 & sign == 0b0 | rm_3b == 0b011 & sign == 0b1) then { - (true, zero_extend(64, sign @ ones(e - 1) @ 0b0 @ ones(s))) - } - else (true, zero_extend(64, sign @ ones(e) @ zeros(s))) - } else (false, zero_extend(64, sign @ out_exp @ out_sig)) -} - -val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) -function riscv_f16Recip7 (rm, v) = { - let (round_abnormal_true, res_true) = recip7(v, rm, true); - let (round_abnormal_false, res_false) = recip7(v, rm, false); - match fp_class(v) { - 0x0001 => (zeros(5), 0x8000), - 0x0080 => (zeros(5), 0x0000), - 0x0008 => (dzFlag(), 0xfc00), - 0x0010 => (dzFlag(), 0x7c00), - 0x0100 => (nvFlag(), 0x7e00), - 0x0200 => (zeros(5), 0x7e00), - 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), - 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[15 .. 0]) else (zeros(5), res_true[15 .. 0]), - _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[15 .. 0]) else (zeros(5), res_false[15 .. 0]) - } -} - -val riscv_f32Recip7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) -function riscv_f32Recip7 (rm, v) = { - let (round_abnormal_true, res_true) = recip7(v, rm, true); - let (round_abnormal_false, res_false) = recip7(v, rm, false); - match fp_class(v)[15 .. 0] { - 0x0001 => (zeros(5), 0x80000000), - 0x0080 => (zeros(5), 0x00000000), - 0x0008 => (dzFlag(), 0xff800000), - 0x0010 => (dzFlag(), 0x7f800000), - 0x0100 => (nvFlag(), 0x7fc00000), - 0x0200 => (zeros(5), 0x7fc00000), - 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), - 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[31 .. 0]) else (zeros(5), res_true[31 .. 0]), - _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[31 .. 0]) else (zeros(5), res_false[31 .. 0]) - } -} - -val riscv_f64Recip7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) -function riscv_f64Recip7 (rm, v) = { - let (round_abnormal_true, res_true) = recip7(v, rm, true); - let (round_abnormal_false, res_false) = recip7(v, rm, false); - match fp_class(v)[15 .. 0] { - 0x0001 => (zeros(5), 0x8000000000000000), - 0x0080 => (zeros(5), 0x0000000000000000), - 0x0008 => (dzFlag(), 0xfff0000000000000), - 0x0010 => (dzFlag(), 0x7ff0000000000000), - 0x0100 => (nvFlag(), 0x7ff8000000000000), - 0x0200 => (zeros(5), 0x7ff8000000000000), - 0x0004 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), - 0x0020 => if round_abnormal_true then (nxFlag() | ofFlag(), res_true[63 .. 0]) else (zeros(5), res_true[63 .. 0]), - _ => if round_abnormal_false then (nxFlag() | ofFlag(), res_false[63 .. 0]) else (zeros(5), res_false[63 .. 0]) - } -} diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 745f53e..91ce3f3 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -8,7 +8,7 @@ /* ******************************************************************************* */ /* This file implements part of the vector extension. */ -/* Mask instructions from Chap 11 (integer arithmetic) and 13 (floating-point) */ +/* Mask instructions from Chap 11 (integer arithmetic) */ /* ******************************************************************************* */ /* ******************************* OPIVV (VVMTYPE) ******************************* */ @@ -721,133 +721,3 @@ mapping vicmptype_mnemonic : vicmpfunct6 <-> string = { mapping clause assembly = VICMPTYPE(funct6, vm, vs2, simm, vd) <-> vicmptype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ hex_bits_5(simm) ^ maybe_vmask(vm) - -/* ******************************* OPFVV (VVMTYPE) ******************************* */ -/* FVVM instructions' destination is a mask register */ -union clause ast = FVVMTYPE : (fvvmfunct6, bits(1), regidx, regidx, regidx) - -mapping encdec_fvvmfunct6 : fvvmfunct6 <-> bits(6) = { - FVVM_VMFEQ <-> 0b011000, - FVVM_VMFLE <-> 0b011001, - FVVM_VMFLT <-> 0b011011, - FVVM_VMFNE <-> 0b011100 -} - -mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) - <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) - -function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { - let rm_3b = fcsr[FRM]; - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); - - if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; - assert(SEW != 8); - - let 'n = num_elem; - let 'm = SEW; - - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); - result : vector('n, dec, bool) = undefined; - mask : vector('n, dec, bool) = undefined; - - (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { - let res : bool = match funct6 { - FVVM_VMFEQ => fp_eq(vs2_val[i], vs1_val[i]), - FVVM_VMFNE => ~(fp_eq(vs2_val[i], vs1_val[i])), - FVVM_VMFLE => fp_le(vs2_val[i], vs1_val[i]), - FVVM_VMFLT => fp_lt(vs2_val[i], vs1_val[i]) - }; - result[i] = res - } - }; - - write_vmask(num_elem, vd, result); - vstart = zeros(); - RETIRE_SUCCESS -} - -mapping fvvmtype_mnemonic : fvvmfunct6 <-> string = { - FVVM_VMFEQ <-> "vmfeq.vv", - FVVM_VMFLE <-> "vmfle.vv", - FVVM_VMFLT <-> "vmflt.vv", - FVVM_VMFNE <-> "vmfne.vv" -} - -mapping clause assembly = FVVMTYPE(funct6, vm, vs2, vs1, vd) - <-> fvvmtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ vreg_name(vs1) ^ maybe_vmask(vm) - -/* ******************************* OPFVF (VFMTYPE) ******************************* */ -/* VFM instructions' destination is a mask register */ -union clause ast = FVFMTYPE : (fvfmfunct6, bits(1), regidx, regidx, regidx) - -mapping encdec_fvfmfunct6 : fvfmfunct6 <-> bits(6) = { - VFM_VMFEQ <-> 0b011000, - VFM_VMFLE <-> 0b011001, - VFM_VMFLT <-> 0b011011, - VFM_VMFNE <-> 0b011100, - VFM_VMFGT <-> 0b011101, - VFM_VMFGE <-> 0b011111 -} - -mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) - <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) - -function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { - let rm_3b = fcsr[FRM]; - let SEW = get_sew(); - let LMUL_pow = get_lmul_pow(); - let num_elem = get_num_elem(LMUL_pow, SEW); - - if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; - assert(SEW != 8); - - let 'n = num_elem; - let 'm = SEW; - - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); - let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); - result : vector('n, dec, bool) = undefined; - mask : vector('n, dec, bool) = undefined; - - (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val); - - foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { - let res : bool = match funct6 { - VFM_VMFEQ => fp_eq(vs2_val[i], rs1_val), - VFM_VMFNE => ~(fp_eq(vs2_val[i], rs1_val)), - VFM_VMFLE => fp_le(vs2_val[i], rs1_val), - VFM_VMFLT => fp_lt(vs2_val[i], rs1_val), - VFM_VMFGE => fp_ge(vs2_val[i], rs1_val), - VFM_VMFGT => fp_gt(vs2_val[i], rs1_val) - }; - result[i] = res - } - }; - - write_vmask(num_elem, vd, result); - vstart = zeros(); - RETIRE_SUCCESS -} - -mapping fvfmtype_mnemonic : fvfmfunct6 <-> string = { - VFM_VMFEQ <-> "vmfeq.vf", - VFM_VMFLE <-> "vmfle.vf", - VFM_VMFLT <-> "vmflt.vf", - VFM_VMFNE <-> "vmfne.vf", - VFM_VMFGT <-> "vmfgt.vf", - VFM_VMFGE <-> "vmfge.vf" -} - -mapping clause assembly = FVFMTYPE(funct6, vm, vs2, rs1, vd) - <-> fvfmtype_mnemonic(funct6) ^ spc() ^ vreg_name(vd) ^ sep() ^ vreg_name(vs2) ^ sep() ^ reg_name(rs1) ^ maybe_vmask(vm) |