From 809337eb0db5de41928c7d9ad90c20f786107a41 Mon Sep 17 00:00:00 2001
From: Ved Shanbhogue <91900059+ved-rivos@users.noreply.github.com>
Date: Tue, 9 Jul 2024 11:50:32 -0500
Subject: [PATCH] Add Zabha extension

Specification: https://github.com/riscv/riscv-zabha

This adds optional support for byte and half LR/SC (though currently it is always enabled).

Tested with RISC-V arch. tests and checked against spike.
---
 model/riscv_insts_aext.sail | 32 ++++++++++++++++++++------------
 model/riscv_sys_regs.sail   |  3 +++
 2 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 3bf44b8f5..8141acec2 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -21,7 +21,7 @@ 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",
@@ -29,23 +29,31 @@ function lrsc_width_str(width : word_width) -> string =
   }
 
 /**
- * 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) {
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 66b601049..6eb174189 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -172,6 +172,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.