From 46fd0299d1aa76ace29c49b406940a3e9af2b7f3 Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Sat, 6 Apr 2024 23:20:41 -0700 Subject: [PATCH] Updates for consistency between F, D, Q, and Zfh. Complete implementation of fmin/fmax for Q --- model/riscv_fdext_control.sail | 12 +- model/riscv_fdext_regs.sail | 31 ++++- model/riscv_freg_type.sail | 18 +-- model/riscv_insts_dext.sail | 6 +- model/riscv_insts_fext.sail | 8 +- model/riscv_insts_qext.sail | 240 +++++++++++++++++++-------------- model/riscv_insts_zfh.sail | 6 +- 7 files changed, 188 insertions(+), 133 deletions(-) diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 8f299994b..74f0b029f 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -6,14 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* **************************************************************** */ -/* Floating point register file and accessors for F, D extensions */ -/* Floating point CSR and accessors */ -/* **************************************************************** */ +/* ***************************************************************** */ +/* Floating point register file and accessors for F, D, Q extensions */ +/* Floating point CSR and accessors */ +/* ***************************************************************** */ -/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ -/* **************************************************************** */ +/* ***************************************************************** */ /* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */ diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 67c9706a4..a8c7c4d80 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -15,13 +15,17 @@ /* **************************************************************** */ /* NaN boxing/unboxing. */ -/* When 16-bit floats (half-precision) are stored in 32/64-bit regs */ -/* they must be 'NaN boxed'. */ -/* When 16-bit floats (half-precision) are read from 32/64-bit regs */ -/* they must be 'NaN unboxed'. */ -/* When 32-bit floats (single-precision) are stored in 64-bit regs */ +/* When 16-bit floats (half-precision) are stored in 32/64/128-bit */ +/* regs they must be 'NaN boxed'. */ +/* When 16-bit floats (half-precision) are read from 32/64/128-bit */ +/* regs they must be 'NaN unboxed'. */ +/* When 32-bit floats (single-precision) are stored in 64/128-bit */ +/* regs they must be 'NaN boxed'. */ +/* When 32-bit floats (single-precision) are read from 64/128-bit */ +/* regs they must be 'NaN unboxed'. */ +/* When 64-bit floats (double-precision) are stored in 128-bit regs */ /* they must be 'NaN boxed' (upper 32b all ones). */ -/* When 32-bit floats (single-precision) are read from 64-bit regs */ +/* When 64-bit floats (double-precision) are read from 128-bit regs */ /* they must be 'NaN unboxed'. */ function canonical_NaN_H() -> bits(16) = 0x_7e00 @@ -290,9 +294,24 @@ function wF_D(i, data) = { F(i) = nan_box(data) } +val rF_Q : bits(5) -> bits(128) +function rF_Q(i) = { + assert(sizeof(flen) >= 128); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) +} + +val wF_Q : (bits(5), bits(128)) -> unit +function wF_Q(i, data) = { + assert(sizeof(flen) >= 128); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) = data +} + overload F_H = { rF_H, wF_H } overload F_S = { rF_S, wF_S } overload F_D = { rF_D, wF_D } +overload F_Q = { rF_Q, wF_Q } val rF_or_X_H : bits(5) -> bits(16) function rF_or_X_H(i) = { diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail index be2d12c8d..c9478271f 100644 --- a/model/riscv_freg_type.sail +++ b/model/riscv_freg_type.sail @@ -60,25 +60,25 @@ enum f_bin_op_S = {FSGNJ_S, FSGNJN_S, FSGNJX_S, FMIN_S, FMAX_S, FEQ_S, FLT_S, FL enum f_madd_op_D = {FMADD_D, FMSUB_D, FNMSUB_D, FNMADD_D} -enum f_madd_op_Q = {FMADD_Q, FMSUB_Q, FNMSUB_Q, FNMADD_Q} - enum f_bin_rm_op_D = {FADD_D, FSUB_D, FMUL_D, FDIV_D} -enum f_bin_rm_op_Q = {FADD_Q, FSUB_Q, FMUL_Q, FDIV_Q} - 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_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FLE_D} + +enum f_un_op_D = {FCLASS_D, /* RV32 and RV64 */ + FMV_X_D, FMV_D_X} /* RV64 only */ + +enum f_madd_op_Q = {FMADD_Q, FMSUB_Q, FNMSUB_Q, FNMADD_Q} + +enum f_bin_rm_op_Q = {FADD_Q, FSUB_Q, FMUL_Q, FDIV_Q} + enum f_un_rm_op_Q = {FSQRT_Q, FCVT_W_Q, FCVT_WU_Q, FCVT_Q_W, FCVT_Q_WU, // RV32 and RV64 FCVT_S_Q, FCVT_Q_S, FCVT_D_Q, FCVT_Q_D, FCVT_L_Q, FCVT_LU_Q, FCVT_Q_L, FCVT_Q_LU} // RV64 only -enum f_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FLE_D} - enum f_bin_op_Q = {FSGNJ_Q, FSGNJN_Q, FSGNJX_Q, FMIN_Q, FMAX_Q, FEQ_Q, FLT_Q, FLE_Q} -enum f_un_op_D = {FCLASS_D, /* RV32 and RV64 */ - FMV_X_D, FMV_D_X} /* RV64 only */ - enum f_un_op_Q = {FCLASS_Q} diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index db967e525..43d27f6de 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -16,9 +16,9 @@ /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 25f42ef82..8c1b57059 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -16,9 +16,9 @@ /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ @@ -384,11 +384,9 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if haveDExt() <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if haveDExt() - mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, QUAD) if haveQExt() <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b100 @ imm5 : bits(5) @ 0b010_0111 if haveQExt() - /* Execution semantics ================================ */ val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired diff --git a/model/riscv_insts_qext.sail b/model/riscv_insts_qext.sail index 014061d17..124827dab 100644 --- a/model/riscv_insts_qext.sail +++ b/model/riscv_insts_qext.sail @@ -7,8 +7,8 @@ /*=======================================================================================*/ /* **************************************************************** */ -/* This file specifies the instructions in the F extension */ -/* (single precision floating point). */ +/* This file specifies the instructions in the Q extension */ +/* (quad precision floating point). */ /* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */ @@ -16,14 +16,18 @@ /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ /* **************************************************************** */ +/* Note: Rounding Modes and Floating point accrued exception flags */ +/* are defined in riscv_insts_fext.sail. */ +/* In RISC-V, the Q extension requires the F extension, so that */ +/* should have been processed before this one. */ /* **************************************************************** */ /* S and D value structure (sign, exponent, mantissa) */ @@ -217,35 +221,45 @@ function fle_Q (v1, v2, is_quiet) = { (result, fflags) } +/* ****************************************************************** */ +/* Floating-point loads */ +/* These are defined in: riscv_insts_fext.sail */ + +/* ****************************************************************** */ +/* Floating-point stores */ +/* These are defined in: riscv_insts_fext.sail */ +/* ****************************************************************** */ +/* Fused multiply-add */ -/* not sure about the bits repr, thus extract here TODO : check the repr */ -let Q_word_width_repr = 0b100 +/* AST */ -/* AST <-> Binary encoding ================================ */ union clause ast = F_MADD_TYPE_Q : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_Q) +/* AST <-> Binary encoding ================================ */ + mapping clause encdec = - F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FMADD_Q) if haveQExt() -<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if haveQExt() + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FMADD_Q) if haveQExt() +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if haveQExt() mapping clause encdec = - F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FMSUB_Q) if haveQExt() -<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if haveQExt() + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FMSUB_Q) if haveQExt() +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if haveQExt() mapping clause encdec = - F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FNMSUB_Q) if haveQExt() -<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if haveQExt() + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FNMSUB_Q) if haveQExt() +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if haveQExt() mapping clause encdec = - F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FNMADD_Q) if haveQExt() -<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if haveQExt() + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FNMADD_Q) if haveQExt() +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if haveQExt() +/* Execution semantics ================================ */ function clause execute (F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, op)) = { - let rs1_val_128b = F(rs1); - let rs2_val_128b = F(rs2); - let rs3_val_128b = F(rs3); + let rs1_val_128b = F_Q(rs1); + let rs2_val_128b = F_Q(rs2); + let rs3_val_128b = F_Q(rs3); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -259,12 +273,14 @@ function clause execute (F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, op)) = { FNMADD_Q => riscv_f128MulAdd (rm_3b, negate_Q (rs1_val_128b), rs2_val_128b, negate_Q (rs3_val_128b)) }; accrue_fflags(fflags); - F(rd) = rd_val_128b; + F_Q(rd) = rd_val_128b; RETIRE_SUCCESS } } } +/* AST -> Assembly notation ================================ */ + mapping f_madd_type_mnemonic_Q : f_madd_op_Q <-> string = { FMADD_Q <-> "fmadd.q", FMSUB_Q <-> "fmsub.q", @@ -280,7 +296,10 @@ mapping clause assembly = F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, op) ^ sep() ^ freg_or_reg_name(rs3) ^ sep() ^ frm_mnemonic(rm) +/* ****************************************************************** */ +/* Binary ops with rounding mode */ +/* AST */ union clause ast = F_BIN_RM_TYPE_Q : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_Q) @@ -305,8 +324,8 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, op)) = { - let rs1_val_128b = F(rs1); - let rs2_val_128b = F(rs2); + let rs1_val_128b = F_Q(rs1); + let rs2_val_128b = F_Q(rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -318,7 +337,7 @@ function clause execute (F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, op)) = { FDIV_Q => riscv_f128Div (rm_3b, rs1_val_128b, rs2_val_128b) }; accrue_fflags(fflags); - F(rd) = rd_val_128b; + F_Q(rd) = rd_val_128b; RETIRE_SUCCESS } } @@ -340,7 +359,6 @@ mapping clause assembly = F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, op) ^ sep() ^ freg_or_reg_name(rs2) ^ sep() ^ frm_mnemonic(rm) - /* ****************************************************************** */ /* Unary with rounding mode */ @@ -407,7 +425,7 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FSQRT_Q)) = { - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -415,14 +433,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FSQRT_Q)) = { let (fflags, rd_val_Q) = riscv_f128Sqrt (rm_3b, rs1_val_Q); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_W_Q)) = { - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -437,7 +455,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_W_Q)) = { } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_WU_Q)) = { - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -460,7 +478,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_W)) = { let (fflags, rd_val_Q) = riscv_i32ToF128 (rm_3b, rs1_val_W); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } @@ -475,14 +493,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_WU)) = { let (fflags, rd_val_Q) = riscv_ui32ToF128 (rm_3b, rs1_val_WU); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_S_Q)) = { - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -490,14 +508,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_S_Q)) = { let (fflags, rd_val_S) = riscv_f128ToF32 (rm_3b, rs1_val_Q); accrue_fflags(fflags); - F(rd) = rd_val_S; + F_Q(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_S)) = { - let rs1_val_S = F(rs1); + let rs1_val_S = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -505,14 +523,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_S)) = { let (fflags, rd_val_Q) = riscv_f32ToF128 (rm_3b, rs1_val_S); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_D_Q)) = { - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -520,14 +538,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_D_Q)) = { let (fflags, rd_val_D) = riscv_f128ToF64 (rm_3b, rs1_val_Q); accrue_fflags(fflags); - F(rd) = rd_val_D; + F_Q(rd) = rd_val_D; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -535,7 +553,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D)) = { let (fflags, rd_val_Q) = riscv_f64ToF128 (rm_3b, rs1_val_D); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } @@ -543,7 +561,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D)) = { function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_L_Q)) = { assert(sizeof(xlen) >= 64); - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -559,7 +577,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_L_Q)) = { function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_LU_Q)) = { assert(sizeof(xlen) >= 64); - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -583,7 +601,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_L)) = { let (fflags, rd_val_Q) = riscv_i64ToF128 (rm_3b, rs1_val_L); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } @@ -599,7 +617,7 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_LU)) = { let (fflags, rd_val_Q) = riscv_ui64ToF128 (rm_3b, rs1_val_LU); accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } } @@ -711,7 +729,7 @@ mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D) union clause ast = F_BIN_TYPE_Q : (regidx, regidx, regidx, f_bin_op_Q) -/* AST <-> Binary encoding ================ */ +/* AST <-> Binary encoding ================================ */ mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJ_Q) if haveQExt() <-> 0b001_0011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveQExt() @@ -722,6 +740,11 @@ mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJN_Q) if hav mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJX_Q) if haveQExt() <-> 0b001_0011 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveQExt() +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q) if haveQExt() + <-> 0b001_0111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveQExt() + +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q) if haveQExt() + <-> 0b001_0111 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveQExt() mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if haveQExt() <-> 0b101_0011 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveQExt() @@ -732,80 +755,45 @@ mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if hav mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if haveQExt() <-> 0b101_0011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveQExt() +/* Execution semantics ================================ */ + function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJ_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); let (s1, e1, m1) = fsplit_Q (rs1_val_Q); let (s2, e2, m2) = fsplit_Q (rs2_val_Q); let rd_val_Q = fmake_Q (s2, e1, m1); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJN_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); let (s1, e1, m1) = fsplit_Q (rs1_val_Q); let (s2, e2, m2) = fsplit_Q (rs2_val_Q); let rd_val_Q = fmake_Q (0b1 ^ s2, e1, m1); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJX_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); let (s1, e1, m1) = fsplit_Q (rs1_val_Q); let (s2, e2, m2) = fsplit_Q (rs2_val_Q); let rd_val_Q = fmake_Q (s1 ^ s2, e1, m1); - F(rd) = rd_val_Q; - RETIRE_SUCCESS -} - -function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FEQ_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); - - let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f128Eq (rs1_val_Q, rs2_val_Q); - - accrue_fflags(fflags); - X(rd) = zero_extend(bool_to_bits(rd_val)); - RETIRE_SUCCESS -} - -function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FLT_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); - - let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f128Lt (rs1_val_Q, rs2_val_Q); - - accrue_fflags(fflags); - X(rd) = zero_extend(bool_to_bits(rd_val)); - RETIRE_SUCCESS -} - -function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FLE_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); - - let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f128Le (rs1_val_Q, rs2_val_Q); - - accrue_fflags(fflags); - X(rd) = zero_extend(bool_to_bits(rd_val)); + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } - function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_Q (rs1_val_Q, rs2_val_Q, is_quiet); @@ -819,13 +807,13 @@ function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q)) = { else /* (not rs1_lt_rs2) */ rs2_val_Q; accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q)) = { - let rs1_val_Q = F(rs1); - let rs2_val_Q = F(rs2); + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_Q (rs2_val_Q, rs1_val_Q, is_quiet); @@ -839,10 +827,48 @@ function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q)) = { else /* (not rs2_lt_rs1) */ rs2_val_Q; accrue_fflags(fflags); - F(rd) = rd_val_Q; + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FEQ_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Eq (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FLT_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Lt (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FLE_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Le (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + mapping f_bin_type_mnemonic_Q : f_bin_op_Q <-> string = { FSGNJ_Q <-> "fsgnj.q", FSGNJN_Q <-> "fsgnjn.q", @@ -872,7 +898,17 @@ mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJX_Q) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q) + <-> f_bin_type_mnemonic_Q(FMIN_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q) + <-> f_bin_type_mnemonic_Q(FMAX_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FEQ_Q) <-> f_bin_type_mnemonic_Q(FEQ_Q) ^ spc() ^ reg_name(rd) @@ -891,7 +927,6 @@ mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FLE_Q) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) - /* ****************************************************************** */ /* Unary, no rounding mode */ @@ -899,12 +934,13 @@ union clause ast = F_UN_TYPE_Q : (regidx, regidx, f_un_op_Q) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = F_UN_TYPE_Q(rs1, rd, FCLASS_Q) - <-> 0b111_0011 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 - +mapping clause encdec = F_UN_TYPE_Q(rs1, rd, FCLASS_Q) if haveQExt() + <-> 0b111_0011 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveQExt() +/* FMV Q instructions are RV128 only */ +/* Execution semantics ================================ */ function clause execute (F_UN_TYPE_Q(rs1, rd, FCLASS_Q)) = { - let rs1_val_Q = F(rs1); + let rs1_val_Q = F_Q(rs1); let rd_val_10b : bits (10) = if f_is_neg_inf_Q (rs1_val_Q) then 0b_00_0000_0001 @@ -923,13 +959,15 @@ function clause execute (F_UN_TYPE_Q(rs1, rd, FCLASS_Q)) = { RETIRE_SUCCESS } +/* AST -> Assembly notation ================================ */ mapping f_un_type_mnemonic_Q : f_un_op_Q <-> string = { FCLASS_Q <-> "fclass.d" } - mapping clause assembly = F_UN_TYPE_Q(rs1, rd, FCLASS_Q) <-> f_un_type_mnemonic_Q(FCLASS_Q) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) + +/* ****************************************************************** */ diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 5522bad22..f16d99895 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -16,9 +16,9 @@ /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */