Add Zabha extension

model/riscv_insts_aext.sail

@@ -21,31 +21,39 @@ function aqrl_str(aq : bool, rl : bool) -> string =
   }
 
 function lrsc_width_str(width : word_width) -> string =
-  match (width) {
+  match width {
     BYTE   => ".b",
     HALF   => ".h",
     WORD   => ".w",
     DOUBLE => ".d"
   }
 
 /**
- * RISC-V only appears to define LR / SC / AMOs for word and double, although
- * there seem to be encodings reserved for other widths.
+ * RISC-V A-extension defines LR / SC / AMOs for word and double
+ * RISC-V Zabha extension defines AMOs for byte and halfword
  */
-function amo_width_valid(size : word_width) -> bool = {
-  match(size) {
+function lrsc_width_valid(size : word_width) -> bool = {
+  match size {
     WORD   => true,
     DOUBLE => sizeof(xlen) >= 64,
     _      => false
   }
 }
 
+function amo_width_valid(size : word_width) -> bool = {
+  match size {
+    BYTE   => haveZabha(),
+    HALF   => haveZabha(),
+    WORD   => true,
+    DOUBLE => sizeof(xlen) >= 64,
+  }
+}
+
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 
-mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if haveZalrsc() & amo_width_valid(size)
-  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
-
+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)
 
 /* We could set load-reservations on physical or virtual addresses.
  * For now we set them on virtual addresses, since it makes the
@@ -88,8 +96,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() & amo_width_valid(size)
-  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
+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)
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
@@ -125,7 +133,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
               TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
               TR_Address(addr, _) => {
                 let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
-                match (eares) {
+                match eares {
                   MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
                   MemValue(_) => {
                     let rs2_val = X(rs2);
@@ -187,7 +195,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
         TR_Address(addr, _) => {
           let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
           let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
-          match (eares) {
+          match eares {
             MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
             MemValue(_) => {
               match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {

model/riscv_sys_regs.sail

@@ -168,6 +168,9 @@ function haveZalrsc() -> bool = haveAtomics()
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* 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.