Fix error in senvcfg definition

[ved-rivos]

1. The following statement is incorrect. SXLEN can be 64-bit in RV64. Using same type places fields that do not exist in senvcfg in the senvcfg register.

// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two
// upper fields so for simplicity we can use the same type.

2. The menvcfg and senvcfg should be legalized separately as they do not hold identical fields.

3. senvcfg is SXLEN wide and not 64-bit wide.

[Timmmm]

Good spot. I don't think there's any issue using the same type for both since the lower 32 bits are the same? However we have ended up splitting the legalize functions up as you have done here so I think that is a good idea (also needed for PBMT).

[Timmmm]

Does this actually compile on RV32? You have v as 64-bit and SEnvcfg as 32-bit.

[ved-rivos]

Ah. v should also be xlenbits. I will fix that. SEnvcfg is not 32-bit - its xlenbits

[ved-rivos]

This is fixed.

[ved-rivos]

Good spot. I don't think there's any issue using the same type for both since the lower 32 bits are the same? However we have ended up splitting the legalize functions up as you have done here so I think that is a good idea (also needed for PBMT).

senvcfg is not 32-bits - its xlenbits i.e. SXLEN wide and xlenbits is 64-bits on RV64.

[Timmmm]

senvcfg is not 32-bits - its xlenbits i.e. SXLEN wide and xlenbits is 64-bits on RV64.

Correct, but the code to read/write senvcfg ignores the top half so it makes no difference that the underlying type you're using is 64 bits. Unless I'm missing something?

[ved-rivos]

Correct, but the code to read/write senvcfg ignores the top half so it makes no difference that the underlying type you're using is 64 bits. Unless I'm missing something?

The underlying type is not 64 bits. Its xlenbits - xlenbits is 32 or 64 based on xlen. When both MXLEN and SXLEN are 64-bit, the current implementation would allow storing setting PBMTE/ADUE/STCE/CDE bits in senvcfg.

The common legalizer is also a problem because it does not allow legalizing senvcfg based on menvcfg as needed by some ISA extensions - such as this rule - "The Zicfiss extension adds the SSE field (bit 3) to menvcfg. When the SSE field is set to 1 the Zicfiss extension is activated in S-mode. Zicfiss extension introduces the SSE field (bit 3) in senvcfg. When menvcfg.SSE field is 0, the henvcfg.SSE and senvcfg.SSE fields will read as zero and are read-only. "

[Timmmm]

The underlying type is not 64 bits.

I mean the underlying type of bitfield [S]Envcfg : bits(64) = { which is 64 bits.

When both MXLEN and SXLEN are 64-bit, the current implementation would allow storing setting PBMTE/ADUE/STCE/CDE bits in senvcfg.

Right, but we fixed (privately) that just by splitting the legalize functions. I still don't think there's any need to split the register type. Here's our current code:

// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two
// upper fields so for simplicity we can use the same type.
bitfield Envcfg : bits(64) = {
  // Supervisor TimeCmp Extension. Not present in senvcfg.
  STCE   : 63,
  // Page Based Memory Types Extension. Not presetn in senvcfg.
  PBMTE  : 62,
  // Cache Block Zero instruction Enable
  CBZE   : 7,
  // Cache Block Clean and Flush instruction Enable
  CBCFE  : 6,
  // Cache Block Invalidate instruction Enable
  CBIE   : 5 .. 4,
  // Reserved WPRI bits.
  wpri_0 : 3 .. 1,
  // Fence of I/O implies Memory
  FIOM   : 0,
}

function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
  let v = Mk_Envcfg(v);
  let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
  let o = update_CBZE(o, v.CBZE());
  let o = update_CBCFE(o, v.CBCFE());
  let o = update_CBIE(o, if v.CBIE() != 0b10 then v.CBIE() else 0b00);
  let o = update_PBMTE(o, if sys_pbmte_always_enabled() then 0b1 else if sys_pbmte_always_disabled() then 0b0 else v.PBMTE());

  // Other extensions are not implemented yet so all other fields are read only zero.
  o
}

function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
  let v = Mk_Envcfg(v);
  let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
  let o = update_CBZE(o, v.CBZE());
  let o = update_CBCFE(o, v.CBCFE());
  let o = update_CBIE(o, if v.CBIE() != 0b10 then v.CBIE() else 0b00);

  // Other extensions are not implemented yet so all other fields are read only zero.
  o
}

// Write senvcfg:
    (0x10A,  _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) },
// Read senvcfg:
    (0x10A,  _) => senvcfg.bits()[sizeof(xlen) - 1 .. 0],

This implementation does not allow storing PBMTE etc. in senvcfg because we split the legalize functions like you have. I'm totally open to splitting the bitfields too on the basis of readability but it isn't necessary from a functional correctness point of view.

Maybe need a third opinion on the readability. I guess since you changed it that's at least one data point that having both registers use the same type is confusing!

[ved-rivos]

Maybe need a third opinion on the readability. I guess since you changed it that's at least one data point that having both registers use the same type is confusing!

We should have the formal model to be clear about the types. And if someday documentation is going to be generated, as envisioned, from sail then this will be not very helpful.

[Timmmm]

I don't really know much about the formal models (will defer to @arichardson / @Alasdair there). Good point about the documentation though. You can generate register diagrams from Sail's bitfield and that's going to work much better with separate types.

[github-actions]

Test Results

712 tests  ±0   712 ✅ ±0   0s ⏱️ ±0s
  6 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 6c0b7ab. ± Comparison against base commit 9602e3a.