From 085cfcd3fc3be92aaa86b4caabf9d248eae5f83e Mon Sep 17 00:00:00 2001 From: Jessica Clarke Date: Mon, 22 Nov 2021 18:02:40 +0000 Subject: Implement support for Zfinx (#130) NB: Smstateen support is missing in the model so enabling the Zfinx extension provides an architectural covert channel via FCSR if privileged software is not aware of Zfinx's existence. Co-authored-by: Jessica Clarke Co-authored-by: Ibrahim Abu Kharmeh --- model/riscv_insts_dext.sail | 313 +++++++++++++++++++++++--------------------- 1 file changed, 163 insertions(+), 150 deletions(-) (limited to 'model/riscv_insts_dext.sail') diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index ea6f280..ebd6eae 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -98,10 +98,6 @@ function fsplit_D x64 = (x64[63..63], x64[62..52], x64[51..0]) val fmake_D : (bits(1), bits(11), bits(52)) -> bits(64) function fmake_D (sign, exp, mant) = sign @ exp @ mant -/* ---- Canonical NaNs */ - -function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000 - /* ---- Structure tests */ val f_is_neg_inf_D : bits(64) -> bool @@ -284,6 +280,21 @@ function fle_D (v1, v2, is_quiet) = { (result, fflags) } +/* **************************************************************** */ +/* Helper functions for 'encdec()' */ + +function haveDoubleFPU() -> bool = haveDExt() | haveZdinx() + +/* RV32Zdinx requires even register pairs; can be omitted for code */ +/* not used for RV32Zdinx (i.e. RV64-only or D-only). */ +val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, dec, regidx)) -> bool +function validDoubleRegs(n, regs) = { + if haveZdinx() & sizeof(xlen) == 32 then + foreach (i from 0 to (n - 1)) + if (regs[i][0] == bitone) then return false; + true +} + /* ****************************************************************** */ /* Floating-point loads */ /* These are defined in: riscv_insts_fext.sail */ @@ -302,27 +313,28 @@ union clause ast = F_MADD_TYPE_D : (regidx, regidx, regidx, rounding_mode, regid /* AST <-> Binary encoding ================================ */ mapping clause encdec = - F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D) if is_RV32D_or_RV64D() -<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if is_RV32D_or_RV64D() + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) mapping clause encdec = - F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D) if is_RV32D_or_RV64D() -<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if is_RV32D_or_RV64D() + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) mapping clause encdec = - F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D) if is_RV32D_or_RV64D() -<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if is_RV32D_or_RV64D() + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) mapping clause encdec = - F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D) if is_RV32D_or_RV64D() -<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if is_RV32D_or_RV64D() + F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd]) /* Execution semantics ================================ */ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { - let rs1_val_64b = F(rs1); - let rs2_val_64b = F(rs2); - let rs3_val_64b = F(rs3); + let rs1_val_64b = F_or_X_D(rs1); + let rs2_val_64b = F_or_X_D(rs2); + let rs3_val_64b = F_or_X_D(rs3); + match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -335,7 +347,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b)) }; write_fflags(fflags); - F(rd) = rd_val_64b; + F_or_X_D(rd) = rd_val_64b; RETIRE_SUCCESS } } @@ -352,10 +364,10 @@ mapping f_madd_type_mnemonic_D : f_madd_op_D <-> string = { mapping clause assembly = F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op) <-> f_madd_type_mnemonic_D(op) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) - ^ sep() ^ freg_name(rs3) + ^ 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) /* ****************************************************************** */ @@ -368,26 +380,26 @@ union clause ast = F_BIN_RM_TYPE_D : (regidx, regidx, rounding_mode, regidx, f_b /* AST <-> Binary encoding ================================ */ mapping clause encdec = - F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D) if is_RV32D_or_RV64D() -<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) +<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) mapping clause encdec = - F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D) if is_RV32D_or_RV64D() -<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) +<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) mapping clause encdec = - F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D) if is_RV32D_or_RV64D() -<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) +<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) mapping clause encdec = - F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D) if is_RV32D_or_RV64D() -<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) +<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = { - let rs1_val_64b = F(rs1); - let rs2_val_64b = F(rs2); + let rs1_val_64b = F_or_X_D(rs1); + let rs2_val_64b = F_or_X_D(rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -399,7 +411,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = { FDIV_D => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b) }; write_fflags(fflags); - F(rd) = rd_val_64b; + F_or_X_D(rd) = rd_val_64b; RETIRE_SUCCESS } } @@ -416,9 +428,9 @@ mapping f_bin_rm_type_mnemonic_D : f_bin_rm_op_D <-> string = { mapping clause assembly = F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op) <-> f_bin_rm_type_mnemonic_D(op) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -431,55 +443,55 @@ union clause ast = F_UN_RM_TYPE_D : (regidx, rounding_mode, regidx, f_un_rm_op_D /* AST <-> Binary encoding ================================ */ mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) if is_RV32D_or_RV64D() -<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) if haveDoubleFPU() & validDoubleRegs([rs1, rd]) +<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1, rd]) mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) if is_RV32D_or_RV64D() -<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) if haveDoubleFPU() & validDoubleRegs([rs1]) +<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1]) mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) if is_RV32D_or_RV64D() -<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) if haveDoubleFPU() & validDoubleRegs([rs1]) +<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1]) mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) if is_RV32D_or_RV64D() -<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) if haveDoubleFPU() & validDoubleRegs([rd]) +<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rd]) mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) if is_RV32D_or_RV64D() -<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) if haveDoubleFPU() & validDoubleRegs([rd]) +<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rd]) mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) if is_RV32D_or_RV64D() -<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) if haveDoubleFPU() & validDoubleRegs([rs1]) +<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1]) mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) if is_RV32D_or_RV64D() -<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) if haveDoubleFPU() & validDoubleRegs([rd]) +<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rd]) /* D instructions, RV64 only */ mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if is_RV64D() -<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if haveDoubleFPU() & sizeof(xlen) >= 64 +<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if is_RV64D() -<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if haveDoubleFPU() & sizeof(xlen) >= 64 +<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if is_RV64D() -<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if haveDoubleFPU() & sizeof(xlen) >= 64 +<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if is_RV64D() -<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D() + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if haveDoubleFPU() & sizeof(xlen) >= 64 +<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 /* Execution semantics ================================ */ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -487,14 +499,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { let (fflags, rd_val_D) = riscv_f64Sqrt (rm_3b, rs1_val_D); write_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -509,7 +521,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -532,7 +544,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = { let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W); write_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -547,14 +559,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = { let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU); write_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -562,14 +574,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D); write_fflags(fflags); - F(rd) = nan_box (rd_val_S); + F_or_X_S(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { - let rs1_val_S = nan_unbox (F(rs1)); + let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -577,7 +589,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S); write_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -585,7 +597,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { assert(sizeof(xlen) >= 64); - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -601,7 +613,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { assert(sizeof(xlen) >= 64); - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -625,7 +637,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = { let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L); write_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -641,7 +653,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = { let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU); write_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -667,68 +679,68 @@ mapping f_un_rm_type_mnemonic_D : f_un_rm_op_D <-> string = { mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) <-> f_un_rm_type_mnemonic_D(FSQRT_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) <-> f_un_rm_type_mnemonic_D(FCVT_W_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) <-> f_un_rm_type_mnemonic_D(FCVT_WU_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) <-> f_un_rm_type_mnemonic_D(FCVT_D_W) - ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) <-> f_un_rm_type_mnemonic_D(FCVT_D_WU) - ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) <-> f_un_rm_type_mnemonic_D(FCVT_L_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) <-> f_un_rm_type_mnemonic_D(FCVT_LU_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) <-> f_un_rm_type_mnemonic_D(FCVT_D_L) - ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) <-> f_un_rm_type_mnemonic_D(FCVT_D_LU) - ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_or_reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) <-> f_un_rm_type_mnemonic_D(FCVT_S_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) <-> f_un_rm_type_mnemonic_D(FCVT_D_S) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -740,68 +752,69 @@ union clause ast = F_BIN_TYPE_D : (regidx, regidx, regidx, f_bin_op_D) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) if is_RV32D_or_RV64D() - <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) + <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) if is_RV32D_or_RV64D() - <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) + <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) if is_RV32D_or_RV64D() - <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) + <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) if is_RV32D_or_RV64D() - <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) + <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) if is_RV32D_or_RV64D() - <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) + <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if is_RV32D_or_RV64D() - <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1]) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if is_RV32D_or_RV64D() - <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1]) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1]) -mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if is_RV32D_or_RV64D() - <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1]) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1]) /* Execution semantics ================================ */ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); + let (s1, e1, m1) = fsplit_D (rs1_val_D); let (s2, e2, m2) = fsplit_D (rs2_val_D); let rd_val_D = fmake_D (s2, e1, m1); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let (s1, e1, m1) = fsplit_D (rs1_val_D); let (s2, e2, m2) = fsplit_D (rs2_val_D); let rd_val_D = fmake_D (0b1 ^ s2, e1, m1); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let (s1, e1, m1) = fsplit_D (rs1_val_D); let (s2, e2, m2) = fsplit_D (rs2_val_D); let rd_val_D = fmake_D (s1 ^ s2, e1, m1); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); @@ -815,13 +828,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { else /* (not rs1_lt_rs2) */ rs2_val_D; accrue_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); @@ -835,13 +848,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { else /* (not rs2_lt_rs1) */ rs2_val_D; accrue_fflags(fflags); - F(rd) = rd_val_D; + F_or_X_D(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Eq (rs1_val_D, rs2_val_D); @@ -852,8 +865,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Lt (rs1_val_D, rs2_val_D); @@ -864,8 +877,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = { - let rs1_val_D = F(rs1); - let rs2_val_D = F(rs2); + let rs1_val_D = F_or_X_D(rs1); + let rs2_val_D = F_or_X_D(rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Le (rs1_val_D, rs2_val_D); @@ -890,51 +903,51 @@ mapping f_bin_type_mnemonic_D : f_bin_op_D <-> string = { mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) <-> f_bin_type_mnemonic_D(FSGNJ_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) <-> f_bin_type_mnemonic_D(FSGNJN_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) <-> f_bin_type_mnemonic_D(FSGNJX_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) <-> f_bin_type_mnemonic_D(FMIN_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) <-> f_bin_type_mnemonic_D(FMAX_D) - ^ spc() ^ freg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) <-> f_bin_type_mnemonic_D(FEQ_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) <-> f_bin_type_mnemonic_D(FLT_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) <-> f_bin_type_mnemonic_D(FLE_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) - ^ sep() ^ freg_name(rs2) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) /* ****************************************************************** */ /* Unary, no rounding mode */ @@ -943,21 +956,21 @@ union clause ast = F_UN_TYPE_D : (regidx, regidx, f_un_op_D) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if haveDExt() - <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDExt() +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if haveDoubleFPU() & validDoubleRegs([rs1]) + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1]) /* D instructions, RV64 only */ -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if is_RV64D() - <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if haveDExt() + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if is_RV64D() - <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if haveDExt() + <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() /* Execution semantics ================================ */ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = F_or_X_D(rs1); let rd_val_10b : bits (10) = if f_is_neg_inf_D (rs1_val_D) then 0b_00_0000_0001 @@ -1013,6 +1026,6 @@ mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_D_X) mapping clause assembly = F_UN_TYPE_D(rs1, rd, FCLASS_D) <-> f_un_type_mnemonic_D(FCLASS_D) ^ spc() ^ reg_name(rd) - ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs1) /* ****************************************************************** */ -- cgit v1.1