aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_insts_dext.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_insts_dext.sail')
-rw-r--r--model/riscv_insts_dext.sail313
1 files changed, 163 insertions, 150 deletions
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)
/* ****************************************************************** */
generated by cgit v1.1 at 2024-11-16 16:08:31 +0000