From 3d2690402350da607ac3d7f8b1f835cd194c015e Mon Sep 17 00:00:00 2001 From: "Paul A. Clarke" Date: Fri, 29 Sep 2023 18:11:37 -0500 Subject: [PATCH] Add enums and "extensionEnabled" function for discriminating extension content Extensions: D, F, Zbc, Zbkb, Zbkc, Zbkx, Zbs, Zfa, Zfh, Zicond, Zknd, Zkne, Zknh, Zkr, Zksed, Zksh. --- model/riscv_fdext_control.sail | 12 +++- model/riscv_insts_cdext.sail | 16 ++--- model/riscv_insts_cfext.sail | 16 ++--- model/riscv_insts_dext.sail | 10 +-- model/riscv_insts_end.sail | 2 + model/riscv_insts_fext.sail | 37 +++++------ model/riscv_insts_zbb.sail | 47 +++++++------- model/riscv_insts_zbc.sail | 18 ++++-- model/riscv_insts_zbkb.sail | 24 ++++---- model/riscv_insts_zbkx.sail | 11 ++-- model/riscv_insts_zbs.sail | 35 ++++++----- model/riscv_insts_zfa.sail | 99 +++++++++++++++--------------- model/riscv_insts_zfh.sail | 10 +-- model/riscv_insts_zicond.sail | 11 ++-- model/riscv_insts_zkn.sail | 108 ++++++++++++++++++--------------- model/riscv_insts_zks.sail | 22 ++++--- model/riscv_sys_control.sail | 4 +- model/riscv_sys_regs.sail | 28 --------- model/riscv_types.sail | 7 +++ 19 files changed, 272 insertions(+), 245 deletions(-) diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 8f299994b..baf5eb7ee 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -15,11 +15,17 @@ /* **************************************************************** */ +enum clause extensions = Ext_F +function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b00) + +enum clause extensions = Ext_D +function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64 + /* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */ -function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx() -function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx() -function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx() +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_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS])) function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM])) diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail index aeda8fc3f..6412d781b 100644 --- a/model/riscv_insts_cdext.sail +++ b/model/riscv_insts_cdext.sail @@ -17,9 +17,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() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) <-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) function clause execute (C_FLDSP(uimm, rd)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -35,9 +35,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() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) <-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) function clause execute (C_FSDSP(uimm, rs2)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -53,9 +53,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() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) <-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) function clause execute (C_FLD(uimm, rsc, rdc)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -73,9 +73,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() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) <-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & extensionEnabled(Ext_D) function clause execute (C_FSD(uimm, rsc1, rsc2)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail index 71b1e0b25..3787e2420 100644 --- a/model/riscv_insts_cfext.sail +++ b/model/riscv_insts_cfext.sail @@ -17,9 +17,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() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) function clause execute (C_FLWSP(imm, rd)) = { let imm : bits(12) = zero_extend(imm @ 0b00); @@ -35,9 +35,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() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) function clause execute (C_FSWSP(uimm, rs2)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); @@ -53,9 +53,9 @@ mapping clause assembly = C_FSWSP(uimm, rs2) 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() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) function clause execute (C_FLW(uimm, rsc, rdc)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); @@ -73,9 +73,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() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) <-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & extensionEnabled(Ext_F) function clause execute (C_FSW(uimm, rsc1, rsc2)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 03b582434..3b2c34d96 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -224,7 +224,7 @@ function fle_D (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveDoubleFPU() -> bool = haveDExt() | haveZdinx() +function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | haveZdinx() /* RV32Zdinx requires even register pairs; can be omitted for code */ /* not used for RV32Zdinx (i.e. RV64-only or D-only). */ @@ -902,11 +902,11 @@ mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if /* D instructions, RV64 only */ -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if haveDExt() & sizeof(xlen) >= 64 - <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & sizeof(xlen) >= 64 +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if haveDExt() & sizeof(xlen) >= 64 - <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & sizeof(xlen) >= 64 +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 + <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 /* Execution semantics ================================ */ diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail index d6a328d48..3e0c2a3ec 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -27,6 +27,8 @@ mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s) /* ****************************************************************** */ /* End definitions */ +end extension_supported +end extensions end ast end execute end assembly diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 5c89e9188..c14054ddb 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -25,6 +25,9 @@ /* **************************************************************** */ +enum clause extensions = Ext_Zfh +function clause extensionEnabled(Ext_Zfh) = (misa[F] == 0b1) & (mstatus[FS] != 0b00) + mapping encdec_rounding_mode : rounding_mode <-> bits(3) = { RM_RNE <-> 0b000, RM_RTZ <-> 0b001, @@ -259,7 +262,7 @@ function fle_S (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveSingleFPU() -> bool = haveFExt() | haveZfinx() +function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | haveZfinx() /* ****************************************************************** */ /* Floating-point loads */ @@ -271,14 +274,14 @@ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = LOAD_FP(imm, rs1, rd, HALF) if haveZfh() - <-> imm @ rs1 @ 0b001 @ rd @ 0b000_0111 if haveZfh() +mapping clause encdec = LOAD_FP(imm, rs1, rd, HALF) if extensionEnabled(Ext_Zfh) + <-> imm @ rs1 @ 0b001 @ rd @ 0b000_0111 if extensionEnabled(Ext_Zfh) -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, WORD) if extensionEnabled(Ext_F) + <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if extensionEnabled(Ext_F) -mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt() - <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if haveDExt() +mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if extensionEnabled(Ext_D) + <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if extensionEnabled(Ext_D) /* Execution semantics ================================ */ @@ -357,14 +360,14 @@ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, HALF) if haveZfh() - <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b001 @ imm5 : bits(5) @ 0b010_0111 if haveZfh() +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, HALF) if extensionEnabled(Ext_Zfh) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b001 @ imm5 : bits(5) @ 0b010_0111 if extensionEnabled(Ext_Zfh) -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, WORD) if extensionEnabled(Ext_F) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if extensionEnabled(Ext_F) -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() +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if extensionEnabled(Ext_D) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if extensionEnabled(Ext_D) /* Execution semantics ================================ */ @@ -1024,11 +1027,11 @@ union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S) mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S) if haveSingleFPU() <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU() -mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W) if haveFExt() - <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W) if extensionEnabled(Ext_F) + <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_F) -mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if haveFExt() - <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if extensionEnabled(Ext_F) + <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_F) /* Execution semantics ================================ */ diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index d39afc00b..446720853 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -6,11 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extensions = Ext_Zbkb +function clause extensionEnabled(Ext_Zbkb) = true + /* ****************************************************************** */ union clause ast = RISCV_RORIW : (bits(5), regidx, regidx) -mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 mapping clause assembly = RISCV_RORIW(shamt, rs1, rd) <-> "roriw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) @@ -25,8 +28,8 @@ function clause execute (RISCV_RORIW(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_RORI : (bits(6), regidx, regidx) -mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero) mapping clause assembly = RISCV_RORI(shamt, rs1, rd) <-> "rori" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) @@ -43,11 +46,11 @@ function clause execute (RISCV_RORI(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = ZBB_RTYPEW : (regidx, regidx, regidx, bropw_zbb) -mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 -mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = { RISCV_ROLW <-> "rolw", @@ -71,14 +74,14 @@ function clause execute (ZBB_RTYPEW(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBB_RTYPE : (regidx, regidx, regidx, brop_zbb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb() | haveZbkb() - <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb() | extensionEnabled(Ext_Zbkb) + <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | haveZbkb() - <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | extensionEnabled(Ext_Zbkb) + <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | haveZbkb() - <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | extensionEnabled(Ext_Zbkb) + <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb) mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if haveZbb() <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() @@ -92,11 +95,11 @@ mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if haveZbb() mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MINU) if haveZbb() <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | haveZbkb() - <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | extensionEnabled(Ext_Zbkb) + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | haveZbkb() - <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | haveZbkb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | extensionEnabled(Ext_Zbkb) + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb) mapping zbb_rtype_mnemonic : brop_zbb <-> string = { RISCV_ANDN <-> "andn", @@ -173,11 +176,11 @@ function clause execute (ZBB_EXTOP(rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = RISCV_REV8 : (regidx, regidx) -mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32 - <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32 +mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32 + <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32 -mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 - <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 mapping clause assembly = RISCV_REV8(rs1, rd) <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail index 458b9faf0..abc0ad06f 100644 --- a/model/riscv_insts_zbc.sail +++ b/model/riscv_insts_zbc.sail @@ -6,11 +6,17 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extensions = Ext_Zbc +function clause extensionEnabled(Ext_Zbc) = true + +enum clause extensions = Ext_Zbkc +function clause extensionEnabled(Ext_Zbkc) = true + /* ****************************************************************** */ union clause ast = RISCV_CLMUL : (regidx, regidx, regidx) -mapping clause encdec = RISCV_CLMUL(rs2, rs1, rd) if haveZbc() | haveZbkc() - <-> 0b0000101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbc() | haveZbkc() +mapping clause encdec = RISCV_CLMUL(rs2, rs1, rd) if extensionEnabled(Ext_Zbc) | extensionEnabled(Ext_Zbkc) + <-> 0b0000101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbc) | extensionEnabled(Ext_Zbkc) mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd) <-> "clmul" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -28,8 +34,8 @@ function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CLMULH : (regidx, regidx, regidx) -mapping clause encdec = RISCV_CLMULH(rs2, rs1, rd) if haveZbc() | haveZbkc() - <-> 0b0000101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011 if haveZbc() | haveZbkc() +mapping clause encdec = RISCV_CLMULH(rs2, rs1, rd) if extensionEnabled(Ext_Zbc) | extensionEnabled(Ext_Zbkc) + <-> 0b0000101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbc) | extensionEnabled(Ext_Zbkc) mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd) <-> "clmulh" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -47,8 +53,8 @@ function clause execute (RISCV_CLMULH(rs2, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CLMULR : (regidx, regidx, regidx) -mapping clause encdec = RISCV_CLMULR(rs2, rs1, rd) if haveZbc() - <-> 0b0000101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZbc() +mapping clause encdec = RISCV_CLMULR(rs2, rs1, rd) if extensionEnabled(Ext_Zbc) + <-> 0b0000101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbc) mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd) <-> "clmulr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail index f6246d17a..b8ce9569b 100644 --- a/model/riscv_insts_zbkb.sail +++ b/model/riscv_insts_zbkb.sail @@ -9,11 +9,11 @@ /* ****************************************************************** */ union clause ast = ZBKB_RTYPE : (regidx, regidx, regidx, brop_zbkb) -mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACK) if haveZbkb() - <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbkb() +mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACK) if extensionEnabled(Ext_Zbkb) + <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbkb) -mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACKH) if haveZbkb() - <-> 0b0000100 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbkb() +mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACKH) if extensionEnabled(Ext_Zbkb) + <-> 0b0000100 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbkb) mapping zbkb_rtype_mnemonic : brop_zbkb <-> string = { RISCV_PACK <-> "pack", @@ -37,8 +37,8 @@ function clause execute (ZBKB_RTYPE(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBKB_PACKW : (regidx, regidx, regidx) -mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if haveZbkb() & sizeof(xlen) == 64 - <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZbkb() & sizeof(xlen) == 64 +mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 64 + <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 64 mapping clause assembly = ZBKB_PACKW(rs2, rs1, rd) <-> "packw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -55,8 +55,8 @@ function clause execute (ZBKB_PACKW(rs2, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_ZIP : (regidx, regidx) -mapping clause encdec = RISCV_ZIP(rs1, rd) if haveZbkb() & sizeof(xlen) == 32 - <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbkb() & sizeof(xlen) == 32 +mapping clause encdec = RISCV_ZIP(rs1, rd) if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 + <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 mapping clause assembly = RISCV_ZIP(rs1, rd) <-> "zip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -76,8 +76,8 @@ function clause execute (RISCV_ZIP(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_UNZIP : (regidx, regidx) -mapping clause encdec = RISCV_UNZIP(rs1, rd) if haveZbkb() & sizeof(xlen) == 32 - <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbkb() & sizeof(xlen) == 32 +mapping clause encdec = RISCV_UNZIP(rs1, rd) if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 + <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 mapping clause assembly = RISCV_UNZIP(rs1, rd) <-> "unzip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -97,8 +97,8 @@ function clause execute (RISCV_UNZIP(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_BREV8 : (regidx, regidx) -mapping clause encdec = RISCV_BREV8(rs1, rd) if haveZbkb() - <-> 0b011010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbkb() +mapping clause encdec = RISCV_BREV8(rs1, rd) if extensionEnabled(Ext_Zbkb) + <-> 0b011010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) mapping clause assembly = RISCV_BREV8(rs1, rd) <-> "brev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail index d19a2b15d..c1dc506bd 100644 --- a/model/riscv_insts_zbkx.sail +++ b/model/riscv_insts_zbkx.sail @@ -6,11 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extensions = Ext_Zbkx +function clause extensionEnabled(Ext_Zbkx) = true + /* ****************************************************************** */ union clause ast = RISCV_XPERM8 : (regidx, regidx, regidx) -mapping clause encdec = RISCV_XPERM8(rs2, rs1, rd) if haveZbkx() - <-> 0b0010100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbkx() +mapping clause encdec = RISCV_XPERM8(rs2, rs1, rd) if extensionEnabled(Ext_Zbkx) + <-> 0b0010100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbkx) mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd) <-> "xperm8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -32,8 +35,8 @@ function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_XPERM4 : (regidx, regidx, regidx) -mapping clause encdec = RISCV_XPERM4(rs2, rs1, rd) if haveZbkx() - <-> 0b0010100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZbkx() +mapping clause encdec = RISCV_XPERM4(rs2, rs1, rd) if extensionEnabled(Ext_Zbkx) + <-> 0b0010100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbkx) mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd) <-> "xperm4" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail index b535701c8..817b8b044 100644 --- a/model/riscv_insts_zbs.sail +++ b/model/riscv_insts_zbs.sail @@ -6,20 +6,23 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extensions = Ext_Zbs +function clause extensionEnabled(Ext_Zbs) = true | haveBExt() + /* ****************************************************************** */ union clause ast = ZBS_IOP : (bits(6), regidx, regidx, biop_zbs) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) mapping zbs_iop_mnemonic : biop_zbs <-> string = { RISCV_BCLRI <-> "bclri", @@ -49,17 +52,17 @@ function clause execute (ZBS_IOP(shamt, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBS_RTYPE : (regidx, regidx, regidx, brop_zbs) -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BCLR) if haveZbs() - <-> 0b0100100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BCLR) if extensionEnabled(Ext_Zbs) + <-> 0b0100100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbs) -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BEXT) if haveZbs() - <-> 0b0100100 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BEXT) if extensionEnabled(Ext_Zbs) + <-> 0b0100100 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbs) -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BINV) if haveZbs() - <-> 0b0110100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BINV) if extensionEnabled(Ext_Zbs) + <-> 0b0110100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbs) -mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BSET) if haveZbs() - <-> 0b0010100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs() +mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BSET) if extensionEnabled(Ext_Zbs) + <-> 0b0010100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbs) mapping zbs_rtype_mnemonic : brop_zbs <-> string = { RISCV_BCLR <-> "bclr", diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 1443daf3d..d37521843 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -6,12 +6,15 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extensions = Ext_Zfa +function clause extensionEnabled(Ext_Zfa) = true + /* FLI.H */ union clause ast = RISCV_FLI_H : (bits(5), regidx) -mapping clause encdec = RISCV_FLI_H(rs1, rd) if haveZfh() & haveZfa() - <-> 0b111_1010 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FLI_H(rs1, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b111_1010 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLI_H(constantidx, rd) <-> "fli.h" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) @@ -59,8 +62,8 @@ function clause execute (RISCV_FLI_H(constantidx, rd)) = { union clause ast = RISCV_FLI_S : (bits(5), regidx) -mapping clause encdec = RISCV_FLI_S(rs1, rd) if haveZfa() - <-> 0b111_1000 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FLI_S(rs1, rd) if extensionEnabled(Ext_Zfa) + <-> 0b111_1000 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLI_S(constantidx, rd) <-> "fli.s" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) @@ -108,8 +111,8 @@ function clause execute (RISCV_FLI_S(constantidx, rd)) = { union clause ast = RISCV_FLI_D : (bits(5), regidx) -mapping clause encdec = RISCV_FLI_D(rs1, rd) if haveDExt() & haveZfa() - <-> 0b111_1001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FLI_D(rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b111_1001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLI_D(constantidx, rd) <-> "fli.d" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) @@ -157,8 +160,8 @@ function clause execute (RISCV_FLI_D(constantidx, rd)) = { union clause ast = RISCV_FMINM_H : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMINM_H(rs2, rs1, rd) if haveZfh() & haveZfa() - <-> 0b001_0110 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FMINM_H(rs2, rs1, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b001_0110 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FMINM_H(rs2, rs1, rd) <-> "fminm.h" ^ spc() ^ freg_name(rd) @@ -187,8 +190,8 @@ function clause execute (RISCV_FMINM_H(rs2, rs1, rd)) = { union clause ast = RISCV_FMAXM_H : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMAXM_H(rs2, rs1, rd) if haveZfh() & haveZfa() - <-> 0b001_0110 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FMAXM_H(rs2, rs1, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b001_0110 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FMAXM_H(rs2, rs1, rd) <-> "fmaxm.h" ^ spc() ^ freg_name(rd) @@ -217,8 +220,8 @@ function clause execute (RISCV_FMAXM_H(rs2, rs1, rd)) = { union clause ast = RISCV_FMINM_S : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMINM_S(rs2, rs1, rd) if haveZfa() - <-> 0b001_0100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FMINM_S(rs2, rs1, rd) if extensionEnabled(Ext_Zfa) + <-> 0b001_0100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FMINM_S(rs2, rs1, rd) <-> "fminm.s" ^ spc() ^ freg_name(rd) @@ -247,8 +250,8 @@ function clause execute (RISCV_FMINM_S(rs2, rs1, rd)) = { union clause ast = RISCV_FMAXM_S : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMAXM_S(rs2, rs1, rd) if haveZfa() - <-> 0b001_0100 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FMAXM_S(rs2, rs1, rd) if extensionEnabled(Ext_Zfa) + <-> 0b001_0100 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FMAXM_S(rs2, rs1, rd) <-> "fmaxm.s" ^ spc() ^ freg_name(rd) @@ -277,8 +280,8 @@ function clause execute (RISCV_FMAXM_S(rs2, rs1, rd)) = { union clause ast = RISCV_FMINM_D : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMINM_D(rs2, rs1, rd) if haveDExt() & haveZfa() - <-> 0b001_0101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FMINM_D(rs2, rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b001_0101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FMINM_D(rs2, rs1, rd) <-> "fminm.d" ^ spc() ^ freg_name(rd) @@ -307,8 +310,8 @@ function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = { union clause ast = RISCV_FMAXM_D : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMAXM_D(rs2, rs1, rd) if haveDExt() & haveZfa() - <-> 0b001_0101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FMAXM_D(rs2, rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b001_0101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FMAXM_D(rs2, rs1, rd) <-> "fmaxm.d" ^ spc() ^ freg_name(rd) @@ -337,8 +340,8 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = { union clause ast = RISCV_FROUND_H : (regidx, rounding_mode, regidx) -mapping clause encdec = RISCV_FROUND_H(rs1, rm, rd) if haveZfh() & haveZfa() - <-> 0b010_0010 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FROUND_H(rs1, rm, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b010_0010 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FROUND_H(rs1, rm, rd) <-> "fround.h" ^ spc() ^ freg_name(rd) @@ -365,8 +368,8 @@ function clause execute (RISCV_FROUND_H(rs1, rm, rd)) = { union clause ast = RISCV_FROUNDNX_H : (regidx, rounding_mode, regidx) -mapping clause encdec = RISCV_FROUNDNX_H(rs1, rm, rd) if haveZfh() & haveZfa() - <-> 0b010_0010 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FROUNDNX_H(rs1, rm, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b010_0010 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FROUNDNX_H(rs1, rm, rd) <-> "froundnx.h" ^ spc() ^ freg_name(rd) @@ -393,8 +396,8 @@ function clause execute (RISCV_FROUNDNX_H(rs1, rm, rd)) = { union clause ast = RISCV_FROUND_S : (regidx, rounding_mode, regidx) -mapping clause encdec = RISCV_FROUND_S(rs1, rm, rd) if haveZfa() - <-> 0b010_0000 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FROUND_S(rs1, rm, rd) if extensionEnabled(Ext_Zfa) + <-> 0b010_0000 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FROUND_S(rs1, rm, rd) <-> "fround.s" ^ spc() ^ freg_name(rd) @@ -421,8 +424,8 @@ function clause execute (RISCV_FROUND_S(rs1, rm, rd)) = { union clause ast = RISCV_FROUNDNX_S : (regidx, rounding_mode, regidx) -mapping clause encdec = RISCV_FROUNDNX_S(rs1, rm, rd) if haveZfa() - <-> 0b010_0000 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FROUNDNX_S(rs1, rm, rd) if extensionEnabled(Ext_Zfa) + <-> 0b010_0000 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FROUNDNX_S(rs1, rm, rd) <-> "froundnx.s" ^ spc() ^ freg_name(rd) @@ -449,8 +452,8 @@ function clause execute (RISCV_FROUNDNX_S(rs1, rm, rd)) = { union clause ast = RISCV_FROUND_D : (regidx, rounding_mode, regidx) -mapping clause encdec = RISCV_FROUND_D(rs1, rm, rd) if haveDExt() & haveZfa() - <-> 0b010_0001 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FROUND_D(rs1, rm, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b010_0001 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FROUND_D(rs1, rm, rd) <-> "fround.d" ^ spc() ^ freg_name(rd) @@ -477,8 +480,8 @@ function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = { union clause ast = RISCV_FROUNDNX_D : (regidx, rounding_mode, regidx) -mapping clause encdec = RISCV_FROUNDNX_D(rs1, rm, rd) if haveDExt() & haveZfa() - <-> 0b010_0001 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FROUNDNX_D(rs1, rm, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b010_0001 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FROUNDNX_D(rs1, rm, rd) <-> "froundnx.d" ^ spc() ^ freg_name(rd) @@ -505,8 +508,8 @@ function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = { union clause ast = RISCV_FMVH_X_D : (regidx, regidx) -mapping clause encdec = RISCV_FMVH_X_D(rs1, rd) if haveDExt() & haveZfa() & in32BitMode() - <-> 0b111_0001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & haveZfa() & in32BitMode() +mapping clause encdec = RISCV_FMVH_X_D(rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) & in32BitMode() + <-> 0b111_0001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) & in32BitMode() mapping clause assembly = RISCV_FMVH_X_D(rs1, rd) <-> "fmvh.x.d" ^ spc() ^ reg_name(rd) @@ -523,8 +526,8 @@ function clause execute (RISCV_FMVH_X_D(rs1, rd)) = { union clause ast = RISCV_FMVP_D_X : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FMVP_D_X(rs2, rs1, rd) if haveDExt() & haveZfa() & in32BitMode() - <-> 0b101_1001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & haveZfa() & in32BitMode() +mapping clause encdec = RISCV_FMVP_D_X(rs2, rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) & in32BitMode() + <-> 0b101_1001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) & in32BitMode() mapping clause assembly = RISCV_FMVP_D_X(rs2, rs1, rd) <-> "fmvp.d.x" ^ spc() ^ freg_name(rd) @@ -550,8 +553,8 @@ function clause execute (RISCV_FMVP_D_X(rs2, rs1, rd)) = { union clause ast = RISCV_FLEQ_H : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FLEQ_H(rs2, rs1, rd) if haveZfh() & haveZfa() - <-> 0b101_0010 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FLEQ_H(rs2, rs1, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b101_0010 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLEQ_H(rs2, rs1, rd) <-> "fleq.h" ^ spc() ^ freg_name(rd) @@ -574,8 +577,8 @@ function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = { union clause ast = RISCV_FLTQ_H : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FLTQ_H(rs2, rs1, rd) if haveZfh() & haveZfa() - <-> 0b101_0010 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveZfh() & haveZfa() +mapping clause encdec = RISCV_FLTQ_H(rs2, rs1, rd) if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) + <-> 0b101_0010 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLTQ_H(rs2, rs1, rd) <-> "fltq.h" ^ spc() ^ freg_name(rd) @@ -598,8 +601,8 @@ function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = { union clause ast = RISCV_FLEQ_S : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FLEQ_S(rs2, rs1, rd) if haveZfa() - <-> 0b101_0000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FLEQ_S(rs2, rs1, rd) if extensionEnabled(Ext_Zfa) + <-> 0b101_0000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLEQ_S(rs2, rs1, rd) <-> "fleq.s" ^ spc() ^ freg_name(rd) @@ -622,8 +625,8 @@ function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = { union clause ast = RISCV_FLTQ_S : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FLTQ_S(rs2, rs1, rd) if haveZfa() - <-> 0b101_0000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveZfa() +mapping clause encdec = RISCV_FLTQ_S(rs2, rs1, rd) if extensionEnabled(Ext_Zfa) + <-> 0b101_0000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLTQ_S(rs2, rs1, rd) <-> "fltq.s" ^ spc() ^ freg_name(rd) @@ -647,8 +650,8 @@ function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = { union clause ast = RISCV_FLEQ_D : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FLEQ_D(rs2, rs1, rd) if haveDExt() & haveZfa() - <-> 0b101_0001 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FLEQ_D(rs2, rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLEQ_D(rs2, rs1, rd) <-> "fleq.d" ^ spc() ^ freg_name(rd) @@ -671,8 +674,8 @@ function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = { union clause ast = RISCV_FLTQ_D : (regidx, regidx, regidx) -mapping clause encdec = RISCV_FLTQ_D(rs2, rs1, rd) if haveDExt() & haveZfa() - <-> 0b101_0001 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FLTQ_D(rs2, rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FLTQ_D(rs2, rs1, rd) <-> "fltq.d" ^ spc() ^ freg_name(rd) @@ -759,8 +762,8 @@ function fcvtmod_helper(x64) = { union clause ast = RISCV_FCVTMOD_W_D : (regidx, regidx) /* We need rounding mode to be explicitly specified to RTZ(0b001) */ -mapping clause encdec = RISCV_FCVTMOD_W_D(rs1, rd) if haveDExt() & haveZfa() - <-> 0b110_0001 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDExt() & haveZfa() +mapping clause encdec = RISCV_FCVTMOD_W_D(rs1, rd) if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) + <-> 0b110_0001 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & extensionEnabled(Ext_Zfa) mapping clause assembly = RISCV_FCVTMOD_W_D(rs1, rd) <-> "fcvtmod.w.d" ^ spc() ^ reg_name(rd) diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 5522bad22..af54b5679 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -162,7 +162,7 @@ function fle_H (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveHalfFPU() -> bool = haveZfh() | haveZhinx() +function haveHalfFPU() -> bool = extensionEnabled(Ext_Zfh) | haveZhinx() /* ****************************************************************** */ /* Floating-point loads */ @@ -881,11 +881,11 @@ union clause ast = F_UN_TYPE_H : (regidx, regidx, f_un_op_H) mapping clause encdec = F_UN_TYPE_H(rs1, rd, FCLASS_H) if haveHalfFPU() <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveHalfFPU() -mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_X_H) if haveZfh() - <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveZfh() +mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_X_H) if extensionEnabled(Ext_Zfh) + <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) -mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_H_X) if haveZfh() - <-> 0b111_1010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveZfh() +mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_H_X) if extensionEnabled(Ext_Zfh) + <-> 0b111_1010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Zfh) /* Execution semantics ================================ */ diff --git a/model/riscv_insts_zicond.sail b/model/riscv_insts_zicond.sail index d51260312..5b315452d 100644 --- a/model/riscv_insts_zicond.sail +++ b/model/riscv_insts_zicond.sail @@ -6,12 +6,15 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extensions = Ext_Zicond +function clause extensionEnabled(Ext_Zicond) = true + union clause ast = ZICOND_RTYPE : (regidx, regidx, regidx, zicondop) -mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ) if haveZicond() - <-> 0b0000111 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZicond() -mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_NEZ) if haveZicond() - <-> 0b0000111 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZicond() +mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ) if extensionEnabled(Ext_Zicond) + <-> 0b0000111 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extensionEnabled(Ext_Zicond) +mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_NEZ) if extensionEnabled(Ext_Zicond) + <-> 0b0000111 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extensionEnabled(Ext_Zicond) mapping zicond_mnemonic : zicondop <-> string = { RISCV_CZERO_EQZ <-> "czero.eqz", diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail index 8bcd250a7..259b2510b 100644 --- a/model/riscv_insts_zkn.sail +++ b/model/riscv_insts_zkn.sail @@ -10,23 +10,25 @@ * Scalar Cryptography Extension - Scalar SHA256 instructions (RV32/RV64) * ---------------------------------------------------------------------- */ +enum clause extensions = Ext_Zknh +function clause extensionEnabled(Ext_Zknh) = true union clause ast = SHA256SIG0 : (regidx, regidx) union clause ast = SHA256SIG1 : (regidx, regidx) union clause ast = SHA256SUM0 : (regidx, regidx) union clause ast = SHA256SUM1 : (regidx, regidx) -mapping clause encdec = SHA256SUM0 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() +mapping clause encdec = SHA256SUM0 (rs1, rd) if extensionEnabled(Ext_Zknh) + <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) -mapping clause encdec = SHA256SUM1 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() +mapping clause encdec = SHA256SUM1 (rs1, rd) if extensionEnabled(Ext_Zknh) + <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) -mapping clause encdec = SHA256SIG0 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() +mapping clause encdec = SHA256SIG0 (rs1, rd) if extensionEnabled(Ext_Zknh) + <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) -mapping clause encdec = SHA256SIG1 (rs1, rd) if haveZknh() - <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() +mapping clause encdec = SHA256SIG1 (rs1, rd) if extensionEnabled(Ext_Zknh) + <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) mapping clause assembly = SHA256SIG0 (rs1, rd) <-> "sha256sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -73,10 +75,13 @@ function clause execute (SHA256SUM1(rs1, rd)) = { * ---------------------------------------------------------------------- */ +enum clause extensions = Ext_Zkne +function clause extensionEnabled(Ext_Zkne) = true + union clause ast = AES32ESMI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 32 - <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 32 +mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 + <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 mapping clause assembly = AES32ESMI (bs, rs2, rs1, rd) <-> "aes32esmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -93,8 +98,8 @@ function clause execute (AES32ESMI (bs, rs2, rs1, rd)) = { union clause ast = AES32ESI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 32 - <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 32 +mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 + <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 mapping clause assembly = AES32ESI (bs, rs2, rs1, rd) <-> "aes32esi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -113,10 +118,13 @@ function clause execute (AES32ESI (bs, rs2, rs1, rd)) = { * ---------------------------------------------------------------------- */ +enum clause extensions = Ext_Zknd +function clause extensionEnabled(Ext_Zknd) = true + union clause ast = AES32DSMI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 32 - <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 32 +mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 + <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 mapping clause assembly = AES32DSMI (bs, rs2, rs1, rd) <-> "aes32dsmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -133,8 +141,8 @@ function clause execute (AES32DSMI (bs, rs2, rs1, rd)) = { union clause ast = AES32DSI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 32 - <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 32 +mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 + <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 mapping clause assembly = AES32DSI (bs, rs2, rs1, rd) <-> "aes32dsi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -160,23 +168,23 @@ union clause ast = SHA512SIG1H : (regidx, regidx, regidx) union clause ast = SHA512SUM0R : (regidx, regidx, regidx) union clause ast = SHA512SUM1R : (regidx, regidx, regidx) -mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 +mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 + <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 -mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 +mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 + <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 -mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 + <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 -mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 + <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 -mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 + <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 -mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32 - <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 + <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 mapping clause assembly = SHA512SIG0L (rs2, rs1, rd) <-> "sha512sig0l" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -245,26 +253,26 @@ union clause ast = AES64ES : (regidx, regidx, regidx) union clause ast = AES64DSM : (regidx, regidx, regidx) union clause ast = AES64DS : (regidx, regidx, regidx) -mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (haveZkne() | haveZknd()) & (sizeof(xlen) == 64) & (rnum <_u 0xB) - <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (haveZkne() | haveZknd()) & (sizeof(xlen) == 64) & (rnum <_u 0xB) +mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & (sizeof(xlen) == 64) & (rnum <_u 0xB) + <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & (sizeof(xlen) == 64) & (rnum <_u 0xB) -mapping clause encdec = AES64IM (rs1, rd) if haveZknd() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknd() & sizeof(xlen) == 64 +mapping clause encdec = AES64IM (rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 + <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 -mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (haveZkne() | haveZknd()) & sizeof(xlen) == 64 - <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (haveZkne() | haveZknd()) & sizeof(xlen) == 64 +mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & sizeof(xlen) == 64 + <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & sizeof(xlen) == 64 -mapping clause encdec = AES64ESM (rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 64 +mapping clause encdec = AES64ESM (rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 + <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 -mapping clause encdec = AES64ES (rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 64 +mapping clause encdec = AES64ES (rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 + <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 -mapping clause encdec = AES64DSM (rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 64 +mapping clause encdec = AES64DSM (rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 + <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 -mapping clause encdec = AES64DS (rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 64 - <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 64 +mapping clause encdec = AES64DS (rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 + <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 mapping clause assembly = AES64KS1I (rnum, rs1, rd) <-> "aes64ks1i" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_4(rnum) @@ -360,17 +368,17 @@ union clause ast = SHA512SIG1 : (regidx, regidx) union clause ast = SHA512SUM0 : (regidx, regidx) union clause ast = SHA512SUM1 : (regidx, regidx) -mapping clause encdec = SHA512SUM0 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 +mapping clause encdec = SHA512SUM0 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 -mapping clause encdec = SHA512SUM1 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 +mapping clause encdec = SHA512SUM1 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 -mapping clause encdec = SHA512SIG0 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 +mapping clause encdec = SHA512SIG0 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 -mapping clause encdec = SHA512SIG1 (rs1, rd) if haveZknh() & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64 +mapping clause encdec = SHA512SIG1 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 + <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 mapping clause assembly = SHA512SIG0 (rs1, rd) <-> "sha512sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/model/riscv_insts_zks.sail b/model/riscv_insts_zks.sail index 2cb44f181..2890cab95 100644 --- a/model/riscv_insts_zks.sail +++ b/model/riscv_insts_zks.sail @@ -11,14 +11,17 @@ * ---------------------------------------------------------------------- */ +enum clause extensions = Ext_Zksh +function clause extensionEnabled(Ext_Zksh) = true + union clause ast = SM3P0 : (regidx, regidx) union clause ast = SM3P1 : (regidx, regidx) -mapping clause encdec = SM3P0 (rs1, rd) if haveZksh() - <-> 0b00 @ 0b01000 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZksh() +mapping clause encdec = SM3P0 (rs1, rd) if extensionEnabled(Ext_Zksh) + <-> 0b00 @ 0b01000 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zksh) -mapping clause encdec = SM3P1 (rs1, rd) if haveZksh() - <-> 0b00 @ 0b01000 @ 0b01001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZksh() +mapping clause encdec = SM3P1 (rs1, rd) if extensionEnabled(Ext_Zksh) + <-> 0b00 @ 0b01000 @ 0b01001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zksh) mapping clause assembly = SM3P0 (rs1, rd) <-> "sm3p0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -45,14 +48,17 @@ function clause execute (SM3P1(rs1, rd)) = { * ---------------------------------------------------------------------- */ +enum clause extensions = Ext_Zksed +function clause extensionEnabled(Ext_Zksed) = true + union clause ast = SM4ED : (bits(2), regidx, regidx, regidx) union clause ast = SM4KS : (bits(2), regidx, regidx, regidx) -mapping clause encdec = SM4ED (bs, rs2, rs1, rd) if haveZksed() - <-> bs @ 0b11000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZksed() +mapping clause encdec = SM4ED (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zksed) + <-> bs @ 0b11000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zksed) -mapping clause encdec = SM4KS (bs, rs2, rs1, rd) if haveZksed() - <-> bs @ 0b11010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZksed() +mapping clause encdec = SM4KS (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zksed) + <-> bs @ 0b11010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zksed) mapping clause assembly = SM4ED (bs, rs2, rs1, rd) <-> "sm4ed" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 32775c27b..e42cd8e3a 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -8,6 +8,8 @@ /* Machine-mode and supervisor-mode functionality. */ +enum clause extensions = Ext_Zkr +function clause extensionEnabled(Ext_Zkr) = true /* CSR access control */ @@ -87,7 +89,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0xC82 => haveUsrMode() & (sizeof(xlen) == 32), // instreth /* user mode: Zkr */ - 0x015 => haveZkr(), + 0x015 => extensionEnabled(Ext_Zkr), /* check extensions */ _ => ext_is_CSR_defined(csr, p) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6eb174189..76e684d35 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -142,26 +142,6 @@ function haveNExt() -> bool = misa[N] == 0b1 function haveBExt() -> bool = misa[B] == 0b1 function haveZba() -> bool = true | haveBExt() function haveZbb() -> bool = true | haveBExt() -function haveZbs() -> bool = true | haveBExt() -function haveZbc() -> bool = true - -/* Zfa (additional FP) extension */ -function haveZfa() -> bool = true - -/* Scalar Cryptography extensions support. */ -function haveZbkb() -> bool = true -function haveZbkc() -> bool = true -function haveZbkx() -> bool = true - -/* Cryptography extension support. Note these will need updating once */ -/* Sail can be dynamically configured with different extension support */ -/* and have dynamic changes of XLEN via S/UXL */ -function haveZkr() -> bool = true -function haveZksh() -> bool = true -function haveZksed() -> bool = true -function haveZknh() -> bool = true -function haveZkne() -> bool = true -function haveZknd() -> bool = true function haveZmmul() -> bool = true @@ -169,9 +149,6 @@ function haveZmmul() -> bool = true function haveZaamo() -> bool = haveAtomics() function haveZalrsc() -> bool = haveAtomics() -/* Zicond extension support */ -function haveZicond() -> bool = true - /* Zabha extension support */ function haveZabha() -> bool = true @@ -335,11 +312,6 @@ function in32BitMode() -> bool = { cur_Architecture() == RV32 } -/* 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) -function haveDExt() -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64 -/* Zfh (half-precision) extension depends on misa.F and mstatus.FS */ -function haveZfh() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00) /* V extension has to enable both via misa.V as well as mstatus.VS */ function haveVExt() -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00) diff --git a/model/riscv_types.sail b/model/riscv_types.sail index f6e2d1ced..d8eb04de6 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -8,6 +8,13 @@ /* Basic type and function definitions used pervasively in the model. */ +/* ISA extension names as enums */ +scattered enum extensions + +/* Function used to determine if an extension is enabled in the current configuration */ +val extensionEnabled : extensions -> bool +scattered function extensionEnabled + /* this value is only defined for the runtime platform for ELF loading * checks, and not used in the model. */