Add Zilsd/Zclsd Support

README.md

@@ -141,6 +141,7 @@ For booting operating system images, see the information under the
 - Ziccrse extension for Main memory regions with both the cacheability and coherence PMAs must support RsrvEventual, v1.0
 - Zicfilp extension for Landing Pad Control Flow Integrity, v1.0
 - Zicfiss extension for Shadow Stack Control Flow Integrity, v1.0
+- Zilsd and Zclsd extensions for RV32 Load/Store pair instructions, v1.0
 - Zimop extension for May-Be-Operations, v1.0
 - Zihintntl extension for Non-temporal Locality Hints, v1.0
 - Zihintpause extension for Pause Hint, v2.0

config/config.json.in

@@ -82,7 +82,11 @@
       // The configuration option determines how to handle the reserved behavior: Odd-numbered registers for RV32Zdinx.
       // "Zdinx_Fatal"  – raise a Sail exception, stopping execution.
       // "Zdinx_Illegal" – treat it as an illegal instruction.
-      "rv32zdinx_odd_register": "Zdinx_Illegal"
+      "rv32zdinx_odd_register": "Zdinx_Illegal",
+      // The configuration option determines how to handle the reserved behavior: Odd-numbered registers for Zilsd and Zclsd.
+      // "LoadStorePair_Fatal"  – raise a Sail exception, stopping execution.
+      // "LoadStorePair_Illegal" – treat it as an illegal instruction.
+      "rv32load_store_pair_odd_register": "LoadStorePair_Illegal"
     }
   },
   "memory": {
@@ -338,6 +342,9 @@
     "Zihpm": {
       "supported": true
     },
+    "Zilsd": {
+      "supported": @CONFIG_XLEN_IS_32@
+    },
     "Zimop": {
       "supported": true
     },
@@ -395,6 +402,9 @@
     "Zcb": {
       "supported": true
     },
+    "Zclsd": {
+      "supported": false
+    },
     "Zcmop": {
       "supported": true
     },

model/core/extensions.sail

@@ -126,6 +126,10 @@ function clause hartSupports(Ext_Zihintpause) = config extensions.Zihintpause.su
 enum clause extension = Ext_Zihpm
 mapping clause extensionName = Ext_Zihpm <-> "zihpm"
 function clause hartSupports(Ext_Zihpm) = config extensions.Zihpm.supported
+// Load/Store Pair for RV32
+enum clause extension = Ext_Zilsd
+mapping clause extensionName = Ext_Zilsd <-> "zilsd"
+function clause hartSupports(Ext_Zilsd) = config extensions.Zilsd.supported : bool & (xlen == 32)
 // May-Be-Operations
 enum clause extension = Ext_Zimop
 mapping clause extensionName = Ext_Zimop <-> "zimop"
@@ -248,6 +252,11 @@ enum clause extension = Ext_Zbs
 mapping clause extensionName = Ext_Zbs <-> "zbs"
 function clause hartSupports(Ext_Zbs) = config extensions.Zbs.supported
 
+// Compressed Load/Store pair instructions
+enum clause extension = Ext_Zclsd
+mapping clause extensionName = Ext_Zclsd <-> "zclsd"
+function clause hartSupports(Ext_Zclsd) = config extensions.Zclsd.supported : bool & (xlen == 32)
+
 // Main memory supports all atomics in Zaamo
 enum clause extension = Ext_Ziccamoa
 mapping clause extensionName= Ext_Ziccamoa <-> "Ziccamoa"
@@ -646,6 +655,7 @@ let extensions_ordered_for_isa_string = [
   Ext_Zicntr,
   Ext_Zicond,
   Ext_Zicsr,
+  Ext_Zilsd,
   Ext_Zifencei,
   Ext_Zihintntl,
   Ext_Zihintpause,
@@ -679,6 +689,7 @@ let extensions_ordered_for_isa_string = [
   Ext_Zcb,
   Ext_Zcd,
   Ext_Zcf,
+  Ext_Zclsd,
   Ext_Zcmop,
 
   // Zb

model/core/platform_config.sail

@@ -95,9 +95,15 @@ enum RV32ZdinxOddRegisterReservedBehavior = {
   Zdinx_Illegal,
 }
 
+enum RV32LoadStorePairOddRegisterReservedBehavior = {
+  LoadStorePair_Fatal,
+  LoadStorePair_Illegal,
+}
+
 let amocas_odd_register_reserved_behavior : AmocasOddRegisterReservedBehavior = config base.reserved_behavior.amocas_odd_register
 let fcsr_rm_reserved_behavior : FcsrRmReservedBehavior = config base.reserved_behavior.fcsr_rm
 let pmp_write_only_reserved_behavior : PmpWriteOnlyReservedBehavior = config base.reserved_behavior.pmpcfg_write_only
 let xenvcfg_cbie_reserved_behavior : XenvcfgCbieReservedBehavior = config base.reserved_behavior.xenvcfg_cbie
 let xtvec_mode_reserved_behavior : XtvecModeReservedBehavior = config base.reserved_behavior.xtvec_mode
 let rv32zdinx_odd_register_reserved_behavior : RV32ZdinxOddRegisterReservedBehavior = config base.reserved_behavior.rv32zdinx_odd_register
+let rv32load_store_pair_odd_register_reserved_behavior : RV32LoadStorePairOddRegisterReservedBehavior = config base.reserved_behavior.rv32load_store_pair_odd_register

model/extensions/FD/zcf_insts.sail

@@ -6,7 +6,7 @@
 // SPDX-License-Identifier: BSD-2-Clause
 // =======================================================================================
 
-function clause currentlyEnabled(Ext_Zcf) = hartSupports(Ext_Zcf) & currentlyEnabled(Ext_F) & currentlyEnabled(Ext_Zca) & (currentlyEnabled(Ext_C) | not(hartSupports(Ext_C)))
+function clause currentlyEnabled(Ext_Zcf) = hartSupports(Ext_Zcf) & currentlyEnabled(Ext_F) & currentlyEnabled(Ext_Zca) & (currentlyEnabled(Ext_C) | not(hartSupports(Ext_C))) & not(hartSupports(Ext_Zclsd))
 
 union clause instruction = C_FLWSP : (bits(6), fregidx)
 

model/extensions/Zclsd/zclsd_insts.sail

@@ -0,0 +1,87 @@
+/*=======================================================================================*/
+/*  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                                                */
+/*=======================================================================================*/
+
+function clause currentlyEnabled(Ext_Zclsd) = hartSupports(Ext_Zilsd) & currentlyEnabled(Ext_Zca) & not(hartSupports(Ext_Zcf)) & xlen == 32
+
+// RV32Zclsd requires even register pairs
+function validZclsdReg(reg : regidx) -> bool = {
+  if encdec_reg(reg)[0] == 0b1
+  then match rv32load_store_pair_odd_register_reserved_behavior {
+    LoadStorePair_Fatal   => reserved_behavior("Zclsd used odd-numbered register " ^ dec_str(unsigned(encdec_reg(reg)))),
+    LoadStorePair_Illegal => return false,
+  };
+  true
+}
+
+function validZclsdCReg(reg : cregidx) -> bool =
+  validZclsdReg(creg2reg_idx(reg))
+
+/* ****************************************************************** */
+union clause instruction = ZCLSD_C_LDSP : (bits(9), regidx)
+
+$[wavedrom "C.LDSP offset[5] dest offset[4:3] offset[8:6] C2"]
+mapping clause encdec_compressed = ZCLSD_C_LDSP(uimm @ 0b000, rd)
+  <-> 0b011 @ uimm[2] @ encdec_reg(rd) @ uimm[1..0] @ uimm[5..3] @ 0b10
+  when currentlyEnabled(Ext_Zclsd) & validZclsdReg(rd) & rd != zreg
+
+function clause execute ZCLSD_C_LDSP(imm, rd) = {
+  ExecuteAs(ZILSD_LD(zero_extend(imm), sp, rd))
+}
+
+mapping clause assembly = ZCLSD_C_LDSP(uimm, rd)
+  <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_9(uimm)
+  when rd != zreg
+
+/* ****************************************************************** */
+union clause instruction = ZCLSD_C_SDSP : (bits(9), regidx)
+
+$[wavedrom "C.SDSP offset[5:3] offset[8:6] src C2"]
+mapping clause encdec_compressed = ZCLSD_C_SDSP(uimm @ 0b000, rs2)
+  <-> 0b111 @ uimm[2 .. 0] @ uimm[5 .. 3] @ encdec_reg(rs2) @ 0b10
+  when currentlyEnabled(Ext_Zclsd) & validZclsdReg(rs2)
+
+function clause execute ZCLSD_C_SDSP(uimm, rs2) = {
+  ExecuteAs(ZILSD_SD(zero_extend(uimm), rs2, sp))
+}
+
+mapping clause assembly = ZCLSD_C_SDSP(uimm, rs2)
+  <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_9(uimm)
+
+/* ****************************************************************** */
+union clause instruction = ZCLSD_C_LD : (bits(8), cregidx, cregidx)
+
+$[wavedrom "C.LD offset[5:3] base offset[7:6] dest C0"]
+mapping clause encdec_compressed = ZCLSD_C_LD(uimm @ 0b000, rs1, rd)
+  <-> 0b011 @ uimm[2 .. 0] @ encdec_creg(rs1) @ uimm[4 .. 3] @ encdec_creg(rd) @ 0b00
+  when currentlyEnabled(Ext_Zclsd) & validZclsdCReg(rd)
+
+function clause execute ZCLSD_C_LD(uimm, rsc, rdc) = {
+  let rd = creg2reg_idx(rdc);
+  let rs = creg2reg_idx(rsc);
+  ExecuteAs(ZILSD_LD(zero_extend(uimm), rs, rd))
+}
+
+mapping clause assembly = ZCLSD_C_LD(uimm, rsc, rdc)
+  <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm)
+
+/* ****************************************************************** */
+union clause instruction = ZCLSD_C_SD : (bits(8), cregidx, cregidx)
+
+$[wavedrom "C.SD offset[5:3] base offset[7:6] src C0"]
+mapping clause encdec_compressed = ZCLSD_C_SD(uimm @ 0b000, rs1, rs2)
+  <-> 0b111 @ uimm[2 .. 0] @ encdec_creg(rs1) @ uimm[4 .. 3] @ encdec_creg(rs2) @ 0b00
+  when currentlyEnabled(Ext_Zclsd) & validZclsdCReg(rs2)
+
+function clause execute ZCLSD_C_SD(uimm, rsc1, rsc2) = {
+  let rs1 = creg2reg_idx(rsc1);
+  let rs2 = creg2reg_idx(rsc2);
+  ExecuteAs(ZILSD_SD(zero_extend(uimm), rs2, rs1))
+}
+
+mapping clause assembly = ZCLSD_C_SD(uimm, rsc1, rsc2)
+  <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm)

model/extensions/Zilsd/zilsd_insts.sail

@@ -0,0 +1,73 @@
+/*=======================================================================================*/
+/*  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                                                */
+/*=======================================================================================*/
+
+function clause currentlyEnabled(Ext_Zilsd) = hartSupports(Ext_Zilsd) & xlen == 32
+
+// Zilsd requires even register pairs
+function validZilsdReg(reg : regidx) -> bool = {
+  if   encdec_reg(reg)[0] == 0b1
+  then match rv32load_store_pair_odd_register_reserved_behavior {
+    LoadStorePair_Fatal   => reserved_behavior("Zilsd used odd-numbered register " ^ dec_str(unsigned(encdec_reg(reg)))),
+    LoadStorePair_Illegal => return false,
+  };
+  true
+}
+
+// TODO: According to the spec, an implementation can generate a
+// misaligned trap when performing these instructions at 4B-aligned
+// but not 8B-aligned addresses.  The implementation below does not
+// model this, since it always performs word accesses.
+
+/* ****************************************************************** */
+union clause instruction = ZILSD_LD : (bits(12), regidx, regidx)
+
+$[wavedrom "offset[11:5] base width=D dest LOAD"]
+mapping clause encdec = ZILSD_LD(imm, rs1, rd)
+  <-> imm @ encdec_reg(rs1) @ 0b011 @ encdec_reg(rd) @ 0b0000011
+  when currentlyEnabled(Ext_Zilsd) & validZilsdReg(rd)
+
+function clause execute ZILSD_LD(imm, rs1, rd) = {
+  assert(xlen == 32);
+  let access = Load(Data);
+  match vmem_read(rs1, sign_extend(imm), 4, access, false, false, false) {
+    Ok(lo) => {
+      match vmem_read(rs1, sign_extend(imm + 4), 4, access, false, false, false) {
+        Ok(hi) => { X_pair(rd) = hi @ lo; RETIRE_SUCCESS },
+        Err(e) => e,
+      }
+    },
+    Err(e) => e,
+  }
+}
+mapping clause assembly = ZILSD_LD(imm, rs1, rd) <-> "ld" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"
+
+
+/* ****************************************************************** */
+union clause instruction = ZILSD_SD : (bits(12), regidx, regidx)
+
+$[wavedrom "offset[11:5] src base width=D offset[4:0] STORE"]
+mapping clause encdec = ZILSD_SD(imm, rs2, rs1)
+  <-> imm[11 .. 5] @ encdec_reg(rs2) @ encdec_reg(rs1) @ 0b011 @ imm[4 .. 0] @ 0b0100011
+  when currentlyEnabled(Ext_Zilsd) & validZilsdReg(rs2)
+
+function clause execute ZILSD_SD(imm, rs2, rs1) = {
+  assert(xlen == 32);
+  let value = X_pair(rs2);
+  let access = Store(Data);
+  match vmem_write(rs1, sign_extend(imm), 4, value[31 .. 0], access, false, false, false) {
+    Ok(_)  => {
+      match vmem_write(rs1, sign_extend(imm + 4), 4, value[63 .. 32], access, false, false, false) {
+        Ok(_)  => RETIRE_SUCCESS,
+        Err(e) => e,
+      }
+    },
+    Err(e) => e,
+  }
+}
+
+mapping clause assembly = ZILSD_SD(offset, rs2, rs1) <-> "sd" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_12(offset) ^ "(" ^ reg_name(rs1) ^ ")"

model/postlude/validate_config.sail

@@ -373,6 +373,27 @@ private function check_stateen_config() -> bool = {
   valid
 }
 
+private function check_required_zilsd_zclsd_option() -> bool = {
+  var valid : bool = true;
+  if xlen != 32 & (hartSupports(Ext_Zilsd) | hartSupports(Ext_Zclsd)) then {
+    valid = false;
+    print_endline("Zilsd and Zclsd are only available on RV32");
+  };
+  if hartSupports(Ext_Zclsd) & not(hartSupports(Ext_Zilsd)) then {
+    valid = false;
+    print_endline("The Zclsd extensions is enabled but Zilsd is disabled: supporting Zclsd requires Zilsd.");
+  };
+  if hartSupports(Ext_Zclsd) & not(hartSupports(Ext_Zca)) then {
+    valid = false;
+    print_endline("The Zclsd extensions is enabled but Zca is disabled: supporting Zclsd requires Zca.");
+  };
+  if (hartSupports(Ext_Zclsd) & hartSupports(Ext_Zcf)) then {
+    valid = false;
+    print_endline("Both Zclsd and Zcf extensions are enabled: Zclsd is incompatible with Zcf.");
+  };
+  valid
+}
+
 function config_is_valid() -> bool = {
     check_privs()
   & check_mmu_config()
@@ -383,4 +404,5 @@ function config_is_valid() -> bool = {
   & check_misc_extension_dependencies()
   & check_extension_param_constraints()
   & check_stateen_config()
+  & check_required_zilsd_zclsd_option()
 }

model/riscv.sail_project

@@ -381,6 +381,11 @@ extensions {
     }
   }
 
+  Zclsd {
+    requires core, sys, Zilsd
+    files extensions/Zclsd/zclsd_insts.sail
+  }
+
   Zicond {
     requires core
 
@@ -464,6 +469,11 @@ extensions {
     files extensions/Zihintpause/zihintpause_insts.sail
   }
 
+  Zilsd {
+    requires core, sys
+    files extensions/Zilsd/zilsd_insts.sail
+  }
+
   Ssqosid {
     requires core
     files extensions/Ssqosid/ssqosid.sail

test/first_party/CMakeLists.txt

@@ -106,6 +106,9 @@ add_first_party_test("test_pmp_access.c")
 add_first_party_test("test_phys_perms_on_failing_sc.S")
 add_first_party_test("test_wfi_wait.S")
 
+add_first_party_test_with_config("test_zilsd.S" "rv32gcv" 32 "no_override.json")
+add_first_party_test_with_config("test_zclsd.S" "rv32gv"  32 "test_zclsd.json")
+
 list(LENGTH tests tests_len)
 math(EXPR test_last "${tests_len} - 1")
 foreach(idx RANGE 0 ${test_last} 4)