Add Zilsd/Zclsd Support

[trdthg]

spec: https://github.com/riscv/riscv-zilsd/blob/main/zilsd.adoc#insns-sd

• zilsd:
  • RV32 only
  • load/store 64 bit value
  • has same assembly with 2.6. Load and Store Instructions
• zclsd:
  • RV32 only
  • load/store 64 bit value
  • has same assembly with 26.3. Load and Store Instructions
  • compressed
  • base = rs1 or stack_pointer
  • has overlapping encodings with Zcf

function clause extensionEnabled(Ext_Zclsd) = true & xxx is a placeholder, waiting for config system

[github-actions]

Test Results

2 314 tests  ±0   2 314 ✅ ±0   32m 0s ⏱️ -6s
    1 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit ba2adbe. ± Comparison against base commit 9397607.

♻️ This comment has been updated with latest results.

[nadime15]

I'm curious, wouldn't it make more sense to replace LOAD_RV32 (and STORE_RV32) with two sequential 32-bit load/store operations instead of one 64-bit load/store operation?

Most 32-bit systems have a 32-bit memory bus, so performing two 32-bit accesses would be more realistic than a single 64-bit access on such hardware.

This implementation would also allow us to test the more interesting case where interrupts could occur between the two operations, as explicitly permitted by the Zilsd specification.

[trdthg]

That's definitely a good idea, I didn't think of that

[pmundkur]

LOAD_DOUBLE might be a better name for the AST constructor than LOAD_RV32. It's unfortunate that the spec re-uses LOAD. (Could we ask the spec authors to change this before ratification?) Similarly for STORE_RV32.

[trdthg]

I saw your reply at riscvarchive/riscv-zilsd#64, so I update it to the format of EXT_INST(ZILSD_LD...).

[christian-herber-nxp]

how does this relate to #490?

[trdthg]

how does this relate to #490?

I didn't see it before. Currently, the code mainly has the following differences

• zcmlsd -> zclsd
• directly concat the 0 at the end of the imm to the ast
• ast naming inconsistency (adopted theirs, I haven't added co-authored-by yet because I don't know his email)
• simply execute
• TODO some refactor based on the new features of sail
  • Update mappings to use the when construct for guards #768
  • Replace ad-hoc model configuration with Sail-native configuration #758

[pmundkur]

@trdthg Could you check with @christian-herber-nxp to make sure we're not missing anything from #490 and we get the appropriate co-authors?

[christian-herber-nxp]

the author of the original PR should be clear from that, it is @simonacostinescu

[trdthg]

Update

I am trying to run act tests (there is already a PR, not merged yet), but encountered a few problems

• riscv-config Updating Load/Store Pair for RV32 to version 0.10 riscv-software-src/riscv-config#189 waiting for merge
• the tests have some issue(seems about ISA constrains), I'm doing some fix done
• gcc zilsd/zclsd support not merged yet(and it's not complete, some orgs have complete version, but lack maintenance, need rebase), trying with clang / compile gcc locally

I think you could review this after I finished those tests.

Co-authored-by already added

[trdthg]

Rebased. I also added two first-party tests. Since I need to specify specific config for these two tests, I changed the CMake a lot and introduced two python scripts:

• test/first_party/scripts/test_matrix.py: Used to define configs for different tests, where you can specify -match, xlen, and an override parameter to indicate which fields in the default JSON should be overridden. CMake is not good at defining such data structure.
• test/first_party/scripts/merge_config.py: Used to merge override_json and default_json. because jq dosn't support our comments in json.

Btw, I don't really understand how to properly write $[wavedrom], such as how each segment maps to sail and the meaning of various _ symbols. For now, I just copied the attr fields directly from the manual:

{reg: [
  {bits: 2, name: 0x2,      type: 8, attr: ['C2']},
  {bits: 5, name: 'rs2',    type: 4, attr: ['src, src[0]=0']},
  {bits: 6, name: 'imm',    type: 3, attr: ['offset[5:3|8:6]']},
  {bits: 3, name: 0x7,      type: 8, attr: ['C.SDSP']},
], config: {bits: 16}}

[Timmmm]

I've been really really really trying to avoid adding any Python, since it usually ends up being a complete nightmare. It's not quite so bad these days with uv but if we do add any we will have to do the whole pyproject.toml, Pyright, Pylint stuff.

My strong preference would be to use almost anything other than Python. Maybe Deno.

[Timmmm]

This should use ExecuteAs.

[Timmmm]

We have X_pair for this.

[Timmmm]

This is incorrect. It will write to x1 if you load into x0. I'd use X_pair here too.

[Timmmm]

For C.LDSP, usage of x0 as the destination is reserved.

[Timmmm]

These compressed encodings are missing the odd register check I think?

Also double check how we do it for the other instructions that only allow even registers (Zfinx). We have a config setting to configure that behaviour so we should make the code the same style at least.

[Timmmm]

I think this is only supported on RV32 so this should be

Suggested change

	"supported": true
	"supported": @CONFIG_XLEN_IS_32@

Also we should probably add a check to validate_config.sail to make sure you don't set this on RV64.

[arichardson]

I've been really really really trying to avoid adding any Python, since it usually ends up being a complete nightmare. It's not quite so bad these days with uv but if we do add any we will have to do the whole pyproject.toml, Pyright, Pylint stuff.

My strong preference would be to use almost anything other than Python. Maybe Deno.

I think python is fine as long as it is limited to 3.8 (or whatever the version in RHEL8 is) with only the standard library. Otherwise I agree that it can be a dependency hell.

[arichardson]

This script shouldn't be too difficult to write in CMake?

[trdthg]

done

[Timmmm]

I haven't used any third-party libraries in the scripts, so it‘s not necessary to introduce uv or any other management tools.

Yeah but third party libraries always creep in so even in that case you need to start with a proper setup. If we do start using Python we're going to end up using at least Pydantic and Typer.

As for Deno, I feel that anything requiring extra installation won't be easily accepted.

Deno is easier to install than Python + uv. It's literally one command. I don't think the avoidance of a single command is worth the pain of Python.

What if we just rewrite those two scripts in cpp?

I think that's a good idea.

[trdthg]

Lean is not happy again. But this is a bit tricky because Zcf and Zclsd seem to be at the same level.

It(Zclsd) has overlapping encodings with Zcf and is thus incompatible with Zcf.

The error msg is

  error: LeanRV64D/PlatformConfig.lean:5680:20: failed to prove termination, possible solutions:
    - Use `have`-expressions to prove the remaining goals
    - Use `termination_by` to specify a different well-founded relation
    - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
  ⊢ max (currentlyEnabled_measure Ext_Zclsd) 0 < currentlyEnabled_measure Ext_Zcf
  error: Lean exited with code 1
  Some required targets logged failures:
  - LeanRV64D.PlatformConfig

but if you write Zcf > Zclsd

    Ext_Zcf => 3, // > C
    Ext_Zclsd => 2, // > C

It will become:

⊢ max (currentlyEnabled_measure Ext_Zcf) 0 < currentlyEnabled_measure Ext_Zclsd

[Timmmm]

Much better! The --config-override thing seems to be a lot simpler and nicer than I would have guessed. I think it needs to go in its own PR though.

[pmundkur]

Looks pretty close; just minor fixes.

[pmundkur]

@trdthg i made some minor fixes, hope that's okay. I wonder what you think about the TODO I left.

[trdthg]

LGTM. For the alignment issue, my current thought is to either modify the function definitions directly or overload [vmem_read_addr, vmem_write_addr, vmem_read, vmem_write], let them accept an align_width parameter. For example:

diff --git a/model/extensions/Zilsd/zilsd_insts.sail b/model/extensions/Zilsd/zilsd_insts.sail
index 60c7fd7b..4ea5f8a2 100644
--- a/model/extensions/Zilsd/zilsd_insts.sail
+++ b/model/extensions/Zilsd/zilsd_insts.sail
@@ -29,9 +29,10 @@ mapping clause encdec = ZILSD_LD(imm, rs1, 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) {
+  let align_width = if true then 8 else 4;
+  match vmem_read(rs1, sign_extend(imm), 4, align_width, access, false, false, false) {
     Ok(lo) => {
-      match vmem_read(rs1, sign_extend(imm + 4), 4, access, false, false, false) {
+      match vmem_read(rs1, sign_extend(imm + 4), 4, align_width, access, false, false, false) {
         Ok(hi) => { X_pair(rd) = hi @ lo; RETIRE_SUCCESS },
         Err(e) => e,
       }
diff --git a/model/sys/vmem_utils.sail b/model/sys/vmem_utils.sail
index a54d44f2..4dde6a74 100644
--- a/model/sys/vmem_utils.sail
+++ b/model/sys/vmem_utils.sail
@@ -130,14 +130,14 @@ private function access_causes_misaligned_exception(
 
 // External API
 
-val vmem_read_addr : forall 'width, is_mem_width('width).
-  (virtaddr, xlenbits, int('width), MemoryAccessType(mem_payload), bool, bool, bool)
+val vmem_read_addr_with_custom_align : forall 'width 'align_width, is_mem_width('width) & is_mem_width('align_width).
+  (virtaddr, xlenbits, int('width), int('align_width), MemoryAccessType(mem_payload), bool, bool, bool)
   -> result(bits(8 * 'width), ExecutionResult)
 
-function vmem_read_addr(vaddr, offset, width, access, aq, rl, res) = {
+function vmem_read_addr_with_custom_align(vaddr, offset, width, align_width, access, aq, rl, res) = {
   // "LR faults like a normal load, even though it's in the AMO major opcode space."
   // - Andrew Waterman, isa-dev, 10 Jul 2018.
-  if access_causes_misaligned_exception(vaddr, width, res)
+  if access_causes_misaligned_exception(vaddr, align_width, res)
   then return Err(Memory_Exception(vaddr, E_Load_Addr_Align()));
 
   // If the load is misaligned or an allowed misaligned access, split into `n`
@@ -180,6 +180,16 @@ function vmem_read_addr(vaddr, offset, width, access, aq, rl, res) = {
   Ok(data)
 }
 
+val vmem_read_addr_with_width_align : forall 'width, is_mem_width('width).
+  (virtaddr, xlenbits, int('width), MemoryAccessType(mem_payload), bool, bool, bool)
+  -> result(bits(8 * 'width), ExecutionResult)
+
+function vmem_read_addr_with_width_align(vaddr, offset, width, access, aq, rl, res) = {
+  vmem_read_addr_with_custom_align(vaddr, offset, width, width, access, aq, rl, res)
+}
+
+overload vmem_read_addr = { vmem_read_addr_with_width_align, vmem_read_addr_with_custom_align }
+
 // This lets the Rocq extraction know why the repeat loop above terminates
 termination_measure vmem_read_addr repeat n
 
@@ -252,11 +262,11 @@ function vmem_write_addr(vaddr, width, data, access, aq, rl, res) = {
 // This lets the Rocq extraction know why the repeat loop above terminates
 termination_measure vmem_write_addr repeat n
 
-val vmem_read : forall 'width, is_mem_width('width).
-  (regidx, xlenbits, int('width), MemoryAccessType(mem_payload), bool, bool, bool)
+val vmem_read_with_custom_align : forall 'width 'align_width, is_mem_width('width) & is_mem_width('align_width).
+  (regidx, xlenbits, int('width), int('align_width), MemoryAccessType(mem_payload), bool, bool, bool)
   -> result(bits(8 * 'width), ExecutionResult)
 
-function vmem_read(rs, offset, width, access, aq, rl, res) = {
+function vmem_read_with_custom_align(rs, offset, width, align_width, access, aq, rl, res) = {
   // Get the address, X(rs1) + offset.
   // Extensions might perform additional checks on address validity.
   let vaddr : virtaddr = match ext_data_get_addr(rs, offset, access, width) {
@@ -264,9 +274,19 @@ function vmem_read(rs, offset, width, access, aq, rl, res) = {
     Ext_DataAddr_Error(e)  => return Err(Ext_DataAddr_Check_Failure(e)),
   };
 
-  vmem_read_addr(vaddr, offset, width, access, aq, rl, res)
+  vmem_read_addr_with_custom_align(vaddr, offset, width, align_width, access, aq, rl, res)
 }
 
+val vmem_read_with_width_align : forall 'width, is_mem_width('width).
+  (regidx, xlenbits, int('width), MemoryAccessType(mem_payload), bool, bool, bool)
+  -> result(bits(8 * 'width), ExecutionResult)
+
+function vmem_read_with_width_align(rs, offset, width, access, aq, rl, res) = {
+  vmem_read_with_custom_align(rs, offset, width, width, access, aq, rl, res)
+}
+
+overload vmem_read = { vmem_read_with_custom_align, vmem_read_with_width_align }
+
 val vmem_write : forall 'width, is_mem_width('width).
   (regidx, xlenbits, int('width), bits(8 * 'width), MemoryAccessType(mem_payload), bool, bool, bool)
   -> result(bool, ExecutionResult)

Or we just add an extra alignment check for Zilsd? This would be the simplest approach. I personally prefer this option. :D

[pmundkur]

I too prefer the simpler approach of an extra alignment check in Zilsd, and making it depend on a configuration option (something like require_8byte_aligned_access).