Add support for the Zalasr extension

Makefile.old

@@ -53,6 +53,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbkb.sail
 SAIL_DEFAULT_INST += riscv_insts_zbkx.sail
 
 SAIL_DEFAULT_INST += riscv_insts_zicond.sail
+SAIL_DEFAULT_INST += riscv_insts_zalasr.sail
 
 SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail
 SAIL_DEFAULT_INST += riscv_insts_vext_fp_utils.sail

README.md

@@ -105,6 +105,7 @@ Supported RISC-V ISA features
 - Zalrsc extension for load-reserved and store-conditional operations, v1.0
 - Zaamo extension for atomic memory operations, v1.0
 - Zabha extension for byte and halfword atomic memory operations, v1.0
+- Zalasr extension for load-acquire and store-release, v0.3.5
 - F and D extensions for single and double-precision floating-point, v2.2
 - Zfh and Zfhmin extensions for half-precision floating-point, v1.0
 - Zfa extension for additional floating-point instructions, v1.0

model/CMakeLists.txt

@@ -78,6 +78,7 @@ foreach (xlen IN ITEMS 32 64)
                 ${vext_srcs}
                 "riscv_insts_zicbom.sail"
                 "riscv_insts_zicboz.sail"
+                "riscv_insts_zalasr.sail"
             )
 
             if (variant STREQUAL "rmem")

model/riscv_extensions.sail

@@ -50,6 +50,8 @@ enum clause extension = Ext_Zaamo
 enum clause extension = Ext_Zabha
 // Load-Reserved/Store-Conditional Instructions
 enum clause extension = Ext_Zalrsc
+// Load-Acquire/Store-Release Instructions
+enum clause extension = Ext_Zalasr
 
 // Additional Floating-Point Instructions
 enum clause extension = Ext_Zfa

model/riscv_insts_zalasr.sail

@@ -0,0 +1,53 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* *********************************************************************** */
+/* This file specifies the atomic instructions in the 'Zalasr' extension.  */
+
+/* *********************************************************************** */
+
+function clause extensionEnabled(Ext_Zalasr) = true
+
+union clause ast = LOADAQ : (bool, bool, regidx, word_width, regidx)
+
+mapping clause encdec = LOADAQ(aq, rl, rs1, size, rd)                                                 if extensionEnabled(Ext_Zalasr)
+  <-> 0b00110 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalasr)
+
+function clause execute(LOADAQ(aq, rl, rs1, width, rd)) = {
+  // load-acquire is required to have the acquire bit set
+  if not(aq)
+  then { handle_illegal(); RETIRE_FAIL }
+  else {
+    execute(LOAD(zeros(), rs1, rd, false, width, aq, rl))
+  }
+}
+
+mapping clause assembly = LOADAQ(aq, rl, rs1, size, rd)
+                      <-> "l" ^ size_mnemonic(size)
+                          ^ maybe_aq(aq) ^ maybe_rl(rl)
+                          ^ spc() ^ reg_name(rd)
+                          ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
+
+union clause ast = STORERL : (bool, bool, regidx, regidx, word_width)
+mapping clause encdec = STORERL(aq, rl, rs2, rs1, size)                                                if extensionEnabled(Ext_Zalasr)
+  <-> 0b00111 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ 0b00000 @ 0b0101111 if extensionEnabled(Ext_Zalasr)
+
+function clause execute (STORERL(aq, rl, rs2, rs1, width)) = {
+  // store-release is required to have the release bit set
+  if not(rl)
+  then { handle_illegal(); RETIRE_FAIL }
+  else {
+    execute(STORE(zeros(), rs2, rs1, width, aq, rl))
+  }
+}
+
+mapping clause assembly = STORERL(aq, rl, rs2, rs1, size)
+                      <-> "s" ^ size_mnemonic(size)
+                          ^ maybe_aq(aq) ^ maybe_rl(rl)
+                          ^ spc() ^ reg_name(rs2)
+                          ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"