Merge pull request #506 from ThinkOpenly/upstream-extension-tags

Add a consistent mechanism for identifying instruction's containing extension

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]))

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),

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),

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.
  * However most chips (especially multi-core) will use physical addresses.
@@ -100,8 +106,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)) = {
@@ -162,6 +168,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) = {
@@ -176,8 +185,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. */

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 }

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);