Skip to content

Commit

Permalink
Make use of extensionEnabled() instead of have*()
Browse files Browse the repository at this point in the history
* Utilize extensionEnabled() instead of `haveZmmul()`, `haveUsrMode()`,
  `haveSupMode()`, `haveNExt()`, etc..
* Delete all unused  `have*` definitions of various extensions
  • Loading branch information
jriyyya authored and ThinkOpenly committed Jul 9, 2024
1 parent 12ed765 commit 424e100
Show file tree
Hide file tree
Showing 21 changed files with 385 additions and 374 deletions.
9 changes: 6 additions & 3 deletions model/riscv_fdext_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -21,11 +21,14 @@ function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b0
enum clause extensions = Ext_D
function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64

enum clause extensions = Ext_Zfinx
function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx()

/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */

function clause ext_is_CSR_defined (0x001, _) = extensionEnabled(Ext_F) | haveZfinx()
function clause ext_is_CSR_defined (0x002, _) = extensionEnabled(Ext_F) | haveZfinx()
function clause ext_is_CSR_defined (0x003, _) = extensionEnabled(Ext_F) | haveZfinx()
function clause ext_is_CSR_defined (0x001, _) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause ext_is_CSR_defined (0x002, _) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
function clause ext_is_CSR_defined (0x003, _) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)

function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS]))
function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM]))
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -664,8 +664,8 @@ mapping clause encdec = SRET()
function clause execute SRET() = {
let sret_illegal : bool = match cur_privilege {
User => true,
Supervisor => not(haveSupMode ()) | mstatus[TSR] == 0b1,
Machine => not(haveSupMode ())
Supervisor => not(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
Machine => not(extensionEnabled(Ext_S))
};
if sret_illegal
then { handle_illegal(); RETIRE_FAIL }
Expand Down
7 changes: 5 additions & 2 deletions model/riscv_insts_dext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -224,13 +224,16 @@ function fle_D (v1, v2, is_quiet) = {
/* **************************************************************** */
/* Helper functions for 'encdec()' */

function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | haveZdinx()
enum clause extensions = Ext_Zdinx
function clause extensionEnabled(Ext_Zdinx) = sys_enable_zfinx() & sizeof(flen) >= 64

function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | extensionEnabled(Ext_Zdinx)

/* 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
if extensionEnabled(Ext_Zdinx) & sizeof(xlen) == 32 then
foreach (i from 0 to (n - 1))
if (regs[i][0] == bitone) then return false;
true
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_insts_fext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -262,7 +262,7 @@ function fle_S (v1, v2, is_quiet) = {
/* **************************************************************** */
/* Helper functions for 'encdec()' */

function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | haveZfinx()
function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)

/* ****************************************************************** */
/* Floating-point loads */
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_insts_next.sail
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ mapping clause encdec = URET()
<-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011

function clause execute URET() = {
if not(haveUsrMode()) | not(sys_enable_next())
if not(extensionEnabled(Ext_U)) | not(sys_enable_next())
then handle_illegal()
else if not(ext_check_xret_priv(User))
then ext_fail_xret_priv()
Expand Down
15 changes: 9 additions & 6 deletions model/riscv_insts_svinval.sail
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,14 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

enum clause extensions = Ext_Svinval
function clause extensionEnabled(Ext_Svinval) = sys_enable_svinval()

union clause ast = SINVAL_VMA : (regidx, regidx)

mapping clause encdec =
SINVAL_VMA(rs1, rs2) if haveSvinval()
<-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
SINVAL_VMA(rs1, rs2) if extensionEnabled(Ext_Svinval)
<-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)

function clause execute SINVAL_VMA(rs1, rs2) = {
execute(SFENCE_VMA(rs1, rs2))
Expand All @@ -24,8 +27,8 @@ mapping clause assembly = SINVAL_VMA(rs1, rs2)
union clause ast = SFENCE_W_INVAL : unit

mapping clause encdec =
SFENCE_W_INVAL() if haveSvinval()
<-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
SFENCE_W_INVAL() if extensionEnabled(Ext_Svinval)
<-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)

function clause execute SFENCE_W_INVAL() = {
if cur_privilege == User
Expand All @@ -40,8 +43,8 @@ mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval"
union clause ast = SFENCE_INVAL_IR : unit

mapping clause encdec =
SFENCE_INVAL_IR() if haveSvinval()
<-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
SFENCE_INVAL_IR() if extensionEnabled(Ext_Svinval)
<-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)

function clause execute SFENCE_INVAL_IR() = {
if cur_privilege == User
Expand Down
Loading

0 comments on commit 424e100

Please sign in to comment.