diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 03450e8f6..11b8e425e 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -15,11 +15,20 @@ /* **************************************************************** */ +enum clause extension = Ext_F +function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b00) + +enum clause extension = Ext_D +function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64 + +enum clause extension = Ext_Zfinx +function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx() + /* val clause ext_is_CSR_defined : (csreg) -> 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) | 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])) diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 6fd66917d..78401c8b8 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -19,7 +19,7 @@ function fetch() -> FetchResult = match ext_fetch_check_pc(PC, PC) { Ext_FetchAddr_Error(e) => F_Ext_Error(e), Ext_FetchAddr_OK(use_pc) => { - if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC()))) + if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_C)))) then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index d25237572..cdb8f9416 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -17,7 +17,7 @@ function fetch() -> FetchResult = { Ext_FetchAddr_Error(e) => F_Ext_Error(e), Ext_FetchAddr_OK(use_pc) => { /* then check PC alignment */ - if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC()))) + if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extensionEnabled(Ext_C)))) then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 8141acec2..04ae9a67b 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -10,6 +10,9 @@ /* This file specifies the atomic instructions in the 'A' extension. */ /* ****************************************************************** */ +enum clause extension = Ext_Zabha +function clause extensionEnabled(Ext_Zabha) = true + // Some print utils for lr/sc. function aqrl_str(aq : bool, rl : bool) -> string = @@ -42,18 +45,21 @@ function lrsc_width_valid(size : word_width) -> bool = { function amo_width_valid(size : word_width) -> bool = { match size { - BYTE => haveZabha(), - HALF => haveZabha(), + BYTE => extensionEnabled(Ext_Zabha), + HALF => extensionEnabled(Ext_Zabha), WORD => true, DOUBLE => sizeof(xlen) >= 64, } } /* ****************************************************************** */ +enum clause extension = Ext_Zalrsc +function clause extensionEnabled(Ext_Zalrsc) = misa[A] == 0b1 + union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) -mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if haveZalrsc() & lrsc_width_valid(size) - <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & lrsc_width_valid(size) +mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) + <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) /* We could set load-reservations on physical or virtual addresses. * For now we set them on virtual addresses, since it makes the @@ -96,8 +102,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) /* ****************************************************************** */ union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx) -mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if haveZalrsc() & lrsc_width_valid(size) - <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & lrsc_width_valid(size) +mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) + <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { @@ -157,6 +163,9 @@ mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" /* ****************************************************************** */ +enum clause extension = Ext_Zaamo +function clause extensionEnabled(Ext_Zaamo) = misa[A] == 0b1 + union clause ast = AMO : (amoop, bool, bool, regidx, regidx, word_width, regidx) mapping encdec_amoop : amoop <-> bits(5) = { @@ -171,8 +180,8 @@ mapping encdec_amoop : amoop <-> bits(5) = { AMOMAXU <-> 0b11100 } -mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if haveZaamo() & amo_width_valid(size) - <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZaamo() & amo_width_valid(size) +mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zaamo) & amo_width_valid(size) + <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zaamo) & amo_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 26915f22c..599c0a7a4 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -9,6 +9,8 @@ /* ****************************************************************** */ /* This file specifies the instructions in the base integer set. */ +enum clause extension = Ext_C +function clause extensionEnabled(Ext_C) = misa[C] == 0b1 /* ****************************************************************** */ union clause ast = UTYPE : (bits(20), regidx, uop) @@ -67,7 +69,7 @@ function clause execute (RISCV_JAL(imm, rd)) = { }, Ext_ControlAddr_OK(target) => { /* Perform standard alignment check */ - if bit_to_bool(target[1]) & not(haveRVC()) + if bit_to_bool(target[1]) & not(extensionEnabled(Ext_C)) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL @@ -131,7 +133,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = { RETIRE_FAIL }, Ext_ControlAddr_OK(target) => { - if bit_to_bool(target[1]) & not(haveRVC()) then { + if bit_to_bool(target[1]) & not(extensionEnabled(Ext_C)) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL; } else { @@ -662,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 } diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail index aeda8fc3f..5571befd4 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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) & extensionEnabled(Ext_C) & 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_cext.sail b/model/riscv_insts_cext.sail index b7c63c2a5..c93332a1d 100644 --- a/model/riscv_insts_cext.sail +++ b/model/riscv_insts_cext.sail @@ -17,8 +17,8 @@ /* ****************************************************************** */ union clause ast = C_NOP : unit -mapping clause encdec_compressed = C_NOP() - <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01 +mapping clause encdec_compressed = C_NOP() if extensionEnabled(Ext_C) + <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01 if extensionEnabled(Ext_C) function clause execute C_NOP() = RETIRE_SUCCESS @@ -29,9 +29,9 @@ mapping clause assembly = C_NOP() <-> "c.nop" union clause ast = C_ADDI4SPN : (cregidx, bits(8)) mapping clause encdec_compressed = C_ADDI4SPN(rd, nz96 @ nz54 @ nz3 @ nz2) - if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 + if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 & extensionEnabled(Ext_C) <-> 0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregidx @ 0b00 - if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 + if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 & extensionEnabled(Ext_C) function clause execute (C_ADDI4SPN(rdc, nzimm)) = { let imm : bits(12) = (0b00 @ nzimm @ 0b00); @@ -47,8 +47,8 @@ mapping clause assembly = C_ADDI4SPN(rdc, nzimm) /* ****************************************************************** */ union clause ast = C_LW : (bits(5), cregidx, cregidx) -mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd) - <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 +mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd) if extensionEnabled(Ext_C) + <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 if extensionEnabled(Ext_C) function clause execute (C_LW(uimm, rsc, rdc)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); @@ -64,9 +64,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc) union clause ast = C_LD : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_LD(uimm, rsc, rdc)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -83,8 +83,8 @@ mapping clause assembly = C_LD(uimm, rsc, rdc) /* ****************************************************************** */ union clause ast = C_SW : (bits(5), cregidx, cregidx) -mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2) - <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 +mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2) if extensionEnabled(Ext_C) + <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 if extensionEnabled(Ext_C) function clause execute (C_SW(uimm, rsc1, rsc2)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); @@ -100,9 +100,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2) union clause ast = C_SD : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_SD(uimm, rsc1, rsc2)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -120,9 +120,9 @@ mapping clause assembly = C_SD(uimm, rsc1, rsc2) union clause ast = C_ADDI : (bits(6), regidx) mapping clause encdec_compressed = C_ADDI(nzi5 @ nzi40, rsd) - if nzi5 @ nzi40 != 0b000000 & rsd != zreg + if nzi5 @ nzi40 != 0b000000 & rsd != zreg & extensionEnabled(Ext_C) <-> 0b000 @ nzi5 : bits(1) @ rsd : regidx @ nzi40 : bits(5) @ 0b01 - if nzi5 @ nzi40 != 0b000000 & rsd != zreg + if nzi5 @ nzi40 != 0b000000 & rsd != zreg & extensionEnabled(Ext_C) function clause execute (C_ADDI(nzi, rsd)) = { let imm : bits(12) = sign_extend(nzi); @@ -138,9 +138,9 @@ mapping clause assembly = C_ADDI(nzi, rsd) union clause ast = C_JAL : (bits(11)) mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) - if sizeof(xlen) == 32 + if sizeof(xlen) == 32 & extensionEnabled(Ext_C) <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 - if sizeof(xlen) == 32 + if sizeof(xlen) == 32 & extensionEnabled(Ext_C) function clause execute (C_JAL(imm)) = execute(RISCV_JAL(sign_extend(imm @ 0b0), ra)) @@ -154,9 +154,9 @@ mapping clause assembly = C_JAL(imm) union clause ast = C_ADDIW : (bits(6), regidx) mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) - if rsd != zreg & sizeof(xlen) == 64 + if rsd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b001 @ imm5 : bits(1) @ rsd : regidx @ imm40 : bits(5) @ 0b01 - if rsd != zreg & sizeof(xlen) == 64 + if rsd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_ADDIW(imm, rsd)) = execute(ADDIW(sign_extend(imm), rsd, rsd)) @@ -170,9 +170,9 @@ mapping clause assembly = C_ADDIW(imm, rsd) union clause ast = C_LI : (bits(6), regidx) mapping clause encdec_compressed = C_LI(imm5 @ imm40, rd) - if rd != zreg + if rd != zreg & extensionEnabled(Ext_C) <-> 0b010 @ imm5 : bits(1) @ rd : regidx @ imm40 : bits(5) @ 0b01 - if rd != zreg + if rd != zreg & extensionEnabled(Ext_C) function clause execute (C_LI(imm, rd)) = { let imm : bits(12) = sign_extend(imm); @@ -188,9 +188,9 @@ mapping clause assembly = C_LI(imm, rd) union clause ast = C_ADDI16SP : (bits(6)) mapping clause encdec_compressed = C_ADDI16SP(nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4) - if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 + if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 & extensionEnabled(Ext_C) <-> 0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01 - if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 + if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 & extensionEnabled(Ext_C) function clause execute (C_ADDI16SP(imm)) = { let imm : bits(12) = sign_extend(imm @ 0x0); @@ -206,9 +206,9 @@ mapping clause assembly = C_ADDI16SP(imm) union clause ast = C_LUI : (bits(6), regidx) mapping clause encdec_compressed = C_LUI(imm17 @ imm1612, rd) - if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 + if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 & extensionEnabled(Ext_C) <-> 0b011 @ imm17 : bits(1) @ rd : regidx @ imm1612 : bits(5) @ 0b01 - if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 + if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 & extensionEnabled(Ext_C) function clause execute (C_LUI(imm, rd)) = { let res : bits(20) = sign_extend(imm); @@ -224,9 +224,9 @@ mapping clause assembly = C_LUI(imm, rd) union clause ast = C_SRLI : (bits(6), cregidx) mapping clause encdec_compressed = C_SRLI(nzui5 @ nzui40, rsd) - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) + if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C) <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01 - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) + if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C) function clause execute (C_SRLI(shamt, rsd)) = { let rsd = creg2reg_idx(rsd); @@ -242,9 +242,9 @@ mapping clause assembly = C_SRLI(shamt, rsd) union clause ast = C_SRAI : (bits(6), cregidx) mapping clause encdec_compressed = C_SRAI(nzui5 @ nzui40, rsd) - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) + if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C) <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01 - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) + if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C) function clause execute (C_SRAI(shamt, rsd)) = { let rsd = creg2reg_idx(rsd); @@ -259,8 +259,8 @@ mapping clause assembly = C_SRAI(shamt, rsd) /* ****************************************************************** */ union clause ast = C_ANDI : (bits(6), cregidx) -mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd) - <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01 +mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd) if extensionEnabled(Ext_C) + <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_ANDI(imm, rsd)) = { let rsd = creg2reg_idx(rsd); @@ -273,8 +273,8 @@ mapping clause assembly = C_ANDI(imm, rsd) /* ****************************************************************** */ union clause ast = C_SUB : (cregidx, cregidx) -mapping clause encdec_compressed = C_SUB(rsd, rs2) - <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01 +mapping clause encdec_compressed = C_SUB(rsd, rs2) if extensionEnabled(Ext_C) + <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_SUB(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -288,8 +288,8 @@ mapping clause assembly = C_SUB(rsd, rs2) /* ****************************************************************** */ union clause ast = C_XOR : (cregidx, cregidx) -mapping clause encdec_compressed = C_XOR(rsd, rs2) - <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01 +mapping clause encdec_compressed = C_XOR(rsd, rs2) if extensionEnabled(Ext_C) + <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_XOR(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -303,8 +303,8 @@ mapping clause assembly = C_XOR(rsd, rs2) /* ****************************************************************** */ union clause ast = C_OR : (cregidx, cregidx) -mapping clause encdec_compressed = C_OR(rsd, rs2) - <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01 +mapping clause encdec_compressed = C_OR(rsd, rs2) if extensionEnabled(Ext_C) + <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_OR(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -318,8 +318,8 @@ mapping clause assembly = C_OR(rsd, rs2) /* ****************************************************************** */ union clause ast = C_AND : (cregidx, cregidx) -mapping clause encdec_compressed = C_AND(rsd, rs2) - <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01 +mapping clause encdec_compressed = C_AND(rsd, rs2) if extensionEnabled(Ext_C) + <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_AND(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -334,9 +334,9 @@ mapping clause assembly = C_AND(rsd, rs2) union clause ast = C_SUBW : (cregidx, cregidx) mapping clause encdec_compressed = C_SUBW(rsd, rs2) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_SUBW(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -353,9 +353,9 @@ mapping clause assembly = C_SUBW(rsd, rs2) union clause ast = C_ADDW : (cregidx, cregidx) mapping clause encdec_compressed = C_ADDW(rsd, rs2) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_ADDW(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -371,8 +371,8 @@ mapping clause assembly = C_ADDW(rsd, rs2) /* ****************************************************************** */ union clause ast = C_J : (bits(11)) -mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) - <-> 0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 +mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) if extensionEnabled(Ext_C) + <-> 0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_J(imm)) = execute(RISCV_JAL(sign_extend(imm @ 0b0), zreg)) @@ -383,8 +383,8 @@ mapping clause assembly = C_J(imm) /* ****************************************************************** */ union clause ast = C_BEQZ : (bits(8), cregidx) -mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs) - <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 +mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs) if extensionEnabled(Ext_C) + <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_BEQZ(imm, rs)) = execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ)) @@ -395,8 +395,8 @@ mapping clause assembly = C_BEQZ(imm, rs) /* ****************************************************************** */ union clause ast = C_BNEZ : (bits(8), cregidx) -mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs) - <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 +mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs) if extensionEnabled(Ext_C) + <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 if extensionEnabled(Ext_C) function clause execute (C_BNEZ(imm, rs)) = execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE)) @@ -408,9 +408,9 @@ mapping clause assembly = C_BNEZ(imm, rs) union clause ast = C_SLLI : (bits(6), regidx) mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd) - if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) + if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C) <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10 - if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) + if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_C) function clause execute (C_SLLI(shamt, rsd)) = execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI)) @@ -424,9 +424,9 @@ mapping clause assembly = C_SLLI(shamt, rsd) union clause ast = C_LWSP : (bits(6), regidx) mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd) - if rd != zreg + if rd != zreg & extensionEnabled(Ext_C) <-> 0b010 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10 - if rd != zreg + if rd != zreg & extensionEnabled(Ext_C) function clause execute (C_LWSP(uimm, rd)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); @@ -442,9 +442,9 @@ mapping clause assembly = C_LWSP(uimm, rd) union clause ast = C_LDSP : (bits(6), regidx) mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd) - if rd != zreg & sizeof(xlen) == 64 + if rd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if rd != zreg & sizeof(xlen) == 64 + if rd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_LDSP(uimm, rd)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -460,7 +460,9 @@ mapping clause assembly = C_LDSP(uimm, rd) union clause ast = C_SWSP : (bits(6), regidx) mapping clause encdec_compressed = C_SWSP(ui76 @ ui52, rs2) + if extensionEnabled(Ext_C) <-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10 + if extensionEnabled(Ext_C) function clause execute (C_SWSP(uimm, rs2)) = { let imm : bits(12) = zero_extend(uimm @ 0b00); @@ -474,9 +476,9 @@ mapping clause assembly = C_SWSP(uimm, rs2) union clause ast = C_SDSP : (bits(6), regidx) mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2) - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10 - if sizeof(xlen) == 64 + if sizeof(xlen) == 64 & extensionEnabled(Ext_C) function clause execute (C_SDSP(uimm, rs2)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -492,9 +494,9 @@ mapping clause assembly = C_SDSP(uimm, rs2) union clause ast = C_JR : (regidx) mapping clause encdec_compressed = C_JR(rs1) - if rs1 != zreg + if rs1 != zreg & extensionEnabled(Ext_C) <-> 0b100 @ 0b0 @ rs1 : regidx @ 0b00000 @ 0b10 - if rs1 != zreg + if rs1 != zreg & extensionEnabled(Ext_C) function clause execute (C_JR(rs1)) = execute(RISCV_JALR(zero_extend(0b0), rs1, zreg)) @@ -508,9 +510,9 @@ mapping clause assembly = C_JR(rs1) union clause ast = C_JALR : (regidx) mapping clause encdec_compressed = C_JALR(rs1) - if rs1 != zreg + if rs1 != zreg & extensionEnabled(Ext_C) <-> 0b100 @ 0b1 @ rs1 : regidx @ 0b00000 @ 0b10 - if rs1 != zreg + if rs1 != zreg & extensionEnabled(Ext_C) function clause execute (C_JALR(rs1)) = execute(RISCV_JALR(zero_extend(0b0), rs1, ra)) @@ -524,9 +526,9 @@ mapping clause assembly = C_JALR(rs1) union clause ast = C_MV : (regidx, regidx) mapping clause encdec_compressed = C_MV(rd, rs2) - if rd != zreg & rs2 != zreg + if rd != zreg & rs2 != zreg & extensionEnabled(Ext_C) <-> 0b100 @ 0b0 @ rd : regidx @ rs2 : regidx @ 0b10 - if rd != zreg & rs2 != zreg + if rd != zreg & rs2 != zreg & extensionEnabled(Ext_C) function clause execute (C_MV(rd, rs2)) = execute(RTYPE(rs2, zreg, rd, RISCV_ADD)) @@ -539,8 +541,8 @@ mapping clause assembly = C_MV(rd, rs2) /* ****************************************************************** */ union clause ast = C_EBREAK : unit -mapping clause encdec_compressed = C_EBREAK() - <-> 0b100 @ 0b1 @ 0b00000 @ 0b00000 @ 0b10 +mapping clause encdec_compressed = C_EBREAK() if extensionEnabled(Ext_C) + <-> 0b100 @ 0b1 @ 0b00000 @ 0b00000 @ 0b10 if extensionEnabled(Ext_C) function clause execute C_EBREAK() = execute(EBREAK()) @@ -551,9 +553,9 @@ mapping clause assembly = C_EBREAK() <-> "c.ebreak" union clause ast = C_ADD : (regidx, regidx) mapping clause encdec_compressed = C_ADD(rsd, rs2) - if rsd != zreg & rs2 != zreg + if rsd != zreg & rs2 != zreg & extensionEnabled(Ext_C) <-> 0b100 @ 0b1 @ rsd : regidx @ rs2 : regidx @ 0b10 - if rsd != zreg & rs2 != zreg + if rsd != zreg & rs2 != zreg & extensionEnabled(Ext_C) function clause execute (C_ADD(rsd, rs2)) = execute(RTYPE(rs2, rsd, rsd, RISCV_ADD)) diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail index 71b1e0b25..976425d53 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 & extensionEnabled(Ext_C) & 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 & extensionEnabled(Ext_C) & 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 & extensionEnabled(Ext_C) & extensionEnabled(Ext_F) <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & extensionEnabled(Ext_C) & 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 & extensionEnabled(Ext_C) & 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 & extensionEnabled(Ext_C) & 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 & extensionEnabled(Ext_C) & 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 & extensionEnabled(Ext_C) & 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..f366c487a 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -224,13 +224,16 @@ function fle_D (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveDoubleFPU() -> bool = haveDExt() | haveZdinx() +enum clause extension = 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 @@ -902,11 +905,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..d9167a109 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -27,6 +27,7 @@ mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s) /* ****************************************************************** */ /* End definitions */ +end extensions end ast end execute end assembly diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 5c89e9188..3a5509ea4 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -25,6 +25,9 @@ /* **************************************************************** */ +enum clause extension = 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) | extensionEnabled(Ext_Zfinx) /* ****************************************************************** */ /* 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_mext.sail b/model/riscv_insts_mext.sail index cfac3bb31..b153e792b 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -11,6 +11,12 @@ /* ****************************************************************** */ +enum clause extension = Ext_M +function clause extensionEnabled(Ext_M) = misa[M] == 0b1 +enum clause extension = Ext_Zmmul +function clause extensionEnabled(Ext_Zmmul) = true + + union clause ast = MUL : (regidx, regidx, regidx, mul_op) mapping encdec_mul_op : mul_op <-> bits(3) = { @@ -20,8 +26,8 @@ mapping encdec_mul_op : mul_op <-> bits(3) = { struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011 } -mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if haveMulDiv() | haveZmmul() - <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul() +mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul) + <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul) function clause execute (MUL(rs2, rs1, rd, mul_op)) = { let rs1_val = X(rs1); @@ -49,8 +55,8 @@ mapping clause assembly = MUL(rs2, rs1, rd, mul_op) /* ****************************************************************** */ union clause ast = DIV : (regidx, regidx, regidx, bool) -mapping clause encdec = DIV(rs2, rs1, rd, s) if haveMulDiv() - <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv() +mapping clause encdec = DIV(rs2, rs1, rd, s) if extensionEnabled(Ext_M) + <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if extensionEnabled(Ext_M) function clause execute (DIV(rs2, rs1, rd, s)) = { let rs1_val = X(rs1); @@ -75,8 +81,8 @@ mapping clause assembly = DIV(rs2, rs1, rd, s) /* ****************************************************************** */ union clause ast = REM : (regidx, regidx, regidx, bool) -mapping clause encdec = REM(rs2, rs1, rd, s) if haveMulDiv() - <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv() +mapping clause encdec = REM(rs2, rs1, rd, s) if extensionEnabled(Ext_M) + <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if extensionEnabled(Ext_M) function clause execute (REM(rs2, rs1, rd, s)) = { let rs1_val = X(rs1); @@ -96,9 +102,9 @@ mapping clause assembly = REM(rs2, rs1, rd, s) union clause ast = MULW : (regidx, regidx, regidx) mapping clause encdec = MULW(rs2, rs1, rd) - if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul()) + if sizeof(xlen) == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul()) + if sizeof(xlen) == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) function clause execute (MULW(rs2, rs1, rd)) = { let rs1_val = X(rs1)[31..0]; @@ -121,9 +127,9 @@ mapping clause assembly = MULW(rs2, rs1, rd) union clause ast = DIVW : (regidx, regidx, regidx, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 & haveMulDiv() + if sizeof(xlen) == 64 & extensionEnabled(Ext_M) <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 - if sizeof(xlen) == 64 & haveMulDiv() + if sizeof(xlen) == 64 & extensionEnabled(Ext_M) function clause execute (DIVW(rs2, rs1, rd, s)) = { let rs1_val = X(rs1)[31..0]; @@ -146,9 +152,9 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s) union clause ast = REMW : (regidx, regidx, regidx, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 & haveMulDiv() + if sizeof(xlen) == 64 & extensionEnabled(Ext_M) <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 - if sizeof(xlen) == 64 & haveMulDiv() + if sizeof(xlen) == 64 & extensionEnabled(Ext_M) function clause execute (REMW(rs2, rs1, rd, s)) = { let rs1_val = X(rs1)[31..0]; diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index dd9197adb..52d8bc26d 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -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() diff --git a/model/riscv_insts_svinval.sail b/model/riscv_insts_svinval.sail index 168fb17ff..2816fdc14 100644 --- a/model/riscv_insts_svinval.sail +++ b/model/riscv_insts_svinval.sail @@ -6,11 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extension = 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)) @@ -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 @@ -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 diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 6104e7ee4..b351b01bb 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -40,8 +40,8 @@ mapping encdec_vvfunct6 : vvfunct6 <-> bits(6) = { VV_VSSRA <-> 0b101011 } -mapping clause encdec = VVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_vvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_pow = get_sew_pow(); @@ -174,8 +174,8 @@ mapping encdec_nvsfunct6 : nvsfunct6 <-> bits(6) = { NVS_VNSRA <-> 0b101101 } -mapping clause encdec = NVSTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_nvsfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = NVSTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_nvsfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -241,8 +241,8 @@ mapping encdec_nvfunct6 : nvfunct6 <-> bits(6) = { NV_VNCLIP <-> 0b101111 } -mapping clause encdec = NVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_nvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = NVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_nvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -303,8 +303,8 @@ mapping clause assembly = NVTYPE(funct6, vm, vs2, vs1, vd) /* ********************** OPIVV (Integer Merge Instruction) ********************** */ union clause ast = MASKTYPEV : (regidx, regidx, regidx) -mapping clause encdec = MASKTYPEV (vs2, vs1, vd) if haveVExt() - <-> 0b010111 @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MASKTYPEV (vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MASKTYPEV(vs2, vs1, vd)) = { let start_element = get_start_element(); @@ -351,8 +351,8 @@ mapping clause assembly = MASKTYPEV(vs2, vs1, vd) /* ********************** OPIVV (Integer Move Instruction) *********************** */ union clause ast = MOVETYPEV : (regidx, regidx) -mapping clause encdec = MOVETYPEV (vs1, vd) if haveVExt() - <-> 0b010111 @ 0b1 @ 0b00000 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MOVETYPEV (vs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b1 @ 0b00000 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MOVETYPEV(vs1, vd)) = { let SEW = get_sew(); @@ -410,8 +410,8 @@ mapping encdec_vxfunct6 : vxfunct6 <-> bits(6) = { VX_VSSRA <-> 0b101011 } -mapping clause encdec = VXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_vxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -526,8 +526,8 @@ mapping encdec_nxsfunct6 : nxsfunct6 <-> bits(6) = { NXS_VNSRA <-> 0b101101 } -mapping clause encdec = NXSTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_nxsfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = NXSTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_nxsfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -593,8 +593,8 @@ mapping encdec_nxfunct6 : nxfunct6 <-> bits(6) = { NX_VNCLIP <-> 0b101111 } -mapping clause encdec = NXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_nxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = NXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_nxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -662,8 +662,8 @@ mapping encdec_vxsgfunct6 : vxsgfunct6 <-> bits(6) = { VX_VRGATHER <-> 0b001100 } -mapping clause encdec = VXSG(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_vxsgfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VXSG(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vxsgfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let SEW_pow = get_sew_pow(); @@ -725,8 +725,8 @@ mapping clause assembly = VXSG(funct6, vm, vs2, rs1, vd) /* ********************** OPIVX (Integer Merge Instruction) ********************** */ union clause ast = MASKTYPEX : (regidx, regidx, regidx) -mapping clause encdec = MASKTYPEX(vs2, rs1, vd) if haveVExt() - <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MASKTYPEX(vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MASKTYPEX(vs2, rs1, vd)) = { let start_element = get_start_element(); @@ -773,8 +773,8 @@ mapping clause assembly = MASKTYPEX(vs2, rs1, vd) /* ********************** OPIVX (Integer Move Instruction) *********************** */ union clause ast = MOVETYPEX : (regidx, regidx) -mapping clause encdec = MOVETYPEX (rs1, vd) if haveVExt() - <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MOVETYPEX (rs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MOVETYPEX(rs1, vd)) = { let SEW = get_sew(); @@ -824,8 +824,8 @@ mapping encdec_vifunct6 : vifunct6 <-> bits(6) = { VI_VSSRA <-> 0b101011 } -mapping clause encdec = VITYPE(funct6, vm, vs2, simm, vd) if haveVExt() - <-> encdec_vifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VITYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_vifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let SEW = get_sew(); @@ -916,8 +916,8 @@ mapping encdec_nisfunct6 : nisfunct6 <-> bits(6) = { NIS_VNSRA <-> 0b101101 } -mapping clause encdec = NISTYPE(funct6, vm, vs2, simm, vd) if haveVExt() - <-> encdec_nisfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = NISTYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_nisfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let SEW = get_sew(); @@ -983,8 +983,8 @@ mapping encdec_nifunct6 : nifunct6 <-> bits(6) = { NI_VNCLIP <-> 0b101111 } -mapping clause encdec = NITYPE(funct6, vm, vs2, simm, vd) if haveVExt() - <-> encdec_nifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = NITYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_nifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let SEW = get_sew(); @@ -1052,8 +1052,8 @@ mapping encdec_visgfunct6 : visgfunct6 <-> bits(6) = { VI_VRGATHER <-> 0b001100 } -mapping clause encdec = VISG(funct6, vm, vs2, simm, vd) if haveVExt() - <-> encdec_visgfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VISG(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_visgfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let SEW_pow = get_sew_pow(); @@ -1115,8 +1115,8 @@ mapping clause assembly = VISG(funct6, vm, vs2, simm, vd) /* ********************** OPIVI (Integer Merge Instruction) ********************** */ union clause ast = MASKTYPEI : (regidx, bits(5), regidx) -mapping clause encdec = MASKTYPEI(vs2, simm, vd) if haveVExt() - <-> 0b010111 @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MASKTYPEI(vs2, simm, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MASKTYPEI(vs2, simm, vd)) = { let start_element = get_start_element(); @@ -1163,8 +1163,8 @@ mapping clause assembly = MASKTYPEI(vs2, simm, vd) /* ********************** OPIVI (Integer Move Instruction) *********************** */ union clause ast = MOVETYPEI : (regidx, bits(5)) -mapping clause encdec = MOVETYPEI (vd, simm) if haveVExt() - <-> 0b010111 @ 0b1 @ 0b00000 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MOVETYPEI (vd, simm) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b1 @ 0b00000 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MOVETYPEI(vd, simm)) = { let SEW = get_sew(); @@ -1199,8 +1199,8 @@ mapping clause assembly = MOVETYPEI(vd, simm) /* ********************* OPIVI (Whole Vector Register Move) ********************** */ union clause ast = VMVRTYPE : (regidx, bits(5), regidx) -mapping clause encdec = VMVRTYPE(vs2, simm, vd) if haveVExt() - <-> 0b100111 @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VMVRTYPE(vs2, simm, vd) if extensionEnabled(Ext_V) + <-> 0b100111 @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMVRTYPE(vs2, simm, vd)) = { let start_element = get_start_element(); @@ -1257,8 +1257,8 @@ mapping encdec_mvvfunct6 : mvvfunct6 <-> bits(6) = { MVV_VREM <-> 0b100011 } -mapping clause encdec = MVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_mvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_mvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -1366,8 +1366,8 @@ mapping encdec_mvvmafunct6 : mvvmafunct6 <-> bits(6) = { MVV_VNMSUB <-> 0b101011 } -mapping clause encdec = MVVMATYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_mvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MVVMATYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_mvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -1426,8 +1426,8 @@ mapping encdec_wvvfunct6 : wvvfunct6 <-> bits(6) = { WVV_VWMULSU <-> 0b111010 } -mapping clause encdec = WVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_wvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = WVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_wvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -1496,8 +1496,8 @@ mapping encdec_wvfunct6 : wvfunct6 <-> bits(6) = { WV_VSUBU <-> 0b110110 } -mapping clause encdec = WVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_wvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = WVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_wvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -1559,8 +1559,8 @@ mapping encdec_wmvvfunct6 : wmvvfunct6 <-> bits(6) = { WMVV_VWMACCSU <-> 0b111111 } -mapping clause encdec = WMVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_wmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = WMVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_wmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -1620,8 +1620,8 @@ mapping vext2_vs1 : vext2funct6 <-> bits(5) = { VEXT2_SVF2 <-> 0b00111 } -mapping clause encdec = VEXT2TYPE(funct6, vm, vs2, vd) if haveVExt() - <-> 0b010010 @ vm @ vs2 @ vext2_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VEXT2TYPE(funct6, vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010010 @ vm @ vs2 @ vext2_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { let SEW = get_sew(); @@ -1678,8 +1678,8 @@ mapping vext4_vs1 : vext4funct6 <-> bits(5) = { VEXT4_SVF4 <-> 0b00101 } -mapping clause encdec = VEXT4TYPE(funct6, vm, vs2, vd) if haveVExt() - <-> 0b010010 @ vm @ vs2 @ vext4_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VEXT4TYPE(funct6, vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010010 @ vm @ vs2 @ vext4_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { let SEW = get_sew(); @@ -1736,8 +1736,8 @@ mapping vext8_vs1 : vext8funct6 <-> bits(5) = { VEXT8_SVF8 <-> 0b00011 } -mapping clause encdec = VEXT8TYPE(funct6, vm, vs2, vd) if haveVExt() - <-> 0b010010 @ vm @ vs2 @ vext8_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VEXT8TYPE(funct6, vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010010 @ vm @ vs2 @ vext8_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { let SEW = get_sew(); @@ -1788,8 +1788,8 @@ mapping clause assembly = VEXT8TYPE(funct6, vm, vs2, vd) /* ************************ OPMVV (vmv.x.s in VWXUNARY0) ************************* */ union clause ast = VMVXS : (regidx, regidx) -mapping clause encdec = VMVXS(vs2, rd) if haveVExt() - <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b010 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VMVXS(vs2, rd) if extensionEnabled(Ext_V) + <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b010 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMVXS(vs2, rd)) = { let SEW = get_sew(); @@ -1816,8 +1816,8 @@ mapping clause assembly = VMVXS(vs2, rd) /* ********************* OPMVV (Vector Compress Instruction) ********************* */ union clause ast = MVVCOMPRESS : (regidx, regidx, regidx) -mapping clause encdec = MVVCOMPRESS(vs2, vs1, vd) if haveVExt() - <-> 0b010111 @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MVVCOMPRESS(vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { let start_element = get_start_element(); @@ -1890,8 +1890,8 @@ mapping encdec_mvxfunct6 : mvxfunct6 <-> bits(6) = { MVX_VREM <-> 0b100011 } -mapping clause encdec = MVXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_mvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MVXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_mvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -2010,8 +2010,8 @@ mapping encdec_mvxmafunct6 : mvxmafunct6 <-> bits(6) = { MVX_VNMSUB <-> 0b101011 } -mapping clause encdec = MVXMATYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_mvxmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MVXMATYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_mvxmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -2071,8 +2071,8 @@ mapping encdec_wvxfunct6 : wvxfunct6 <-> bits(6) = { WVX_VWMULSU <-> 0b111010 } -mapping clause encdec = WVXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_wvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = WVXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_wvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -2140,8 +2140,8 @@ mapping encdec_wxfunct6 : wxfunct6 <-> bits(6) = { WX_VSUBU <-> 0b110110 } -mapping clause encdec = WXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_wxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = WXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_wxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -2203,8 +2203,8 @@ mapping encdec_wmvxfunct6 : wmvxfunct6 <-> bits(6) = { WMVX_VWMACCSU <-> 0b111111 } -mapping clause encdec = WMVXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_wmvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = WMVXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_wmvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -2259,8 +2259,8 @@ mapping clause assembly = WMVXTYPE(funct6, vm, vs2, rs1, vd) /* ****************************** OPMVX (VRXUNARY0) ****************************** */ union clause ast = VMVSX : (regidx, regidx) -mapping clause encdec = VMVSX(rs1, vd) if haveVExt() - <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VMVSX(rs1, vd) if extensionEnabled(Ext_V) + <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMVSX(rs1, vd)) = { let SEW = get_sew(); diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 0b36b01b6..945199da8 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -27,8 +27,8 @@ mapping encdec_fvvfunct6 : fvvfunct6 <-> bits(6) = { FVV_VMUL <-> 0b100100 } -mapping clause encdec = FVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -102,8 +102,8 @@ mapping encdec_fvvmafunct6 : fvvmafunct6 <-> bits(6) = { FVV_VNMSAC <-> 0b101111 } -mapping clause encdec = FVVMATYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FVVMATYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -169,8 +169,8 @@ mapping encdec_fwvvfunct6 : fwvvfunct6 <-> bits(6) = { FWVV_VMUL <-> 0b111000 } -mapping clause encdec = FWVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FWVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -234,8 +234,8 @@ mapping encdec_fwvvmafunct6 : fwvvmafunct6 <-> bits(6) = { FWVV_VNMSAC <-> 0b111111 } -mapping clause encdec = FWVVMATYPE(funct6, vm, vs1, vs2, vd) if haveVExt() - <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FWVVMATYPE(funct6, vm, vs1, vs2, vd) if extensionEnabled(Ext_V) + <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { let rm_3b = fcsr[FRM]; @@ -298,8 +298,8 @@ mapping encdec_fwvfunct6 : fwvfunct6 <-> bits(6) = { FWV_VSUB <-> 0b110110 } -mapping clause encdec = FWVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FWVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -361,8 +361,8 @@ mapping encdec_vfunary0_vs1 : vfunary0 <-> bits(5) = { FV_CVT_RTZ_X_F <-> 0b00111 } -mapping clause encdec = VFUNARY0(vm, vs2, vfunary0, vd) if haveVExt() - <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFUNARY0(vm, vs2, vfunary0, vd) if extensionEnabled(Ext_V) + <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { let rm_3b = fcsr[FRM]; @@ -475,8 +475,8 @@ mapping encdec_vfwunary0_vs1 : vfwunary0 <-> bits(5) = { FWV_CVT_RTZ_X_F <-> 0b01111 } -mapping clause encdec = VFWUNARY0(vm, vs2, vfwunary0, vd) if haveVExt() - <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFWUNARY0(vm, vs2, vfwunary0, vd) if extensionEnabled(Ext_V) + <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { let rm_3b = fcsr[FRM]; @@ -605,8 +605,8 @@ mapping encdec_vfnunary0_vs1 : vfnunary0 <-> bits(5) = { FNV_CVT_RTZ_X_F <-> 0b10111 } -mapping clause encdec = VFNUNARY0(vm, vs2, vfnunary0, vd) if haveVExt() - <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFNUNARY0(vm, vs2, vfnunary0, vd) if extensionEnabled(Ext_V) + <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { let rm_3b = fcsr[FRM]; @@ -741,8 +741,8 @@ mapping encdec_vfunary1_vs1 : vfunary1 <-> bits(5) = { FVV_VCLASS <-> 0b10000 } -mapping clause encdec = VFUNARY1(vm, vs2, vfunary1, vd) if haveVExt() - <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFUNARY1(vm, vs2, vfunary1, vd) if extensionEnabled(Ext_V) + <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { let rm_3b = fcsr[FRM]; @@ -817,8 +817,8 @@ mapping clause assembly = VFUNARY1(vm, vs2, vfunary1, vd) /* ****************************** OPFVV (VWFUNARY0) ****************************** */ union clause ast = VFMVFS : (regidx, regidx) -mapping clause encdec = VFMVFS(vs2, rd) if haveVExt() - <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VFMVFS(vs2, rd) if extensionEnabled(Ext_V) + <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFMVFS(vs2, rd)) = { let rm_3b = fcsr[FRM]; @@ -865,8 +865,8 @@ mapping encdec_fvffunct6 : fvffunct6 <-> bits(6) = { VF_VRSUB <-> 0b100111 } -mapping clause encdec = FVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FVFTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -955,8 +955,8 @@ mapping encdec_fvfmafunct6 : fvfmafunct6 <-> bits(6) = { VF_VNMSAC <-> 0b101111 } -mapping clause encdec = FVFMATYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FVFMATYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -1022,8 +1022,8 @@ mapping encdec_fwvffunct6 : fwvffunct6 <-> bits(6) = { FWVF_VMUL <-> 0b111000 } -mapping clause encdec = FWVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FWVFTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -1086,8 +1086,8 @@ mapping encdec_fwvfmafunct6 : fwvfmafunct6 <-> bits(6) = { FWVF_VNMSAC <-> 0b111111 } -mapping clause encdec = FWVFMATYPE(funct6, vm, rs1, vs2, vd) if haveVExt() - <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FWVFMATYPE(funct6, vm, rs1, vs2, vd) if extensionEnabled(Ext_V) + <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { let rm_3b = fcsr[FRM]; @@ -1149,8 +1149,8 @@ mapping encdec_fwffunct6 : fwffunct6 <-> bits(6) = { FWF_VSUB <-> 0b110110 } -mapping clause encdec = FWFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FWFTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -1203,8 +1203,8 @@ mapping clause assembly = FWFTYPE(funct6, vm, vs2, rs1, vd) /* This instruction operates on all body elements regardless of mask value */ union clause ast = VFMERGE : (regidx, regidx, regidx) -mapping clause encdec = VFMERGE(vs2, rs1, vd) if haveVExt() - <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFMERGE(vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFMERGE(vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -1254,8 +1254,8 @@ mapping clause assembly = VFMERGE(vs2, rs1, vd) /* This instruction shares the encoding with vfmerge.vfm, but with vm=1 and vs2=v0 */ union clause ast = VFMV : (regidx, regidx) -mapping clause encdec = VFMV(rs1, vd) if haveVExt() - <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFMV(rs1, vd) if extensionEnabled(Ext_V) + <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFMV(rs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -1292,8 +1292,8 @@ mapping clause assembly = VFMV(rs1, vd) /* ****************************** OPFVF (VRFUNARY0) ****************************** */ union clause ast = VFMVSF : (regidx, regidx) -mapping clause encdec = VFMVSF(rs1, vd) if haveVExt() - <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VFMVSF(rs1, vd) if extensionEnabled(Ext_V) + <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFMVSF(rs1, vd)) = { let rm_3b = fcsr[FRM]; diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index f04ae1acb..241e210fd 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -25,8 +25,8 @@ mapping encdec_mmfunct6 : mmfunct6 <-> bits(6) = { MM_VMXNOR <-> 0b011111 } -mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if haveVExt() - <-> encdec_mmfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_mmfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -83,8 +83,8 @@ mapping clause assembly = MMTYPE(funct6, vs2, vs1, vd) /* ************************* OPMVV (vpopc in VWXUNARY0) ************************** */ union clause ast = VCPOP_M : (bits(1), regidx, regidx) -mapping clause encdec = VCPOP_M(vm, vs2, rd) if haveVExt() - <-> 0b010000 @ vm @ vs2 @ 0b10000 @ 0b010 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V) + <-> 0b010000 @ vm @ vs2 @ 0b10000 @ 0b010 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VCPOP_M(vm, vs2, rd)) = { let SEW = get_sew(); @@ -119,8 +119,8 @@ mapping clause assembly = VCPOP_M(vm, vs2, rd) /* ************************* OPMVV (vfirst in VWXUNARY0) ************************* */ union clause ast = VFIRST_M : (bits(1), regidx, regidx) -mapping clause encdec = VFIRST_M(vm, vs2, rd) if haveVExt() - <-> 0b010000 @ vm @ vs2 @ 0b10001 @ 0b010 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V) + <-> 0b010000 @ vm @ vs2 @ 0b10001 @ 0b010 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VFIRST_M(vm, vs2, rd)) = { let SEW = get_sew(); @@ -157,8 +157,8 @@ mapping clause assembly = VFIRST_M(vm, vs2, rd) /* ************************** OPMVV (vmsbf in VMUNARY0) ************************** */ union clause ast = VMSBF_M : (bits(1), regidx, regidx) -mapping clause encdec = VMSBF_M(vm, vs2, vd) if haveVExt() - <-> 0b010100 @ vm @ vs2 @ 0b00001 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010100 @ vm @ vs2 @ 0b00001 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMSBF_M(vm, vs2, vd)) = { let SEW = get_sew(); @@ -198,8 +198,8 @@ mapping clause assembly = VMSBF_M(vm, vs2, vd) /* ************************** OPMVV (vmsif in VMUNARY0) ************************** */ union clause ast = VMSIF_M : (bits(1), regidx, regidx) -mapping clause encdec = VMSIF_M(vm, vs2, vd) if haveVExt() - <-> 0b010100 @ vm @ vs2 @ 0b00011 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010100 @ vm @ vs2 @ 0b00011 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMSIF_M(vm, vs2, vd)) = { let SEW = get_sew(); @@ -239,8 +239,8 @@ mapping clause assembly = VMSIF_M(vm, vs2, vd) /* ************************** OPMVV (vmsof in VMUNARY0) ************************** */ union clause ast = VMSOF_M : (bits(1), regidx, regidx) -mapping clause encdec = VMSOF_M(vm, vs2, vd) if haveVExt() - <-> 0b010100 @ vm @ vs2 @ 0b00010 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010100 @ vm @ vs2 @ 0b00010 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VMSOF_M(vm, vs2, vd)) = { let SEW = get_sew(); @@ -284,8 +284,8 @@ mapping clause assembly = VMSOF_M(vm, vs2, vd) /* ************************** OPMVV (viota in VMUNARY0) ************************** */ union clause ast = VIOTA_M : (bits(1), regidx, regidx) -mapping clause encdec = VIOTA_M(vm, vs2, vd) if haveVExt() - <-> 0b010100 @ vm @ vs2 @ 0b10000 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VIOTA_M(vm, vs2, vd) if extensionEnabled(Ext_V) + <-> 0b010100 @ vm @ vs2 @ 0b10000 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VIOTA_M(vm, vs2, vd)) = { let SEW = get_sew(); @@ -325,8 +325,8 @@ mapping clause assembly = VIOTA_M(vm, vs2, vd) /* *************************** OPMVV (vid in VMUNARY0) *************************** */ union clause ast = VID_V : (bits(1), regidx) -mapping clause encdec = VID_V(vm, vd) if haveVExt() - <-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VID_V(vm, vd) if extensionEnabled(Ext_V) + <-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VID_V(vm, vd)) = { let SEW = get_sew(); diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 4da82e18f..9ffb56eff 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -64,8 +64,8 @@ mapping vlewidth_pow : vlewidth <-> {3, 4, 5, 6} = { /* ******************** Vector Load Unit-Stride Normal & Segment (mop=0b00, lumop=0b00000) ********************* */ union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) -mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if haveVExt() - <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() +mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { @@ -130,8 +130,8 @@ mapping clause assembly = VLSEGTYPE(nf, vm, rs1, width, vd) /* ************ Vector Load Unit-Stride Normal & Segment Fault-Only-First (mop=0b00, lumop=0b10000) ************ */ union clause ast = VLSEGFFTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) -mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if haveVExt() - <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() +mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { @@ -235,8 +235,8 @@ mapping clause assembly = VLSEGFFTYPE(nf, vm, rs1, width, vd) /* ******************** Vector Store Unit-Stride Normal & Segment (mop=0b00, sumop=0b00000) ******************** */ union clause ast = VSSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) -mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if haveVExt() - <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() +mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { @@ -304,8 +304,8 @@ mapping clause assembly = VSSEGTYPE(nf, vm, rs1, width, vs3) /* ****************************** Vector Load Strided Normal & Segment (mop=0b10) ****************************** */ union clause ast = VLSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx) -mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if haveVExt() - <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() +mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { @@ -371,8 +371,8 @@ mapping clause assembly = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) /* ***************************** Vector Store Strided Normal & Segment (mop=0b10) ****************************** */ union clause ast = VSSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx) -mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if haveVExt() - <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() +mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { @@ -441,8 +441,8 @@ mapping clause assembly = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) /* ************************* Vector Load Indexed Unordered Normal & Segment (mop=0b01) ************************* */ union clause ast = VLUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx) -mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if haveVExt() - <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() +mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { @@ -509,8 +509,8 @@ mapping clause assembly = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) /* ************************** Vector Load Indexed Ordered Normal & Segment (mop=0b11) ************************** */ union clause ast = VLOXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx) -mapping clause encdec = VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd) if haveVExt() - <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() +mapping clause encdec = VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) function clause execute(VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { let EEW_index_pow = vlewidth_pow(width); @@ -533,8 +533,8 @@ mapping clause assembly = VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd) /* ************************ Vector Store Indexed Unordered Normal & Segment (mop=0b01) ************************* */ union clause ast = VSUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx) -mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if haveVExt() - <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() +mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { @@ -604,8 +604,8 @@ mapping clause assembly = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) /* ************************* Vector Store Indexed Ordered Normal & Segment (mop=0b11) ************************** */ union clause ast = VSOXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx) -mapping clause encdec = VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if haveVExt() - <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt() +mapping clause encdec = VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) function clause execute(VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { let EEW_index_pow = vlewidth_pow(width); @@ -628,8 +628,8 @@ mapping clause assembly = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) /* ***************** Vector Load Unit-Stride Whole Register (vm=0b1, mop=0b00, lumop=0b01000) ****************** */ union clause ast = VLRETYPE : (bits(3), regidx, vlewidth, regidx) -mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if haveVExt() - <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt() +mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { @@ -710,8 +710,8 @@ mapping clause assembly = VLRETYPE(nf, rs1, width, vd) /* ***************** Vector Store Unit-Stride Whole Register (vm=0b1, mop=0b00, lumop=0b01000) ***************** */ union clause ast = VSRETYPE : (bits(3), regidx, regidx) -mapping clause encdec = VSRETYPE(nf, rs1, vs3) if haveVExt() - <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if haveVExt() +mapping clause encdec = VSRETYPE(nf, rs1, vs3) if extensionEnabled(Ext_V) + <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { @@ -815,8 +815,8 @@ mapping encdec_lsop : vmlsop <-> bits(7) = { VSM <-> 0b0100111 } -mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if haveVExt() - <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if haveVExt() +mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V) + <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if extensionEnabled(Ext_V) val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 358836b02..1bd7657d5 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -19,8 +19,8 @@ mapping encdec_rivvfunct6 : rivvfunct6 <-> bits(6) = { IVV_VWREDSUM <-> 0b110001 } -mapping clause encdec = RIVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_rivvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = RIVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_rivvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -84,8 +84,8 @@ mapping encdec_rmvvfunct6 : rmvvfunct6 <-> bits(6) = { MVV_VREDMAX <-> 0b000111 } -mapping clause encdec = RMVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_rmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = RMVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_rmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -155,8 +155,8 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = { FVV_VFWREDUSUM <-> 0b110001 } -mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index 1f963e771..745f53e13 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -22,8 +22,8 @@ mapping encdec_vvmfunct6 : vvmfunct6 <-> bits(6) = { VVM_VMSBC <-> 0b010011 } -mapping clause encdec = VVMTYPE(funct6, vs2, vs1, vd) if haveVExt() - <-> encdec_vvmfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VVMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vvmfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -78,8 +78,8 @@ mapping encdec_vvmcfunct6 : vvmcfunct6 <-> bits(6) = { VVMC_VMSBC <-> 0b010011 } -mapping clause encdec = VVMCTYPE(funct6, vs2, vs1, vd) if haveVExt() - <-> encdec_vvmcfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VVMCTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vvmcfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -133,8 +133,8 @@ mapping encdec_vvmsfunct6 : vvmsfunct6 <-> bits(6) = { VVMS_VSBC <-> 0b010010 } -mapping clause encdec = VVMSTYPE(funct6, vs2, vs1, vd) if haveVExt() - <-> encdec_vvmsfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VVMSTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vvmsfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -196,8 +196,8 @@ mapping encdec_vvcmpfunct6 : vvcmpfunct6 <-> bits(6) = { VVCMP_VMSLE <-> 0b011101 } -mapping clause encdec = VVCMPTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_vvcmpfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VVCMPTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vvcmpfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW = get_sew(); @@ -260,8 +260,8 @@ mapping encdec_vxmfunct6 : vxmfunct6 <-> bits(6) = { VXM_VMSBC <-> 0b010011 } -mapping clause encdec = VXMTYPE(funct6, vs2, rs1, vd) if haveVExt() - <-> encdec_vxmfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VXMTYPE(funct6, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vxmfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -316,8 +316,8 @@ mapping encdec_vxmcfunct6 : vxmcfunct6 <-> bits(6) = { VXMC_VMSBC <-> 0b010011 } -mapping clause encdec = VXMCTYPE(funct6, vs2, rs1, vd) if haveVExt() - <-> encdec_vxmcfunct6(funct6) @ 0b1 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VXMCTYPE(funct6, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vxmcfunct6(funct6) @ 0b1 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -371,8 +371,8 @@ mapping encdec_vxmsfunct6 : vxmsfunct6 <-> bits(6) = { VXMS_VSBC <-> 0b010010 } -mapping clause encdec = VXMSTYPE(funct6, vs2, rs1, vd) if haveVExt() - <-> encdec_vxmsfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VXMSTYPE(funct6, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vxmsfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -436,8 +436,8 @@ mapping encdec_vxcmpfunct6 : vxcmpfunct6 <-> bits(6) = { VXCMP_VMSGT <-> 0b011111 } -mapping clause encdec = VXCMPTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_vxcmpfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VXCMPTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_vxcmpfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW = get_sew(); @@ -503,8 +503,8 @@ mapping encdec_vimfunct6 : vimfunct6 <-> bits(6) = { VIM_VMADC <-> 0b010001 /* carry in, carry out */ } -mapping clause encdec = VIMTYPE(funct6, vs2, simm, vd) if haveVExt() - <-> encdec_vimfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VIMTYPE(funct6, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_vimfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let SEW = get_sew(); @@ -556,8 +556,8 @@ mapping encdec_vimcfunct6 : vimcfunct6 <-> bits(6) = { VIMC_VMADC <-> 0b010001 /* carry in, carry out */ } -mapping clause encdec = VIMCTYPE(funct6, vs2, simm, vd) if haveVExt() - <-> encdec_vimcfunct6(funct6) @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VIMCTYPE(funct6, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_vimcfunct6(funct6) @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let SEW = get_sew(); @@ -608,8 +608,8 @@ mapping encdec_vimsfunct6 : vimsfunct6 <-> bits(6) = { VIMS_VADC <-> 0b010000 /* Carry in, no carry out */ } -mapping clause encdec = VIMSTYPE(funct6, vs2, simm, vd) if haveVExt() - <-> encdec_vimsfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VIMSTYPE(funct6, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_vimsfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let SEW = get_sew(); @@ -669,8 +669,8 @@ mapping encdec_vicmpfunct6 : vicmpfunct6 <-> bits(6) = { VICMP_VMSGT <-> 0b011111 } -mapping clause encdec = VICMPTYPE(funct6, vm, vs2, simm, vd) if haveVExt() - <-> encdec_vicmpfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = VICMPTYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V) + <-> encdec_vicmpfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let SEW = get_sew(); @@ -733,8 +733,8 @@ mapping encdec_fvvmfunct6 : fvvmfunct6 <-> bits(6) = { FVVM_VMFNE <-> 0b011100 } -mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if haveVExt() - <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { let rm_3b = fcsr[FRM]; @@ -797,8 +797,8 @@ mapping encdec_fvfmfunct6 : fvfmfunct6 <-> bits(6) = { VFM_VMFGE <-> 0b011111 } -mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if haveVExt() - <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt() +mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V) + <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { let rm_3b = fcsr[FRM]; diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 40a7ea9e7..16adf2806 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -11,6 +11,9 @@ /* Chapter 6: Configuration-Setting Instructions */ /* ******************************************************************************* */ +enum clause extension = Ext_V +function clause extensionEnabled(Ext_V) = (misa[V] == 0b1) & (mstatus[VS] != 0b00) + mapping sew_flag : string <-> bits(3) = { "e8" <-> 0b000, "e16" <-> 0b001, @@ -65,8 +68,8 @@ function calculate_new_vl(AVL, VLMAX) = { /* *********************************** vsetvli *********************************** */ union clause ast = VSETVLI : (bits(1), bits(1), bits(3), bits(3), regidx, regidx) -mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if haveVExt() - <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if extensionEnabled(Ext_V) + <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { let LMUL_pow_ori = get_lmul_pow(); @@ -116,8 +119,8 @@ mapping clause assembly = VSETVLI(ma, ta, sew, lmul, rs1, rd) /* *********************************** vsetvl ************************************ */ union clause ast = VSETVL : (regidx, regidx, regidx) -mapping clause encdec = VSETVL(rs2, rs1, rd) if haveVExt() - <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VSETVL(rs2, rs1, rd) if extensionEnabled(Ext_V) + <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute VSETVL(rs2, rs1, rd) = { let LMUL_pow_ori = get_lmul_pow(); @@ -167,8 +170,8 @@ mapping clause assembly = VSETVL(rs2, rs1, rd) /* ********************************** vsetivli *********************************** */ union clause ast = VSETIVLI : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx) -mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if haveVExt() - <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnabled(Ext_V) + <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if extensionEnabled(Ext_V) function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vtype */ diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail index 4f078d342..21dd026f1 100644 --- a/model/riscv_insts_zba.sail +++ b/model/riscv_insts_zba.sail @@ -6,11 +6,17 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extension = Ext_B +function clause extensionEnabled(Ext_B) = misa[B] == 0b1 + +enum clause extension = Ext_Zba +function clause extensionEnabled(Ext_Zba) = true | extensionEnabled(Ext_B) + /* ****************************************************************** */ union clause ast = RISCV_SLLIUW : (bits(6), regidx, regidx) -mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if haveZba() & sizeof(xlen) == 64 - <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 mapping clause assembly = RISCV_SLLIUW(shamt, rs1, rd) <-> "slli.uw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) @@ -25,17 +31,17 @@ function clause execute (RISCV_SLLIUW(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = ZBA_RTYPEUW : (regidx, regidx, regidx, bropw_zba) -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if haveZba() & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 mapping zba_rtypeuw_mnemonic : bropw_zba <-> string = { RISCV_ADDUW <-> "add.uw", @@ -64,12 +70,12 @@ function clause execute (ZBA_RTYPEUW(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBA_RTYPE : (regidx, regidx, regidx, brop_zba) -mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH1ADD) if haveZba() - <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZba() -mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if haveZba() - <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZba() -mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if haveZba() - <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZba() +mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH1ADD) if extensionEnabled(Ext_Zba) + <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extensionEnabled(Ext_Zba) +mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if extensionEnabled(Ext_Zba) + <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zba) +mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if extensionEnabled(Ext_Zba) + <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extensionEnabled(Ext_Zba) mapping zba_rtype_mnemonic : brop_zba <-> string = { RISCV_SH1ADD <-> "sh1add", diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index d39afc00b..696619dfe 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -6,11 +6,17 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extension = Ext_Zbb +function clause extensionEnabled(Ext_Zbb) = true | extensionEnabled(Ext_B) + +enum clause extension = 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 (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (extensionEnabled(Ext_Zbb) | 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 +31,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 (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero) + <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | 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 +49,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 (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | 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 (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = { RISCV_ROLW <-> "rolw", @@ -71,32 +77,32 @@ 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 extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) + <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | 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 extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) + <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | 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 extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) + <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if extensionEnabled(Ext_Zbb) + <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAXU) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAXU) if extensionEnabled(Ext_Zbb) + <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) -mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if haveZbb() - <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() +mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if extensionEnabled(Ext_Zbb) + <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) -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_MINU) if extensionEnabled(Ext_Zbb) + <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) -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 extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | 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 extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb) mapping zbb_rtype_mnemonic : brop_zbb <-> string = { RISCV_ANDN <-> "andn", @@ -138,17 +144,17 @@ function clause execute (ZBB_RTYPE(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBB_EXTOP : (regidx, regidx, extop_zbb) -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if haveZbb() - <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if extensionEnabled(Ext_Zbb) + <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if haveZbb() - <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if extensionEnabled(Ext_Zbb) + <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if haveZbb() & sizeof(xlen) == 32 - <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() & sizeof(xlen) == 32 +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 32 + <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 32 -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if haveZbb() & sizeof(xlen) == 64 - <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 + <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 mapping zbb_extop_mnemonic : extop_zbb <-> string = { RISCV_SEXTB <-> "sext.b", @@ -173,11 +179,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 (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32 + <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | 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 (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 + <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 mapping clause assembly = RISCV_REV8(rs1, rd) <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -194,8 +200,8 @@ function clause execute (RISCV_REV8(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_ORCB : (regidx, regidx) -mapping clause encdec = RISCV_ORCB(rs1, rd) if haveZbb() - <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_ORCB(rs1, rd) if extensionEnabled(Ext_Zbb) + <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) mapping clause assembly = RISCV_ORCB(rs1, rd) <-> "orc.b" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -214,8 +220,8 @@ function clause execute (RISCV_ORCB(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CPOP : (regidx, regidx) -mapping clause encdec = RISCV_CPOP(rs1, rd) if haveZbb() - <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_CPOP(rs1, rd) if extensionEnabled(Ext_Zbb) + <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) mapping clause assembly = RISCV_CPOP(rs1, rd) <-> "cpop" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -232,8 +238,8 @@ function clause execute (RISCV_CPOP(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CPOPW : (regidx, regidx) -mapping clause encdec = RISCV_CPOPW(rs1, rd) if haveZbb() & sizeof(xlen) == 64 - <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CPOPW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 + <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 mapping clause assembly = RISCV_CPOPW(rs1, rd) <-> "cpopw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -250,8 +256,8 @@ function clause execute (RISCV_CPOPW(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CLZ : (regidx, regidx) -mapping clause encdec = RISCV_CLZ(rs1, rd) if haveZbb() - <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_CLZ(rs1, rd) if extensionEnabled(Ext_Zbb) + <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) mapping clause assembly = RISCV_CLZ(rs1, rd) <-> "clz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -271,8 +277,8 @@ function clause execute (RISCV_CLZ(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CLZW : (regidx, regidx) -mapping clause encdec = RISCV_CLZW(rs1, rd) if haveZbb() & sizeof(xlen) == 64 - <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CLZW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 + <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 mapping clause assembly = RISCV_CLZW(rs1, rd) <-> "clzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -292,8 +298,8 @@ function clause execute (RISCV_CLZW(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CTZ : (regidx, regidx) -mapping clause encdec = RISCV_CTZ(rs1, rd) if haveZbb() - <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb() +mapping clause encdec = RISCV_CTZ(rs1, rd) if extensionEnabled(Ext_Zbb) + <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) mapping clause assembly = RISCV_CTZ(rs1, rd) <-> "ctz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -313,8 +319,8 @@ function clause execute (RISCV_CTZ(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_CTZW : (regidx, regidx) -mapping clause encdec = RISCV_CTZW(rs1, rd) if haveZbb() & sizeof(xlen) == 64 - <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CTZW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 + <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 mapping clause assembly = RISCV_CTZW(rs1, rd) <-> "ctzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail index 458b9faf0..54755f584 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 extension = Ext_Zbc +function clause extensionEnabled(Ext_Zbc) = true + +enum clause extension = 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..52c812035 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 extension = 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..348b702ec 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 extension = Ext_Zbs +function clause extensionEnabled(Ext_Zbs) = true | extensionEnabled(Ext_B) + /* ****************************************************************** */ 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_zcb.sail b/model/riscv_insts_zcb.sail index 86253bff4..e0e104081 100644 --- a/model/riscv_insts_zcb.sail +++ b/model/riscv_insts_zcb.sail @@ -6,11 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extension = Ext_Zcb +function clause extensionEnabled(Ext_Zcb) = sys_enable_zcb() + union clause ast = C_LBU : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_LBU(uimm1 @ uimm0, rdc, rs1c) if haveZcb() - <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb() + C_LBU(uimm1 @ uimm0, rdc, rs1c) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_LBU(uimm, rdc, rs1c) <-> "c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -27,8 +30,8 @@ function clause execute C_LBU(uimm, rdc, rs1c) = { union clause ast = C_LHU : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_LHU(uimm1 @ 0b0, rdc, rs1c) if haveZcb() - <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb() + C_LHU(uimm1 @ 0b0, rdc, rs1c) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_LHU(uimm, rdc, rs1c) <-> "c.lhu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -45,8 +48,8 @@ function clause execute C_LHU(uimm, rdc, rs1c) = { union clause ast = C_LH : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_LH(uimm1 @ 0b0, rdc, rs1c) if haveZcb() - <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb() + C_LH(uimm1 @ 0b0, rdc, rs1c) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_LH(uimm, rdc, rs1c) <-> "c.lh" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -63,8 +66,8 @@ function clause execute C_LH(uimm, rdc, rs1c) = { union clause ast = C_SB : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_SB(uimm1 @ uimm0, rs1c, rs2c) if haveZcb() - <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if haveZcb() + C_SB(uimm1 @ uimm0, rs1c, rs2c) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_SB(uimm, rs1c, rs2c) <-> "c.sb" ^ spc() ^ creg_name(rs2c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -81,8 +84,8 @@ function clause execute C_SB(uimm, rs1c, rs2c) = { union clause ast = C_SH : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_SH(uimm1 @ 0b0, rs1c, rs2c) if haveZcb() - <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if haveZcb() + C_SH(uimm1 @ 0b0, rs1c, rs2c) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_SH(uimm, rs1c, rs2c) <-> "c.sh" ^ spc() ^ creg_name(rs1c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs2c) ^ opt_spc() ^ ")" @@ -99,8 +102,8 @@ function clause execute C_SH(uimm, rs1c, rs2c) = { union clause ast = C_ZEXT_B : (cregidx) mapping clause encdec_compressed = - C_ZEXT_B(rsdc) if haveZcb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if haveZcb() + C_ZEXT_B(rsdc) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_ZEXT_B(rsdc) <-> "c.zext.b" ^ spc() ^ creg_name(rsdc) @@ -116,8 +119,8 @@ function clause execute C_ZEXT_B(rsdc) = { union clause ast = C_SEXT_B : (cregidx) mapping clause encdec_compressed = - C_SEXT_B(rsdc) if haveZcb() & haveZbb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if haveZcb() & haveZbb() + C_SEXT_B(rsdc) if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb) mapping clause assembly = C_SEXT_B(rsdc) <-> "c.sext.b" ^ spc() ^ creg_name(rsdc) @@ -132,8 +135,8 @@ function clause execute C_SEXT_B(rsdc) = { union clause ast = C_ZEXT_H : (cregidx) mapping clause encdec_compressed = - C_ZEXT_H(rsdc) if haveZcb() & haveZbb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if haveZcb() & haveZbb() + C_ZEXT_H(rsdc) if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb) mapping clause assembly = C_ZEXT_H(rsdc) <-> "c.zext.h" ^ spc() ^ creg_name(rsdc) @@ -148,8 +151,8 @@ function clause execute C_ZEXT_H(rsdc) = { union clause ast = C_SEXT_H : (cregidx) mapping clause encdec_compressed = - C_SEXT_H(rsdc) if haveZcb() & haveZbb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if haveZcb() & haveZbb() + C_SEXT_H(rsdc) if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb) mapping clause assembly = C_SEXT_H(rsdc) <-> "c.sext.h" ^ spc() ^ creg_name(rsdc) @@ -164,8 +167,8 @@ function clause execute C_SEXT_H(rsdc) = { union clause ast = C_ZEXT_W : (cregidx) mapping clause encdec_compressed = - C_ZEXT_W(rsdc) if haveZcb() & haveZba() & sizeof(xlen) == 64 - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if haveZcb() & haveZba() & sizeof(xlen) == 64 + C_ZEXT_W(rsdc) if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 mapping clause assembly = C_ZEXT_W(rsdc) <-> "c.zext.w" ^ spc() ^ creg_name(rsdc) @@ -180,8 +183,8 @@ function clause execute C_ZEXT_W(rsdc) = { union clause ast = C_NOT : (cregidx) mapping clause encdec_compressed = - C_NOT(rsdc) if haveZcb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if haveZcb() + C_NOT(rsdc) if extensionEnabled(Ext_Zcb) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if extensionEnabled(Ext_Zcb) mapping clause assembly = C_NOT(rsdc) <-> "c.not" ^ spc() ^ creg_name(rsdc) @@ -197,8 +200,8 @@ function clause execute C_NOT(rsdc) = { union clause ast = C_MUL : (cregidx, cregidx) mapping clause encdec_compressed = - C_MUL(rsdc, rs2c) if haveZcb() & (haveMulDiv() | haveZmmul()) - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (haveMulDiv() | haveZmmul()) + C_MUL(rsdc, rs2c) if extensionEnabled(Ext_Zcb) & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if extensionEnabled(Ext_Zcb) & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) mapping clause assembly = C_MUL(rsdc, rs2c) <-> "c.mul" ^ spc() ^ creg_name(rsdc) ^ sep() ^ creg_name(rs2c) diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 1443daf3d..2b1f7c50f 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 extension = 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..5e55fb8a2 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -6,6 +6,9 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +enum clause extension = Ext_Zhinx +function clause extensionEnabled(Ext_Zhinx) = sys_enable_zfinx() + /* **************************************************************** */ /* This file specifies the instructions in the Zfh extension */ /* (half precision floating point). */ @@ -162,7 +165,7 @@ function fle_H (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveHalfFPU() -> bool = haveZfh() | haveZhinx() +function haveHalfFPU() -> bool = extensionEnabled(Ext_Zfh) | extensionEnabled(Ext_Zhinx) /* ****************************************************************** */ /* Floating-point loads */ @@ -881,11 +884,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..9491fe950 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 extension = 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..4bb94eefa 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 extension = 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 extension = 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 extension = 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..ba4a86853 100644 --- a/model/riscv_insts_zks.sail +++ b/model/riscv_insts_zks.sail @@ -11,14 +11,17 @@ * ---------------------------------------------------------------------- */ +enum clause extension = 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 extension = 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_jalr_seq.sail b/model/riscv_jalr_seq.sail index 497a44178..0f4abd0e9 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -24,7 +24,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { }, Ext_ControlAddr_OK(addr) => { let target = [addr with 0 = bitzero]; /* clear addr[0] */ - if bit_to_bool(target[1]) & not(haveRVC()) then { + if bit_to_bool(target[1]) & not(extensionEnabled(Ext_C)) then { handle_mem_exception(target, E_Fetch_Addr_Align()); RETIRE_FAIL } else { diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 6ae84ea63..2f83a0abc 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -8,14 +8,14 @@ /* Functional specification for the 'N' user-level interrupts standard extension. */ -function clause ext_is_CSR_defined(0x000) = haveUsrMode() & haveNExt() // ustatus -function clause ext_is_CSR_defined(0x004) = haveUsrMode() & haveNExt() // uie -function clause ext_is_CSR_defined(0x005) = haveUsrMode() & haveNExt() // utvec -function clause ext_is_CSR_defined(0x040) = haveUsrMode() & haveNExt() // uscratch -function clause ext_is_CSR_defined(0x041) = haveUsrMode() & haveNExt() // uepc -function clause ext_is_CSR_defined(0x042) = haveUsrMode() & haveNExt() // ucause -function clause ext_is_CSR_defined(0x043) = haveUsrMode() & haveNExt() // utval -function clause ext_is_CSR_defined(0x044) = haveUsrMode() & haveNExt() // uip +function clause ext_is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus +function clause ext_is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie +function clause ext_is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec +function clause ext_is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch +function clause ext_is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc +function clause ext_is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause +function clause ext_is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval +function clause ext_is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits) function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 5ff7e4bc0..6f2a15862 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -54,7 +54,7 @@ function step(step_no : int) -> bool = { print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); }; /* check for RVC once here instead of every RVC execute clause. */ - if haveRVC() then { + if extensionEnabled(Ext_C) then { nextPC = PC + 2; (execute(ast), true) } else { diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index becf447a9..1df71d3af 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 extension = Ext_Zkr +function clause extensionEnabled(Ext_Zkr) = true /* CSR access control */ @@ -25,14 +27,14 @@ function is_CSR_defined (csr : csreg) -> bool = /* machine mode: trap setup */ 0x300 => true, // mstatus 0x301 => true, // misa - 0x302 => haveSupMode() | haveNExt(), // medeleg - 0x303 => haveSupMode() | haveNExt(), // mideleg + 0x302 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // medeleg + 0x303 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // mideleg 0x304 => true, // mie 0x305 => true, // mtvec - 0x306 => haveUsrMode(), // mcounteren - 0x30A => haveUsrMode(), // menvcfg + 0x306 => extensionEnabled(Ext_U), // mcounteren + 0x30A => extensionEnabled(Ext_U), // menvcfg 0x310 => sizeof(xlen) == 32, // mstatush - 0x31A => haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh + 0x31A => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // menvcfgh 0x320 => true, // mcountinhibit /* machine mode: trap handling */ 0x340 => true, // mscratch @@ -59,35 +61,35 @@ function is_CSR_defined (csr : csreg) -> bool = 0x7a0 => true, /* supervisor mode: trap setup */ - 0x100 => haveSupMode(), // sstatus - 0x102 => haveSupMode() & haveNExt(), // sedeleg - 0x103 => haveSupMode() & haveNExt(), // sideleg - 0x104 => haveSupMode(), // sie - 0x105 => haveSupMode(), // stvec - 0x106 => haveSupMode(), // scounteren - 0x10A => haveSupMode(), // senvcfg + 0x100 => extensionEnabled(Ext_S), // sstatus + 0x102 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sedeleg + 0x103 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sideleg + 0x104 => extensionEnabled(Ext_S), // sie + 0x105 => extensionEnabled(Ext_S), // stvec + 0x106 => extensionEnabled(Ext_S), // scounteren + 0x10A => extensionEnabled(Ext_S), // senvcfg /* supervisor mode: trap handling */ - 0x140 => haveSupMode(), // sscratch - 0x141 => haveSupMode(), // sepc - 0x142 => haveSupMode(), // scause - 0x143 => haveSupMode(), // stval - 0x144 => haveSupMode(), // sip + 0x140 => extensionEnabled(Ext_S), // sscratch + 0x141 => extensionEnabled(Ext_S), // sepc + 0x142 => extensionEnabled(Ext_S), // scause + 0x143 => extensionEnabled(Ext_S), // stval + 0x144 => extensionEnabled(Ext_S), // sip /* supervisor mode: address translation */ - 0x180 => haveSupMode(), // satp + 0x180 => extensionEnabled(Ext_S), // satp /* user mode: counters */ - 0xC00 => haveUsrMode(), // cycle - 0xC01 => haveUsrMode(), // time - 0xC02 => haveUsrMode(), // instret + 0xC00 => extensionEnabled(Ext_U), // cycle + 0xC01 => extensionEnabled(Ext_U), // time + 0xC02 => extensionEnabled(Ext_U), // instret - 0xC80 => haveUsrMode() & (sizeof(xlen) == 32), // cycleh - 0xC81 => haveUsrMode() & (sizeof(xlen) == 32), // timeh - 0xC82 => haveUsrMode() & (sizeof(xlen) == 32), // instreth + 0xC80 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // cycleh + 0xC81 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // timeh + 0xC82 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // instreth /* user mode: Zkr */ - 0x015 => haveZkr(), + 0x015 => extensionEnabled(Ext_Zkr), /* check extensions */ _ => ext_is_CSR_defined(csr) @@ -107,9 +109,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = (0xC01, Supervisor) => mcounteren[TM] == 0b1, (0xC02, Supervisor) => mcounteren[IR] == 0b1, - (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1), - (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1), - (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | scounteren[IR] == 0b1), + (0xC00, User) => mcounteren[CY] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[CY] == 0b1), + (0xC01, User) => mcounteren[TM] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[TM] == 0b1), + (0xC02, User) => mcounteren[IR] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[IR] == 0b1), (_, _) => /* no HPM counters for now */ if 0xC03 <=_u csr & csr <=_u 0xC1F @@ -168,11 +170,11 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { let idx = num_of_ExceptionType(e); let super = bit_to_bool(medeleg.bits[idx]); /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */ - let user = if haveSupMode() - then super & haveNExt() & bit_to_bool(sedeleg.bits[idx]) - else super & haveNExt(); - let deleg = if haveUsrMode() & user then User - else if haveSupMode() & super then Supervisor + let user = if extensionEnabled(Ext_S) + then super & extensionEnabled(Ext_N) & bit_to_bool(sedeleg.bits[idx]) + else super & extensionEnabled(Ext_N); + let deleg = if extensionEnabled(Ext_U) & user then User + else if extensionEnabled(Ext_S) & super then Supervisor else Machine; /* We cannot transition to a less-privileged mode. */ if privLevel_to_bits(deleg) <_u privLevel_to_bits(p) @@ -228,7 +230,7 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits * allows for example the M_Timer to be delegated to the U-mode. */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { - assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); + assert(extensionEnabled(Ext_U), "no user mode: M/U or M/S/U system required"); let effective_pending = mip.bits & mie.bits; if effective_pending == zero_extend(0b0) then None() /* fast path */ else { @@ -237,13 +239,13 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { * considered blocked. */ let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1); - let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1)); - let uIE = haveNExt() & (priv == User & mstatus[UIE] == 0b1); + let sIE = extensionEnabled(Ext_S) & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1)); + let uIE = extensionEnabled(Ext_N) & (priv == User & mstatus[UIE] == 0b1); match processPending(mip, mie, mideleg.bits, mIE) { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Machine) in Some(r), Ints_Delegated(d) => - if not(haveSupMode()) then { + if not(extensionEnabled(Ext_S)) then { if uIE then let r = (d, User) in Some(r) else None() } else { @@ -267,7 +269,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege /* If we don't have different privilege levels, we don't need to check delegation. * Absence of U-mode implies absence of S-mode. */ - if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then { + if not(extensionEnabled(Ext_U)) | (not(extensionEnabled(Ext_S)) & not(extensionEnabled(Ext_N))) then { assert(priv == Machine, "invalid current privilege"); let enabled_pending = mip.bits & mie.bits; match findPendingInterrupt(enabled_pending) { @@ -346,7 +348,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, mcause) }, Supervisor => { - assert (haveSupMode(), "no supervisor mode present for delegation"); + assert (extensionEnabled(Ext_S), "no supervisor mode present for delegation"); scause[IsInterrupt] = bool_to_bits(intr); scause[Cause] = zero_extend(c); @@ -371,7 +373,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, scause) }, User => { - assert(haveUsrMode(), "no user mode present for delegation"); + assert(extensionEnabled(Ext_U), "no user mode present for delegation"); ucause[IsInterrupt] = bool_to_bits(intr); ucause[Cause] = zero_extend(c); @@ -408,7 +410,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus[MIE] = mstatus[MPIE]; mstatus[MPIE] = 0b1; cur_privilege = privLevel_of_bits(mstatus[MPP]); - mstatus[MPP] = privLevel_to_bits(if haveUsrMode() then User else Machine); + mstatus[MPP] = privLevel_to_bits(if extensionEnabled(Ext_U) then User else Machine); if cur_privilege != Machine then mstatus[MPRV] = 0b0; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6eb174189..fc19d5161 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -128,64 +128,26 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { } } -/* helpers to check support for various extensions. */ -/* we currently don't model 'E', so always assume 'I'. */ -function haveAtomics() -> bool = misa[A] == 0b1 -function haveRVC() -> bool = misa[C] == 0b1 -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 (and Z*inx counterparts) extension tests */ - -/* BitManip extension support. */ -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 - -/* A extension sub-extensions */ -function haveZaamo() -> bool = haveAtomics() -function haveZalrsc() -> bool = haveAtomics() - -/* Zicond extension support */ -function haveZicond() -> bool = true - -/* Zabha extension support */ -function haveZabha() -> bool = true +enum clause extension = Ext_N +function clause extensionEnabled(Ext_N) = misa[N] == 0b1 + +enum clause extension = Ext_U +function clause extensionEnabled(Ext_U) = misa[U] == 0b1 + +enum clause extension = Ext_S +function clause extensionEnabled(Ext_S) = misa[S] == 0b1 /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. */ function lowest_supported_privLevel() -> Privilege = - if haveUsrMode() then User else Machine + if extensionEnabled(Ext_U) then User else Machine function have_privLevel(priv : priv_level) -> bool = match priv { - 0b00 => haveUsrMode(), - 0b01 => haveSupMode(), + 0b00 => extensionEnabled(Ext_U), + 0b01 => extensionEnabled(Ext_S), 0b10 => false, 0b11 => true, } @@ -304,13 +266,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { } else m; /* Hardwired to zero in the absence of 'U' or 'N'. */ - let m = if not(haveNExt()) then { + let m = if not(extensionEnabled(Ext_N)) then { let m = [m with UPIE = 0b0]; let m = [m with UIE = 0b0]; m } else m; - if not(haveUsrMode()) then { + if not(extensionEnabled(Ext_U)) then { let m = [m with MPRV = 0b0]; m } else m @@ -335,24 +297,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) - -function haveSvinval() -> bool = sys_enable_svinval() - -/* Zcb has simple code-size saving instructions. (The Zcb extension depends on the Zca extension.) */ -function haveZcb() -> bool = sys_enable_zcb() - -/* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */ -function haveZhinx() -> bool = sys_enable_zfinx() -function haveZfinx() -> bool = sys_enable_zfinx() -function haveZdinx() -> bool = sys_enable_zfinx() & sizeof(flen) >= 64 - /* interrupt processing state */ bitfield Minterrupts : xlenbits = { @@ -377,7 +321,7 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]; - if haveUsrMode() & haveNExt() then { + if extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then { [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } @@ -393,7 +337,7 @@ function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { SSI = v[SSI] ]; /* The U-mode bits will be modified if we have the 'N' extension. */ - if haveUsrMode() & haveNExt() then { + if extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then { [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } @@ -681,7 +625,7 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; - if haveNExt() then { + if extensionEnabled(Ext_N) then { let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; m @@ -698,7 +642,7 @@ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m; let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m; let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; - if haveNExt() then { + if extensionEnabled(Ext_N) then { let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m; let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; diff --git a/model/riscv_types.sail b/model/riscv_types.sail index f6e2d1ced..166aee072 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -8,6 +8,17 @@ /* Basic type and function definitions used pervasively in the model. */ +/* ISA extension names as enums */ +scattered enum extension + +// Function used to determine if an extension is enabled in the current configuration. +// This means an extension is implemented & supported, *and* any necessary bits +// are set in the relevant CSRs (misa, mstatus, etc.) to enable its use. It is possible +// for some extensions to be supported in hardware, but temporarily disabled via a CSR, +// in which case this function should return false. +val extensionEnabled : extension -> bool +scattered function extensionEnabled + /* this value is only defined for the runtime platform for ELF loading * checks, and not used in the model. */