/*=======================================================================================*/ /* 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 specifies the instructions in the F extension */ /* (single precision floating point). */ /* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */ /* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ /* **************************************************************** */ /* 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 texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ /* **************************************************************** */ mapping encdec_rounding_mode : rounding_mode <-> bits(3) = { RM_RNE <-> 0b000, RM_RTZ <-> 0b001, RM_RDN <-> 0b010, RM_RUP <-> 0b011, RM_RMM <-> 0b100, RM_DYN <-> 0b111 } mapping frm_mnemonic : rounding_mode <-> string = { RM_RNE <-> "rne", RM_RTZ <-> "rtz", RM_RDN <-> "rdn", RM_RUP <-> "rup", RM_RMM <-> "rmm", RM_DYN <-> "dyn" } val valid_rounding_mode : bits(3) -> bool function valid_rounding_mode rm = (rm != 0b101 & rm != 0b110) val select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode) function select_instr_or_fcsr_rm instr_rm = if (instr_rm == RM_DYN) then { let fcsr_rm = fcsr[FRM]; if (valid_rounding_mode(fcsr_rm) & fcsr_rm != encdec_rounding_mode(RM_DYN)) then Some(encdec_rounding_mode(fcsr_rm)) else None() } else Some(instr_rm) /* **************************************************************** */ /* Floating point accrued exception flags */ function nxFlag() -> bits(5) = 0b_00001 function ufFlag() -> bits(5) = 0b_00010 function ofFlag() -> bits(5) = 0b_00100 function dzFlag() -> bits(5) = 0b_01000 function nvFlag() -> bits(5) = 0b_10000 /* **************************************************************** */ /* S and D value structure (sign, exponent, mantissa) */ /* TODO: this should be a 'mapping' */ val fsplit_S : bits(32) -> (bits(1), bits(8), bits(23)) function fsplit_S x32 = (x32[31..31], x32[30..23], x32[22..0]) val fmake_S : (bits(1), bits(8), bits(23)) -> bits(32) function fmake_S (sign, exp, mant) = sign @ exp @ mant /* ---- Structure tests */ val f_is_neg_inf_S : bits(32) -> bool function f_is_neg_inf_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == 0b1) & (exp == ones()) & (mant == zeros())) } val f_is_neg_norm_S : bits(32) -> bool function f_is_neg_norm_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == 0b1) & (exp != zeros()) & (exp != ones())) } val f_is_neg_subnorm_S : bits(32) -> bool function f_is_neg_subnorm_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == 0b1) & (exp == zeros()) & (mant != zeros())) } val f_is_neg_zero_S : bits(32) -> bool function f_is_neg_zero_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == ones()) & (exp == zeros()) & (mant == zeros())) } val f_is_pos_zero_S : bits(32) -> bool function f_is_pos_zero_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == zeros()) & (exp == zeros()) & (mant == zeros())) } val f_is_pos_subnorm_S : bits(32) -> bool function f_is_pos_subnorm_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == zeros()) & (exp == zeros()) & (mant != zeros())) } val f_is_pos_norm_S : bits(32) -> bool function f_is_pos_norm_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == zeros()) & (exp != zeros()) & (exp != ones())) } val f_is_pos_inf_S : bits(32) -> bool function f_is_pos_inf_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (sign == zeros()) & (exp == ones()) & (mant == zeros())) } val f_is_SNaN_S : bits(32) -> bool function f_is_SNaN_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (exp == ones()) & (mant [22] == bitzero) & (mant != zeros())) } val f_is_QNaN_S : bits(32) -> bool function f_is_QNaN_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (exp == ones()) & (mant [22] == bitone)) } /* Either QNaN or SNan */ val f_is_NaN_S : bits(32) -> bool function f_is_NaN_S x32 = { let (sign, exp, mant) = fsplit_S (x32); ( (exp == ones()) & (mant != zeros())) } /* **************************************************************** */ /* Help functions used in the semantic functions */ val negate_S : bits(32) -> bits(32) function negate_S (x32) = { let (sign, exp, mant) = fsplit_S (x32); let new_sign = if (sign == 0b0) then 0b1 else 0b0; fmake_S (new_sign, exp, mant) } val feq_quiet_S : (bits(32), bits (32)) -> (bool, bits(5)) function feq_quiet_S (v1, v2) = { let (s1, e1, m1) = fsplit_S (v1); let (s2, e2, m2) = fsplit_S (v2); let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1); let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2); let result = ((v1 == v2) | (v1Is0 & v2Is0)); let fflags = if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then nvFlag() else zeros(); (result, fflags) } val flt_S : (bits(32), bits (32), bool) -> (bool, bits(5)) function flt_S (v1, v2, is_quiet) = { let (s1, e1, m1) = fsplit_S (v1); let (s2, e2, m2) = fsplit_S (v2); let result : bool = if (s1 == 0b0) & (s2 == 0b0) then if (e1 == e2) then unsigned (m1) < unsigned (m2) else unsigned (e1) < unsigned (e2) else if (s1 == 0b0) & (s2 == 0b1) then false else if (s1 == 0b1) & (s2 == 0b0) then true else if (e1 == e2) then unsigned (m1) > unsigned (m2) else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then nvFlag() else zeros() else if (f_is_NaN_S(v1) | f_is_NaN_S(v2)) then nvFlag() else zeros(); (result, fflags) } val fle_S : (bits(32), bits (32), bool) -> (bool, bits(5)) function fle_S (v1, v2, is_quiet) = { let (s1, e1, m1) = fsplit_S (v1); let (s2, e2, m2) = fsplit_S (v2); let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1); let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2); let result : bool = if (s1 == 0b0) & (s2 == 0b0) then if (e1 == e2) then unsigned (m1) <= unsigned (m2) else unsigned (e1) < unsigned (e2) else if (s1 == 0b0) & (s2 == 0b1) then (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ else if (s1 == 0b1) & (s2 == 0b0) then true else if (e1 == e2) then unsigned (m1) >= unsigned (m2) else unsigned (e1) > unsigned (e2); let fflags = if is_quiet then if (f_is_SNaN_S(v1) | f_is_SNaN_S(v2)) then nvFlag() else zeros() else if (f_is_NaN_S(v1) | f_is_NaN_S(v2)) then nvFlag() else zeros(); (result, fflags) } /* **************************************************************** */ /* Helper functions for 'encdec()' */ function haveSingleFPU() -> bool = haveFExt() | haveZfinx() /* ****************************************************************** */ /* Floating-point loads */ /* AST */ /* FLH, FLW and FLD; H/W/D is encoded in 'word_width' */ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width) /* AST <-> Binary encoding ================================ */ mapping clause encdec = LOAD_FP(imm, rs1, rd, HALF) if haveZfh() <-> imm @ rs1 @ 0b001 @ rd @ 0b000_0111 if haveZfh() mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if haveFExt() <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if haveFExt() mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt() <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if haveDExt() /* Execution semantics ================================ */ val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) -> Retired function process_fload64(rd, addr, value) = if sizeof(flen) == 64 then match value { MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } else { /* should not get here */ RETIRE_FAIL } val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32))) -> Retired function process_fload32(rd, addr, value) = match value { MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16))) -> Retired function process_fload16(rd, addr, value) = match value { MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } function clause execute(LOAD_FP(imm, rs1, rd, width)) = { let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), width) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { let (aq, rl, res) = (false, false, false); match (width) { BYTE => { handle_illegal(); RETIRE_FAIL }, HALF => process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)), WORD => process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), DOUBLE if sizeof(flen) >= 64 => process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"), } } } } } /* AST -> Assembly notation ================================ */ mapping clause assembly = LOAD_FP(imm, rs1, rd, width) <-> "fl" ^ size_mnemonic(width) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" /* ****************************************************************** */ /* Floating-point stores */ /* AST */ /* FSH, FSW and FSD; H/W/D is encoded in 'word_width' */ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width) /* AST <-> Binary encoding ================================ */ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, HALF) if haveZfh() <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b001 @ imm5 : bits(5) @ 0b010_0111 if haveZfh() mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if haveFExt() <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if haveFExt() 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() /* Execution semantics ================================ */ val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired function process_fstore(vaddr, value) = match value { MemValue(true) => { RETIRE_SUCCESS }, MemValue(false) => { internal_error(__FILE__, __LINE__, "store got false from mem_write_value") }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } } function clause execute (STORE_FP(imm, rs2, rs1, width)) = { let offset : xlenbits = sign_extend(imm); let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Write(Data), width) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { let eares : MemoryOpResult(unit) = match width { BYTE => MemValue () /* bogus placeholder for illegal size */, HALF => mem_write_ea(addr, 2, aq, rl, false), WORD => mem_write_ea(addr, 4, aq, rl, false), DOUBLE => mem_write_ea(addr, 8, aq, rl, false) }; match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = F(rs2); match (width) { BYTE => { handle_illegal(); RETIRE_FAIL }, HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), DOUBLE if sizeof(flen) >= 64 => process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"), }; } } } } } } /* AST -> Assembly notation ================================ */ mapping clause assembly = STORE_FP(imm, rs2, rs1, width) <-> "fs" ^ size_mnemonic(width) ^ spc() ^ freg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" /* ****************************************************************** */ /* Fused multiply-add */ /* AST */ union clause ast = F_MADD_TYPE_S : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_S) /* AST <-> Binary encoding ================================ */ mapping clause encdec = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMADD_S) if haveSingleFPU() <-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if haveSingleFPU() mapping clause encdec = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMSUB_S) if haveSingleFPU() <-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if haveSingleFPU() mapping clause encdec = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMSUB_S) if haveSingleFPU() <-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if haveSingleFPU() mapping clause encdec = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMADD_S) if haveSingleFPU() <-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if haveSingleFPU() /* Execution semantics ================================ */ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = { let rs1_val_32b = F_or_X_S(rs1); let rs2_val_32b = F_or_X_S(rs2); let rs3_val_32b = F_or_X_S(rs3); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_32b) : (bits(5), bits(32)) = match op { FMADD_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, rs3_val_32b), FMSUB_S => riscv_f32MulAdd (rm_3b, rs1_val_32b, rs2_val_32b, negate_S (rs3_val_32b)), FNMSUB_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, rs3_val_32b), FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b)) }; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_32b; RETIRE_SUCCESS } } } /* AST -> Assembly notation ================================ */ mapping f_madd_type_mnemonic_S : f_madd_op_S <-> string = { FMADD_S <-> "fmadd.s", FMSUB_S <-> "fmsub.s", FNMSUB_S <-> "fnmsub.s", FNMADD_S <-> "fnmadd.s" } mapping clause assembly = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op) <-> f_madd_type_mnemonic_S(op) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) ^ sep() ^ freg_or_reg_name(rs3) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ /* Binary ops with rounding mode */ /* AST */ union clause ast = F_BIN_RM_TYPE_S : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_S) /* AST <-> Binary encoding ================================ */ mapping clause encdec = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FADD_S) if haveSingleFPU() <-> 0b000_0000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FSUB_S) if haveSingleFPU() <-> 0b000_0100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FMUL_S) if haveSingleFPU() <-> 0b000_1000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FDIV_S) if haveSingleFPU() <-> 0b000_1100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = { let rs1_val_32b = F_or_X_S(rs1); let rs2_val_32b = F_or_X_S(rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_32b) : (bits(5), bits(32)) = match op { FADD_S => riscv_f32Add (rm_3b, rs1_val_32b, rs2_val_32b), FSUB_S => riscv_f32Sub (rm_3b, rs1_val_32b, rs2_val_32b), FMUL_S => riscv_f32Mul (rm_3b, rs1_val_32b, rs2_val_32b), FDIV_S => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b) }; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_32b; RETIRE_SUCCESS } } } /* AST -> Assembly notation ================================ */ mapping f_bin_rm_type_mnemonic_S : f_bin_rm_op_S <-> string = { FADD_S <-> "fadd.s", FSUB_S <-> "fsub.s", FMUL_S <-> "fmul.s", FDIV_S <-> "fdiv.s" } mapping clause assembly = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op) <-> f_bin_rm_type_mnemonic_S(op) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ /* Unary with rounding mode */ /* AST */ union clause ast = F_UN_RM_TYPE_S : (regidx, rounding_mode, regidx, f_un_rm_op_S) /* AST <-> Binary encoding ================================ */ mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S) if haveSingleFPU() <-> 0b010_1100 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S) if haveSingleFPU() <-> 0b110_0000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S) if haveSingleFPU() <-> 0b110_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W) if haveSingleFPU() <-> 0b110_1000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU) if haveSingleFPU() <-> 0b110_1000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() /* F instructions, RV64 only */ mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) if haveSingleFPU() & sizeof(xlen) >= 64 <-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) if haveSingleFPU() & sizeof(xlen) >= 64 <-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) if haveSingleFPU() & sizeof(xlen) >= 64 <-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 mapping clause encdec = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) if haveSingleFPU() & sizeof(xlen) >= 64 <-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 /* Execution semantics ================================ */ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_f32Sqrt (rm_3b, rs1_val_S); accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_W) = riscv_f32ToI32 (rm_3b, rs1_val_S); accrue_fflags(fflags); X(rd) = sign_extend (rd_val_W); RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = { let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_WU) = riscv_f32ToUi32 (rm_3b, rs1_val_S); accrue_fflags(fflags); X(rd) = sign_extend (rd_val_WU); RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = { let rs1_val_W = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W); accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = { let rs1_val_WU = X(rs1) [31..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU); accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = { assert(sizeof(xlen) >= 64); let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_L) = riscv_f32ToI64 (rm_3b, rs1_val_S); accrue_fflags(fflags); X(rd) = sign_extend(rd_val_L); RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = { assert(sizeof(xlen) >= 64); let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_LU) = riscv_f32ToUi64 (rm_3b, rs1_val_S); accrue_fflags(fflags); X(rd) = sign_extend(rd_val_LU); RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = { assert(sizeof(xlen) >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L); accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = { assert(sizeof(xlen) >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU); accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } } } /* AST -> Assembly notation ================================ */ mapping f_un_rm_type_mnemonic_S : f_un_rm_op_S <-> string = { FSQRT_S <-> "fsqrt.s", FCVT_W_S <-> "fcvt.w.s", FCVT_WU_S <-> "fcvt.wu.s", FCVT_S_W <-> "fcvt.s.w", FCVT_S_WU <-> "fcvt.s.wu", FCVT_L_S <-> "fcvt.l.s", FCVT_LU_S <-> "fcvt.lu.s", FCVT_S_L <-> "fcvt.s.l", FCVT_S_LU <-> "fcvt.s.lu" } mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S) <-> f_un_rm_type_mnemonic_S(FSQRT_S) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S) <-> f_un_rm_type_mnemonic_S(FCVT_W_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S) <-> f_un_rm_type_mnemonic_S(FCVT_WU_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W) <-> f_un_rm_type_mnemonic_S(FCVT_S_W) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU) <-> f_un_rm_type_mnemonic_S(FCVT_S_WU) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) <-> f_un_rm_type_mnemonic_S(FCVT_L_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) <-> f_un_rm_type_mnemonic_S(FCVT_LU_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) <-> f_un_rm_type_mnemonic_S(FCVT_S_L) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) <-> f_un_rm_type_mnemonic_S(FCVT_S_LU) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ /* Binary, no rounding mode */ /* AST */ union clause ast = F_BIN_TYPE_S : (regidx, regidx, regidx, f_bin_op_S) /* AST <-> Binary encoding ================================ */ mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S) if haveSingleFPU() <-> 0b001_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S) if haveSingleFPU() <-> 0b001_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S) if haveSingleFPU() <-> 0b001_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S) if haveSingleFPU() <-> 0b001_0100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S) if haveSingleFPU() <-> 0b001_0100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S) if haveSingleFPU() <-> 0b101_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S) if haveSingleFPU() <-> 0b101_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if haveSingleFPU() <-> 0b101_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveSingleFPU() /* Execution semantics ================================ */ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let (s1, e1, m1) = fsplit_S (rs1_val_S); let (s2, e2, m2) = fsplit_S (rs2_val_S); let rd_val_S = fmake_S (s2, e1, m1); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let (s1, e1, m1) = fsplit_S (rs1_val_S); let (s2, e2, m2) = fsplit_S (rs2_val_S); let rd_val_S = fmake_S (0b1 ^ s2, e1, m1); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let (s1, e1, m1) = fsplit_S (rs1_val_S); let (s2, e2, m2) = fsplit_S (rs2_val_S); let rd_val_S = fmake_S (s1 ^ s2, e1, m1); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() else if f_is_NaN_S(rs1_val_S) then rs2_val_S else if f_is_NaN_S(rs2_val_S) then rs1_val_S else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S else if rs1_lt_rs2 then rs1_val_S else /* (not rs1_lt_rs2) */ rs2_val_S; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); let rd_val_S = if (f_is_NaN_S(rs1_val_S) & f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() else if f_is_NaN_S(rs1_val_S) then rs2_val_S else if f_is_NaN_S(rs2_val_S) then rs1_val_S else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S else if rs2_lt_rs1 then rs1_val_S else /* (not rs2_lt_rs1) */ rs2_val_S; accrue_fflags(fflags); F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Eq (rs1_val_S, rs2_val_S); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Lt (rs1_val_S, rs2_val_S); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = { let rs1_val_S = F_or_X_S(rs1); let rs2_val_S = F_or_X_S(rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Le (rs1_val_S, rs2_val_S); accrue_fflags(fflags); X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } /* AST -> Assembly notation ================================ */ mapping f_bin_type_mnemonic_S : f_bin_op_S <-> string = { FSGNJ_S <-> "fsgnj.s", FSGNJN_S <-> "fsgnjn.s", FSGNJX_S <-> "fsgnjx.s", FMIN_S <-> "fmin.s", FMAX_S <-> "fmax.s", FEQ_S <-> "feq.s", FLT_S <-> "flt.s", FLE_S <-> "fle.s" } mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S) <-> f_bin_type_mnemonic_S(FSGNJ_S) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S) <-> f_bin_type_mnemonic_S(FSGNJN_S) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S) <-> f_bin_type_mnemonic_S(FSGNJX_S) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S) <-> f_bin_type_mnemonic_S(FMIN_S) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S) <-> f_bin_type_mnemonic_S(FMAX_S) ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S) <-> f_bin_type_mnemonic_S(FEQ_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S) <-> f_bin_type_mnemonic_S(FLT_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) <-> f_bin_type_mnemonic_S(FLE_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ freg_or_reg_name(rs2) /* ****************************************************************** */ /* Unary, no rounding mode */ union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S) /* AST <-> Binary encoding ================================ */ mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S) if haveSingleFPU() <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU() mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W) if haveFExt() <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if haveFExt() <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() /* Execution semantics ================================ */ function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = { let rs1_val_S = F_or_X_S(rs1); let rd_val_10b : bits (10) = if f_is_neg_inf_S (rs1_val_S) then 0b_00_0000_0001 else if f_is_neg_norm_S (rs1_val_S) then 0b_00_0000_0010 else if f_is_neg_subnorm_S (rs1_val_S) then 0b_00_0000_0100 else if f_is_neg_zero_S (rs1_val_S) then 0b_00_0000_1000 else if f_is_pos_zero_S (rs1_val_S) then 0b_00_0001_0000 else if f_is_pos_subnorm_S (rs1_val_S) then 0b_00_0010_0000 else if f_is_pos_norm_S (rs1_val_S) then 0b_00_0100_0000 else if f_is_pos_inf_S (rs1_val_S) then 0b_00_1000_0000 else if f_is_SNaN_S (rs1_val_S) then 0b_01_0000_0000 else if f_is_QNaN_S (rs1_val_S) then 0b_10_0000_0000 else zeros(); X(rd) = zero_extend (rd_val_10b); RETIRE_SUCCESS } function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = { let rs1_val_S = F(rs1)[31..0]; let rd_val_X : xlenbits = sign_extend(rs1_val_S); X(rd) = rd_val_X; RETIRE_SUCCESS } function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = { let rs1_val_X = X(rs1); let rd_val_S = rs1_val_X [31..0]; F(rd) = nan_box (rd_val_S); RETIRE_SUCCESS } /* AST -> Assembly notation ================================ */ mapping f_un_type_mnemonic_S : f_un_op_S <-> string = { FMV_X_W <-> "fmv.x.w", FCLASS_S <-> "fclass.s", FMV_W_X <-> "fmv.w.x" } mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_X_W) <-> f_un_type_mnemonic_S(FMV_X_W) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_name(rs1) mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_W_X) <-> f_un_type_mnemonic_S(FMV_W_X) ^ spc() ^ freg_name(rd) ^ sep() ^ reg_name(rs1) mapping clause assembly = F_UN_TYPE_S(rs1, rd, FCLASS_S) <-> f_un_type_mnemonic_S(FCLASS_S) ^ spc() ^ reg_name(rd) ^ sep() ^ freg_or_reg_name(rs1) /* ****************************************************************** */