Use extension discriminator for "A" and "M" extensions

Using the `extensionEnabled()` function in `mapping clause encdec`
expressions for extensions allows a parser to clearly know when a
function is part of an extension (or set of extensions).

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. */

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

model/riscv_insts_zcb.sail

@@ -197,8 +197,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 haveZcb() & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
+ <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
 
 mapping clause assembly = C_MUL(rsdc, rs2c) <->
  "c.mul" ^ spc() ^ creg_name(rsdc) ^ sep() ^ creg_name(rs2c)

model/riscv_sys_regs.sail

@@ -130,8 +130,6 @@ 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 haveMulDiv() -> bool = misa[M] == 0b1
 function haveSupMode() -> bool = misa[S] == 0b1
 function haveUsrMode() -> bool = misa[U] == 0b1
 function haveNExt() -> bool = misa[N] == 0b1
@@ -142,15 +140,6 @@ function haveBExt() -> bool = misa[B] == 0b1
 function haveZba() -> bool = true | haveBExt()
 function haveZbb() -> bool = true | haveBExt()
 
-function haveZmmul() -> bool = true
-
-/* A extension sub-extensions */
-function haveZaamo() -> bool = haveAtomics()
-function haveZalrsc() -> bool = haveAtomics()
-
-/* Zabha extension support */
-function haveZabha() -> bool = true
-
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.