Add svnapot extention support #510
Conversation
model/riscv_vmem.sail
Outdated
| @@ -45,6 +45,15 @@ function vpn_j_of_va(sv_params : SV_Params, | |||
| ((va >> lsb) & mask) | |||
| } | |||
|
|
|||
| // PRIVATE: Count trailing zeros | |||
| function LowestSetBit(x : bits(64)) -> bits(64) = { | |||
There was a problem hiding this comment.
Funnily enough I have a version of this already that I wrote to demonstrate Sail's fancy type checking:
val count_trailing_zeros : forall 'n, 'n >= 0 . (bits('n)) -> range(0, 'n)
function count_trailing_zeros(x) = {
foreach (i from 0 to ('n - 1)) {
if x[i] == bitone then return i
};
'n
}
However I'm not sure you need this at all - if you check the PMP code it does some clever bit manipulation instead.
|
I check the code in PMP,It really lights me,And I think the additional code would solve the problem.It adds the 64K check.And use the PMP napot bit manipulation to count the napot_mask. And replaced "perfect_one" with zero_extend(0b1).lol :) |
| // For svnapot ext purpose. | ||
| if (pte & (zero_extend(0b1) << 63)) == (zero_extend(0b1) << 63) then { | ||
| if (napot_mask != zero_extend(0xf)) then { | ||
| return PTW_Failure(PTW_Invalid_PTE(), ext_ptw) |
There was a problem hiding this comment.
Did you mean PTW_Unsupported_Napot here?
I'd probably call it PTW_Reserved_Napot btw.
|
|
||
| // For svnapot ext purpose. | ||
| if (pte & (zero_extend(0b1) << 63)) == (zero_extend(0b1) << 63) then { | ||
| if (napot_mask != zero_extend(0xf)) then { |
There was a problem hiding this comment.
Easier like this: napot_mask[3 .. 0] != ones()
| @@ -164,7 +164,30 @@ function pt_walk(sv_params, | |||
| } | |||
| } | |||
| else { | |||
| let mask_bits = level * sv_params.pte_PPN_j_size_bits; | |||
There was a problem hiding this comment.
I haven't gone through the logic properly but are you sure this is right? level is guaranteed to be 0 here.
|
You also need to update |
|
Svnapot was queued by an earlier PR #393 |
|
Svnapot needs to not have an effect when not enabled, so that the bits can be used by another extension. See Svpbmt for a similar case. |
I agree, sorry I forgot about your PR. I think we should close this one in favour of yours which is much more complete. |
No description provided.