Skip to content

Instantly share code, notes, and snippets.

@jrtc27

jrtc27/interdiff.diff

Created November 22, 2021 00:36
Show Gist options
  • Save jrtc27/c26d373d866a6fac78ec69bc43f6c31f to your computer and use it in GitHub Desktop.
Save jrtc27/c26d373d866a6fac78ec69bc43f6c31f to your computer and use it in GitHub Desktop.
Download ZIP
Zfinx interdiff
Raw
interdiff.diff
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index c4a13f4..a2d1bce 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -330,6 +330,7 @@ char *process_args(int argc, char **argv)
case 'x':
fprintf(stderr, "enabling Zfinx support.\n");
rv_enable_zfinx = true;
+ rv_enable_fdext = false;
break;
#ifdef SAILCOV
case 'c':
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 87211ea..31872d3 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -186,5 +186,5 @@ val ext_read_CSR : csreg -> option(xlenbits) effect {rreg}
scattered function ext_read_CSR
/* returns new value (after legalisation) if the CSR is defined */
-val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg}
+val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg, escape}
scattered function ext_write_CSR
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index 4180a72..4f48b3e 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -83,30 +83,23 @@
function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
-val nan_unbox_do : (bool, bits(64)) -> bits(32)
-function nan_unbox_do (zfinx_en, regval) =
- if zfinx_en
- then regval [31..0]
- else if regval [63..32] == 0x_FFFF_FFFF
- then regval [31..0]
- else canonical_NaN_S()
-
-val nan_unbox_pass : (bool, bits(32)) -> bits(32)
-function nan_unbox_pass (zfinx_en, regval) =
- regval
-
-val nan_box_do : (bool, bits(32)) -> bits(64)
-function nan_box_do (zfinx_en, regval) =
- 0x_FFFF_FFFF @ regval
-
-
-val nan_box_pass : (bool, bits(32)) -> bits(32)
-function nan_box_pass (zfinx_en, regval) =
- regval
-
-overload nan_unbox = { nan_unbox_do, nan_unbox_pass }
-overload nan_box = { nan_box_do, nan_box_pass }
+val nan_box : bits(32) -> flenbits effect {escape}
+function nan_box val_32b = {
+ assert(sys_enable_fdext());
+ if (sizeof(flen) == 32)
+ then val_32b
+ else 0x_FFFF_FFFF @ val_32b
+}
+val nan_unbox : flenbits -> bits(32) effect {escape}
+function nan_unbox regval = {
+ assert(sys_enable_fdext());
+ if (sizeof(flen) == 32)
+ then regval
+ else if regval [63..32] == 0x_FFFF_FFFF
+ then regval [31..0]
+ else canonical_NaN_S()
+}
/* **************************************************************** */
/* Floating point register file */
@@ -145,12 +138,19 @@ register f30 : fregtype
register f31 : fregtype
function dirty_fd_context() -> unit = {
+ assert(sys_enable_fdext());
mstatus->FS() = extStatus_to_bits(Dirty);
mstatus->SD() = 0b1
}
+function dirty_fd_context_if_present() -> unit = {
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext() then dirty_fd_context()
+}
+
val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape}
function rF r = {
+ assert(sys_enable_fdext());
let v : fregtype =
match r {
0 => f0,
@@ -192,6 +192,7 @@ function rF r = {
val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape}
function wF (r, in_v) = {
+ assert(sys_enable_fdext());
let v = fregval_into_freg(in_v);
match r {
0 => f0 = v,
@@ -245,57 +246,57 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
overload F = {rF_bits, wF_bits, rF, wF}
-/* ---- Register Read/ Writes */
-
-val rX_or_F_32 : (bool, bits(5)) -> bits(32) effect {escape, rreg}
-function rX_or_F_32(zfinx_en, i) = {
- if zfinx_en then
- nan_unbox(zfinx_en, rX(unsigned(i)))
- else
- nan_unbox(zfinx_en, rF(unsigned(i)))
+val rF_or_X_S : bits(5) -> bits(32) effect {escape, rreg}
+function rF_or_X_S(i) = {
+ assert(sizeof(flen) >= 32);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then nan_unbox(F(i))
+ else X(i)[31..0]
}
-val rX_or_F_64 : (bool, bits(5)) -> bits(64) effect {escape, rreg}
-function rX_or_F_64(zfinx_en, i) = {
- assert (zfinx_en | sizeof(flen) == 64);
- if zfinx_en & sizeof (xlen) == 32 then {
- assert (i[0] == bitzero);
- if i == 0b00000 then
- sail_zeros(64)
- else rX(unsigned(i+1)) @ rX(unsigned(i))
+val rF_or_X_D : bits(5) -> bits(64) effect {escape, rreg}
+function rF_or_X_D(i) = {
+ assert(sizeof(flen) >= 64);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then F(unsigned(i))
+ else if sizeof(xlen) >= 64
+ then X(i)[63..0]
+ else {
+ assert(i[0] == bitzero);
+ if i == zeros() then zeros() else X(i + 1) @ X(i)
}
- else if zfinx_en & sizeof(xlen) == 64 then
- rX(unsigned(i))
- else
- rF(unsigned(i))
}
-val wX_or_F_64 : (bool, bits(5), bits(64)) -> unit effect {escape, wreg}
-function wX_or_F_64(zfinx_en: bool, i: bits(5), data: bits(64)) = {
- assert (zfinx_en | sizeof(flen) == 64);
- if zfinx_en & sizeof(xlen) == 32 then {
+val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
+function wF_or_X_S(i, data) = {
+ assert(sizeof(flen) >= 32);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then F(i) = nan_box(data)
+ else X(i) = EXTS(data)
+}
+
+val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
+function wF_or_X_D(i, data) = {
+ assert (sizeof(flen) >= 64);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then F(i) = data
+ else if sizeof(xlen) >= 64
+ then X(i) = EXTS(data)
+ else {
assert (i[0] == bitzero);
- if i != 0b00000 then {
- wX(unsigned(i)) = data[31..0];
- wX(unsigned(i+1)) = data[63..32];
+ if i != zeros() then {
+ X(i) = data[31..0];
+ X(i + 1) = data[63..32];
}
}
- else if zfinx_en & sizeof (xlen) == 64 then
- wX(unsigned(i)) = data
- else if ~ (zfinx_en) & sizeof (flen) == 64 then
- wF(unsigned(i)) = data
-}
-
-val wX_or_F_32 : (bool, bits(5), bits(32)) -> unit effect {escape, wreg}
-function wX_or_F_32(zfinx_en: bool, i: bits(5), data : bits(32)) = {
- if zfinx_en then
- wX(unsigned(i)) = nan_box(zfinx_en, data)
- else
- wF(unsigned(i)) = nan_box(zfinx_en, data)
}
-overload X_or_F_S = { rX_or_F_32, wX_or_F_32 }
-overload X_or_F_D = { rX_or_F_64, wX_or_F_64 }
+overload F_or_X_S = { rF_or_X_S, wF_or_X_S }
+overload F_or_X_D = { rF_or_X_D, wF_or_X_D }
/* register names */
@@ -376,10 +377,10 @@ mapping freg_name = {
0b11111 <-> "ft11"
}
-val reg_or_freg_name : bits(5) <-> string
-mapping reg_or_freg_name = {
- reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx(),
- reg if ~ (sys_enable_zfinx()) <-> freg_name(reg) if ~ (sys_enable_zfinx())
+val freg_or_reg_name : bits(5) <-> string
+mapping freg_or_reg_name = {
+ reg if sys_enable_fdext() <-> freg_name(reg) if sys_enable_fdext(),
+ reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx()
}
val init_fdext_regs : unit -> unit effect {wreg}
@@ -432,30 +433,30 @@ bitfield Fcsr : bits(32) = {
register fcsr : Fcsr
-val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg}
+val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg, escape}
function ext_write_fcsr (frm, fflags) = {
fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */
fcsr->FFLAGS() = fflags;
update_softfloat_fflags(fflags);
- if ~ (sys_enable_zfinx()) then dirty_fd_context();
+ dirty_fd_context_if_present();
}
/* called for softfloat paths (softfloat flags are consistent) */
-val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
+val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
function write_fflags(fflags) = {
- if fcsr.FFLAGS() != fflags & ~ (sys_enable_zfinx())
- then dirty_fd_context();
+ if fcsr.FFLAGS() != fflags
+ then dirty_fd_context_if_present();
fcsr->FFLAGS() = fflags;
}
/* called for non-softfloat paths (softfloat flags need updating) */
-val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg}
+val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
function accrue_fflags(flags) = {
let f = fcsr.FFLAGS() | flags;
if fcsr.FFLAGS() != f
then {
fcsr->FFLAGS() = f;
update_softfloat_fflags(f);
- if ~ (sys_enable_zfinx()) then dirty_fd_context();
+ dirty_fd_context_if_present();
}
}
diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail
index 0c6bbd1..77a6302 100644
--- a/model/riscv_insts_cdext.sail
+++ b/model/riscv_insts_cdext.sail
@@ -77,9 +77,9 @@
union clause ast = C_FLDSP : (bits(6), regidx)
mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
<-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
function clause execute (C_FLDSP(uimm, rd)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -95,9 +95,9 @@ mapping clause assembly = C_FLDSP(uimm, rd)
union clause ast = C_FSDSP : (bits(6), regidx)
mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
<-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
function clause execute (C_FSDSP(uimm, rs2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -113,9 +113,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2)
union clause ast = C_FLD : (bits(5), cregidx, cregidx)
mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
<-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
function clause execute (C_FLD(uimm, rsc, rdc)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -133,9 +133,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc)
union clause ast = C_FSD : (bits(5), cregidx, cregidx)
mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
<-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
- if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+ if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail
index 98eea24..9aa94ef 100644
--- a/model/riscv_insts_cfext.sail
+++ b/model/riscv_insts_cfext.sail
@@ -77,9 +77,9 @@
union clause ast = C_FLWSP : (bits(6), regidx)
mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd)
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
<-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
function clause execute (C_FLWSP(imm, rd)) = {
let imm : bits(12) = EXTZ(imm @ 0b00);
@@ -95,9 +95,9 @@ mapping clause assembly = C_FLWSP(imm, rd)
union clause ast = C_FSWSP : (bits(6), regidx)
mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2)
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
<-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
function clause execute (C_FSWSP(uimm, rs2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -113,9 +113,9 @@ mapping clause assembly = C_FSWSP(uimm, rd)
union clause ast = C_FLW : (bits(5), cregidx, cregidx)
mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd)
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
<-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
function clause execute (C_FLW(uimm, rsc, rdc)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -133,9 +133,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc)
union clause ast = C_FSW : (bits(5), cregidx, cregidx)
mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2)
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
<-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
- if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+ if sizeof(xlen) == 32 & haveRVC() & haveFExt()
function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 068bba6..ebd6eae 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -280,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 */
@@ -298,27 +313,27 @@ 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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if supports_RV32D_or_RV64D([rs3, rs2, rs1, rd])
+ 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_64b = X_or_F_D(sys_enable_zfinx(), rs2);
- let rs3_val_64b = X_or_F_D(sys_enable_zfinx(), 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 },
@@ -332,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);
- X_or_F_D(sys_enable_zfinx(), rd, rd_val_64b);
+ F_or_X_D(rd) = rd_val_64b;
RETIRE_SUCCESS
}
}
@@ -349,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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_freg_name(rs2)
- ^ sep() ^ reg_or_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)
/* ****************************************************************** */
@@ -365,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 supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs2, rs1, rd])
-<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+ 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)) = {
- rs1_val_64b = X_or_F_D(sys_enable_zfinx(), rs1);
- rs2_val_64b = X_or_F_D(sys_enable_zfinx(), 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') => {
@@ -396,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);
- X_or_F_D(sys_enable_zfinx(), rd, rd_val_64b);
+ F_or_X_D(rd) = rd_val_64b;
RETIRE_SUCCESS
}
}
@@ -413,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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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)
/* ****************************************************************** */
@@ -428,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 supports_RV32D_or_RV64D([rs1, rd])
-<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs1, rd])
+ 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 supports_RV32D_or_RV64D([rs1])
-<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs1])
+ 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 supports_RV32D_or_RV64D([rs1])
-<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs1])
+ 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 supports_RV32D_or_RV64D([rd])
-<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rd])
+ 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 supports_RV32D_or_RV64D([rd])
-<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rd])
+ 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 supports_RV32D_or_RV64D([rs1])
-<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs1])
+ 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 supports_RV32D_or_RV64D([rd])
-<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rd])
+ 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 = X_or_F_D(sys_enable_zfinx(), rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -484,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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -506,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 = X_or_F_D(sys_enable_zfinx(), rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -529,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);
- X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -544,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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -559,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);
- X_or_F_S(sys_enable_zfinx(), rd, 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)) = {
- rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -574,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);
- X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -582,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);
- rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -598,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 = X_or_F_D(sys_enable_zfinx(), rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -606,7 +621,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D);
write_fflags(fflags);
- X(rd) = rd_val_LU;
+ X(rd) = EXTS(rd_val_LU);
RETIRE_SUCCESS
}
}
@@ -622,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);
- X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -638,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);
- X_or_F_D(sys_enable_zfinx(), rd, rd_val_D);
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -664,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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
/* ****************************************************************** */
@@ -737,69 +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 supports_RV32D_or_RV64D([rs2, rs1, rd])
- <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+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 supports_RV32D_or_RV64D([rs2, rs1, rd])
- <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+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 supports_RV32D_or_RV64D([rs2, rs1, rd])
- <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+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 supports_RV32D_or_RV64D([rs2, rs1, rd])
- <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+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 supports_RV32D_or_RV64D([rs2, rs1, rd])
- <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1, rd])
+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 supports_RV32D_or_RV64D([rs2, rs1])
- <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1])
+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 supports_RV32D_or_RV64D([rs2, rs1])
- <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1])
+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 supports_RV32D_or_RV64D([rs2, rs1])
- <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs2, rs1])
+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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
@@ -813,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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
@@ -833,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);
- X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
@@ -850,11 +865,11 @@ 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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
+ riscv_f64Lt (rs1_val_D, rs2_val_D);
write_fflags(fflags);
X(rd) = EXTZ(bool_to_bits(rd_val));
@@ -862,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 = X_or_F_D(sys_enable_zfinx(), rs1);
- let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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);
@@ -888,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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
/* ****************************************************************** */
/* Unary, no rounding mode */
@@ -941,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 supports_RV32D_or_RV64D([rs1])
- <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rs1])
+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() & ~ (sys_enable_zfinx())
- <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() & ~ (sys_enable_zfinx())
+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() & ~ (sys_enable_zfinx())
- <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() & ~ (sys_enable_zfinx())
+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 = X_or_F_D(sys_enable_zfinx(), 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
@@ -1011,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() ^ reg_or_freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
/* ****************************************************************** */
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 8e42b01..2995f19 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -316,26 +316,10 @@ function fle_S (v1, v2, is_quiet) = {
}
/* **************************************************************** */
-/* Help-functions for 'encdec()' to restrict to certain */
-/* combinations of {F,D} x {RV32,RV64} */
+/* Helper functions for 'encdec()' */
-function is_RV32F_or_RV64F () -> bool = (haveFExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64))
-function is_RV64F () -> bool = (haveFExt() & sizeof(xlen) == 64)
+function haveSingleFPU() -> bool = haveFExt() | haveZfinx()
-function is_RV32D_or_RV64D () -> bool = (haveDExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64))
-function is_RV64D () -> bool = (haveDExt() & sizeof(xlen) == 64)
-
-val supports_RV32D_or_RV64D : forall 'n, 'n > 0. (implicit('n), vector('n, dec, bits(5))) -> bool effect {rreg}
-function supports_RV32D_or_RV64D (reg_vec_len, registers) = {
- if ~ (sys_enable_zfinx()) then is_RV32D_or_RV64D()
- else if sys_enable_zfinx() & is_RV64D() then true
- else {
- foreach (x from 0 to (reg_vec_len - 1) ) {
- if (registers[x][0] == bitone) then return false
- };
- true
- }
-}
/* ****************************************************************** */
/* Floating-point loads */
@@ -346,11 +330,11 @@ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
- <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
+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 is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
- <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
+mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt()
+ <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if haveDExt()
/* Execution semantics ================================ */
@@ -371,7 +355,7 @@ val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32)))
-> Retired effect {escape, rreg, wreg}
function process_fload32(rd, addr, value) =
match value {
- MemValue(result) => { F(rd) = nan_box(false, result); RETIRE_SUCCESS },
+ MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}
@@ -406,7 +390,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
mapping clause assembly = LOAD_FP(imm, rs1, rd, width)
<-> "fl" ^ size_mnemonic(width)
- ^ spc() ^ reg_or_freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ hex_bits_12(imm)
^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
@@ -420,11 +404,11 @@ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
- <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx())
+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 is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
- <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx())
+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 ================================ */
@@ -490,27 +474,27 @@ union clause ast = F_MADD_TYPE_S : (regidx, regidx, regidx, rounding_mode, regid
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMADD_S) if is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if is_RV32F_or_RV64F()
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_32b = X_or_F_S(sys_enable_zfinx(), rs2);
- let rs3_val_32b = X_or_F_S(sys_enable_zfinx(), rs3);
+ 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') => {
@@ -523,7 +507,7 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b))
};
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_32b);
+ F_or_X_S(rd) = rd_val_32b;
RETIRE_SUCCESS
}
}
@@ -540,10 +524,10 @@ mapping f_madd_type_mnemonic_S : f_madd_op_S <-> string = {
mapping clause assembly = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)
<-> f_madd_type_mnemonic_S(op)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_freg_name(rs2)
- ^ sep() ^ reg_or_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)
/* ****************************************************************** */
@@ -556,26 +540,26 @@ union clause ast = F_BIN_RM_TYPE_S : (regidx, regidx, rounding_mode, regidx, f_b
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FADD_S) if is_RV32F_or_RV64F()
-<-> 0b000_0000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b000_0100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b000_1000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b000_1100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_32b = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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') => {
@@ -587,7 +571,7 @@ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
FDIV_S => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b)
};
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_32b);
+ F_or_X_S(rd) = rd_val_32b;
RETIRE_SUCCESS
}
}
@@ -604,9 +588,9 @@ mapping f_bin_rm_type_mnemonic_S : f_bin_rm_op_S <-> string = {
mapping clause assembly = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)
<-> f_bin_rm_type_mnemonic_S(op)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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)
/* ****************************************************************** */
@@ -619,47 +603,47 @@ 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 is_RV32F_or_RV64F()
-<-> 0b010_1100 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b110_0000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b110_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b110_1000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV32F_or_RV64F()
-<-> 0b110_1000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ 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 is_RV64F()
-<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ 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 is_RV64F()
-<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ 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 is_RV64F()
-<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ 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 is_RV64F()
-<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -667,14 +651,14 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
let (fflags, rd_val_S) = riscv_f32Sqrt (rm_3b, rs1_val_S);
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -689,7 +673,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = {
}
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = {
- let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -712,7 +696,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = {
let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W);
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -727,7 +711,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU);
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -735,7 +719,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
assert(sizeof(xlen) >= 64);
- let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -751,7 +735,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = {
assert(sizeof(xlen) >= 64);
- let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -775,7 +759,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = {
let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L);
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -791,7 +775,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = {
let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU);
write_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -814,55 +798,55 @@ mapping f_un_rm_type_mnemonic_S : f_un_rm_op_S <-> string = {
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)
<-> f_un_rm_type_mnemonic_S(FSQRT_S)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_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_S(rs1, rm, rd, FCVT_W_S)
<-> f_un_rm_type_mnemonic_S(FCVT_W_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
+ ^ 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() ^ reg_or_freg_name(rs1)
+ ^ 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() ^ reg_or_freg_name(rd)
+ ^ 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() ^ reg_or_freg_name(rd)
+ ^ 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() ^ reg_or_freg_name(rs1)
+ ^ 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() ^ reg_or_freg_name(rs1)
+ ^ 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() ^ reg_or_freg_name(rd)
+ ^ 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() ^ reg_or_freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
@@ -876,68 +860,68 @@ 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 is_RV32F_or_RV64F()
- <-> 0b001_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b001_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b001_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b001_0100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b001_0100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b101_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b101_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 is_RV32F_or_RV64F()
- <-> 0b101_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
@@ -951,13 +935,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = {
else /* (not rs1_lt_rs2) */ rs2_val_S;
accrue_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
@@ -971,13 +955,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
else /* (not rs2_lt_rs1) */ rs2_val_S;
accrue_fflags(fflags);
- X_or_F_S(sys_enable_zfinx(), rd, rd_val_S);
+ 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 = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
@@ -988,8 +972,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
- let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
@@ -1000,8 +984,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
- let rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1);
- let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2);
+ 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);
@@ -1026,51 +1010,51 @@ mapping f_bin_type_mnemonic_S : f_bin_op_S <-> string = {
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)
<-> f_bin_type_mnemonic_S(FSGNJ_S)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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_S(rs2, rs1, rd, FSGNJN_S)
<-> f_bin_type_mnemonic_S(FSGNJN_S)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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_S(rs2, rs1, rd, FSGNJX_S)
<-> f_bin_type_mnemonic_S(FSGNJX_S)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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_S(rs2, rs1, rd, FMIN_S)
<-> f_bin_type_mnemonic_S(FMIN_S)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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_S(rs2, rs1, rd, FMAX_S)
<-> f_bin_type_mnemonic_S(FMAX_S)
- ^ spc() ^ reg_or_freg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_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_S(rs2, rs1, rd, FEQ_S)
<-> f_bin_type_mnemonic_S(FEQ_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_freg_name(rs2)
+ ^ 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() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_freg_name(rs2)
+ ^ 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() ^ reg_or_freg_name(rs1)
- ^ sep() ^ reg_or_freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
/* ****************************************************************** */
/* Unary, no rounding mode */
@@ -1079,19 +1063,19 @@ 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 haveFExt()
- <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveFExt()
+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() & ~ (sys_enable_zfinx())
- <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & ~ (sys_enable_zfinx())
+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() & ~ (sys_enable_zfinx())
- <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & ~ (sys_enable_zfinx())
+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 = X_or_F_S(sys_enable_zfinx(), rs1);
+ 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
@@ -1120,7 +1104,7 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = {
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(false, rd_val_S);
+ F(rd) = nan_box (rd_val_S);
RETIRE_SUCCESS
}
@@ -1145,6 +1129,6 @@ mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_W_X)
mapping clause assembly = F_UN_TYPE_S(rs1, rd, FCLASS_S)
<-> f_un_type_mnemonic_S(FCLASS_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ reg_or_freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
/* ****************************************************************** */
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 06be736..6204ae5 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -559,10 +559,13 @@ function init_sys() -> unit = {
misa->U() = 0b1; /* user-mode */
misa->S() = 0b1; /* supervisor-mode */
+ if sys_enable_fdext() & sys_enable_zfinx()
+ then internal_error("F and Zfinx cannot both be enabled!");
+
/* We currently support both F and D */
- misa->F() = bool_to_bits(sys_enable_fdext() & ~ (sys_enable_zfinx())); /* single-precision */
- misa->D() = if sizeof(flen) >= 64 & ~ (sys_enable_zfinx())
- then bool_to_bits(sys_enable_fdext()) /* double-precision */
+ misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */
+ misa->D() = if sizeof(flen) >= 64
+ then bool_to_bits(sys_enable_fdext()) /* double-precision */
else 0b0;
mstatus = set_mstatus_SXL(mstatus, misa.MXL());
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 28505e3..2e638cf 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -145,7 +145,7 @@ val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys
/* whether misa.{f,d} were enabled at boot */
val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
/* whether zfinx was enabled at boot */
-val sys_enable_zfinx = {c: "sys_enable_zfinx",ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
+val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
/* whether the N extension was enabled at boot */
val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
@@ -165,7 +165,7 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
then m
else update_C(m, v.C());
/* Handle updates for F/D. */
- if ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) | sys_enable_zfinx()
+ if ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
then m
else update_D(update_F(m, v.F()), v.D())
}
@@ -180,7 +180,7 @@ function haveMulDiv() -> bool = misa.M() == 0b1
function haveSupMode() -> bool = misa.S() == 0b1
function haveUsrMode() -> bool = misa.U() == 0b1
function haveNExt() -> bool = misa.N() == 0b1
-/* see below for F and D extension tests */
+/* see below for F and D (and Z*inx counterparts) extension tests */
/* Cryptography extension support. Note these will need updating once */
/* Sail can be dynamically configured with different extension support */
@@ -280,12 +280,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
/* We don't have any extension context yet. */
let m = update_XS(m, extStatus_to_bits(Off));
- let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m;
+
/* FS is WARL, and making FS writable can support the M-mode emulation of an FPU
- * to support code running in S/U-modes. Spike does this, and for now, we match it.
+ * to support code running in S/U-modes. Spike does this, and for now, we match it,
+ * but only if Zfinx isn't enabled.
* FIXME: This should be made a platform parameter.
*/
-
+ let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m;
let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
let m = update_SD(m, bool_to_bits(dirty));
@@ -331,8 +332,12 @@ function in32BitMode() -> bool = {
}
/* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */
-function haveFExt() -> bool = (misa.F() == 0b1 & mstatus.FS() != 0b00) | sys_enable_zfinx()
-function haveDExt() -> bool = (misa.D() == 0b1 & mstatus.FS() != 0b00) | (sys_enable_zfinx() & sizeof(flen)==64)
+function haveFExt() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00)
+function haveDExt() -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00)
+
+/* Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
+function haveZfinx() -> bool = sys_enable_zfinx()
+function haveZdinx() -> bool = sys_enable_zfinx() & sizeof(flen) >= 64
/* interrupt processing state */
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index a1d9c82..ccf4875 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -11,7 +11,6 @@ let config_enable_dirty_update = ref false
let config_enable_misaligned_access = ref false
let config_mtval_has_illegal_inst_bits = ref false
let config_enable_pmp = ref false
-let config_enable_zfinx = ref false
let platform_arch = ref P.RV64
@@ -83,7 +82,7 @@ let enable_dirty_update () = !config_enable_dirty_update
let enable_misaligned_access () = !config_enable_misaligned_access
let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
let enable_pmp () = !config_enable_pmp
-let enable_zfinx () = !config_enable_zfinx
+let enable_zfinx () = false
let rom_base () = arch_bits_of_int64 P.rom_base
let rom_size () = arch_bits_of_int !rom_size_ref
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment