Simplify and fully specify xscratchcsw[l]

[Timmmm]

I think the specification for xscratchcsw[l] could be significantly simplified and tightened up to avoid implementation defined behaviour by changing it to be something like this:

xscratchcsw and xscratchcswl have behaviour that depends on a condition, respectively:

• the current privilege is not equal to the previous privilege
• the current interrupt level ....

If the condition is true, then csr* rd, xscratchcsw[l], rs1/imm behaves the same as csr* rd, xscratch, rs1/imm. Otherwise it behaves the same as mv rd, rs1/imm.

This is way simpler to understand, and avoids all of the ambiguity around csrs and csrc. It's the most obvious thing to do, and it is also what we have implemented in the Sail model (not upstreamed yet) and in our designs.

Potentially something similar could be done for xnxti but I haven't fully understood that bit of the spec yet.

[xiaoweish]

For mscratchcsw, the formal description is used as below, whereas others use pseudo-code. Would it be better to use pseudo-code consistently for all, to improve uniformity and readability? For instance, the use of _ in the formal description might not be immediately intuitive to all readers.

csrrw rd, mscratchcsw, rs1

match cur_privilege {
  Machine => match mstatus.MPP() {
    Machine => rd = rs1; // mscratch unchanged.
    _       => t = rs1; rd = mscratch; mscratch = t; /* default: for all other priv modes*/
  }
}

[Timmmm]

That's Sail code; I think it's ok to use that. It doesn't really match how we actually implemented it, so it would maybe be worth updating when/if the code below is merged into the upstream Sail repo.

This code implements my suggested specification.

It's also quite annoying that all of the Sail samples are for machine mode, because it leaves open questions about how things should behave when the CSR privilege doesn't match the current privilege (see the TODO for example; there's no way of telling the answer from the spec).

function currentPrivilegeMatchesPrevious() -> bool =
  match cur_privilege() {
    Machine => mstatus[MPP] == 0b11,
    Supervisor => mstatus[SPP] == 0b1,
    User => true,
  }

...

function clause read_CSR(0x348, write_val) = if not(currentPrivilegeMatchesPrevious()) then get_mscratch() else write_val // mscratchcsw
function clause read_CSR(0x349, write_val) = if (mcause[Xpil] == zeros()) != (mil == zeros()) then get_mscratch() else write_val // mscratchcswl
function clause read_CSR(0x148, write_val) = if not(currentPrivilegeMatchesPrevious()) then get_sscratch() else write_val // sscratchcsw
function clause read_CSR(0x149, write_val) = if (scause[Xpil] == zeros()) != (sil == zeros()) then get_sscratch() else write_val // sscratchcswl

// The return value from the write functions is not used except for logging
// so it doesn't really need to makes sense.

// mscratchcsw
function clause write_CSR(0x348, value) = {
  if not(currentPrivilegeMatchesPrevious()) then set_mscratch(value);
  value
}

// mscratchcswl
function clause write_CSR(0x349, value) = {
  if (mcause[Xpil] == zeros()) != (mil == zeros()) then set_mscratch(value);
  value
}

// sscratchcsw
function clause write_CSR(0x148, value) = {
  if not(currentPrivilegeMatchesPrevious()) then set_sscratch(value);
  value
}

// sscratchcswl
function clause write_CSR(0x149, value) = {
  // TODO (CLIC): Should this always use s[p]il, or should it use x[p]il based
  // on the current privilege mode.
  if (scause[Xpil] == zeros()) != (sil == zeros()) then set_sscratch(value);
  value
}