-
Notifications
You must be signed in to change notification settings - Fork 188
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add Svnapot and Svpbmt extensions #393
base: master
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
extPte is used by sail-cheri-riscv. Being an ext* thing it's not to be used in the standard model lest you break such downstream use cases.
The extPte is a misnomer in the current model as being something to be used for non-standard extensions. These bits are reserved for standard extensions. CHERI use of these will be a non-conforming extension which is fine and CHERI should get added accordingly. Non-tree non-standard extensions should not be using bits reserved for future standard use. I think CHERI should define a new virtual memory system mode where it can put new non-RISC-V interpretations on these bits. |
It's ext not stdExt, and there was no non-reserved way to extend the page table format in a custom extension at the time it was created. I am just asking you to not break existing uses of the model, one that has been around for many years and was developed at the same time and influenced the design of the base Sail model. |
If a custom extension needs to redefine PTE layout then the right way would be to use a custom |
CHERI-RISC-V predates all of that. So no, we're not changing what was specified in the past. Ratified CHERI-RISC-V is on the way and will be standard, whatever that means for the design, but we are not changing our current specification. You may not care about CHERI, but CHERI-RISC-V is a big reason the base model exists at all. I'm not saying not to add Svpbmt and Svnapot support, I'm saying to add it in such a way that the existing CHERI-RISC-V model can opt out of it. Otherwise you are breaking a real-world use case that the model has always been intended to support from the very first moment it was written. |
It likely does predate but this repo is the RISC-V reference model and that is the primary goal. Serving non tree extensions would be secondary goal. As to how to make an out of tree usage that conflicts with the base RISC-V architecture work I lack enough known about CHERI and what its specification is. So suggest you create a PR with a suggestion on how that can be made to work and we can review it here. |
@jrtc27 I agree we should not break CHERI, do you have a suggestion for how we can avoid this? It seems to me like we could have something like:
The base model would then have an implementation of ext_isInvalidPTE that always returns The model uses function prefixed |
That seems sufficient and pretty straightforward. |
@Alasdair The use of those bits in walk39/walk48 will also need to be qualified by haveSvnapot() otherwise the walk if it finds the N bit set will interpret the PTE to be in Svnapot form. This should be a small update. I will push an update with this idea. The haveSvnapot() however is hard coded to true (like all other extensions). Should that be made a command line switch? Or do the out of tree uses have a way around this? |
We don't, so that will need some way to turn it off without modifying non-ext files. |
I will add a command line switch. Maybe its time to add an isa parser.
|
That doesn't really help out-of-tree extensions override it, because the command-line switch lives in the .c and .ml files, so you'd be requiring sail-cheri-riscv users to always disable Svnapot on the command-line, which is not a helpful interface. It needs to be disableable statically at build time without modifying non-ext files. |
I planned to have a command line switch to enable it and not disable. The current practice of statically enabling every extension in Sail RISC-V model is a problem because people cannot use it without code modification as a reference model. This switch will be temporary and we should have a ISA string parser so people can customize the reference to their DUT specific configuration without needing source changes. |
Ok, off-by-default works. |
Updated as follows:
|
I'm working on a test framework as the current framework doesn't allow
for testing of things like command line switches. I'll be presenting at the
tech-golden-model meeting on 2024-1-29.
Bill Mc.
…On Mon, Jan 22, 2024 at 12:50 PM Ved Shanbhogue ***@***.***> wrote:
Updated as follows:
1. Add --enable-svnapot and --enable-svpbmt command line switches. In
tree usages will need to provide the switch to explicitly enable the RISC-V
standard extensions. Out of tree usages will not have to do more work.
2. Add ext_isInvalidPTE - returns invalid, valid, or standard. If
custom extension check fails should return invalid. To skip standard
extension checks returns valid. Default is to invoke standard extension
checks. Renamed ext_pte to avoid std_ext.
3. Dropped the test while we figure out what the test framework for
the model should be and how to integrate that into CI.
—
Reply to this email directly, view it on GitHub
<#393 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AXROLOHUFCIYEBYID24QIBDYP3GJZAVCNFSM6AAAAABCDRGRN2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMBUG44DGNZZGA>
.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
--
Bill McSpadden
Formal Verification Engineer
RISC-V International
mobile: 503-807-9309
|
@jrtc27 - Did that address the change requested? |
afc3dd6
to
31658df
Compare
@ved-rivos Quick question: given that purpose of Svpbmt is overriding of PMAs, how and where do you expect PMA checks to access the relevant bits 62–61 of a leaf page table entry? |
@martinberger - for each load/store/instruction-fetch, we would first determine the PBMT from bits 62:61 of the PTE entry that provides its system physical address. If the PBMT is IO or NC then those attributes apply. If PBMT=PMA, then the attributes associated with the system physical address apply. In cases where PBMT is IO or NC, rest of the attributes that apply may be those associated with system physical address or an implementation may override them as well (e.g., an implementation may not support AMO PMAs for IO memory). |
But where is that being captured in the model? |
There are no PMAs modeled afaict. |
Sure. That makes sense. Let me add that to the bundle. |
One possible way could be to change
(This is not the only way) |
Is there a requirement that unions cannot be > 64 bits. I get this error with:
|
There is no such requirement. This looks like a Sail compiler bug because it is the C-compiler complaining. Several such |
I have - Sail 0.17.1 (sail @ opam-v2.1.2) |
That's an old version and will fail on the problem I reported in rems-project/sail#401. I think that's the same problem you are seeing. That problem was fixed last year. I suggest that you upgrade to a new version of the compiler. I don't know if the fix has already reached the official version that is distributed with |
There isn't a newer version tagged, and opam is just pointing at the 0.17.1 tag. Sounds like we need a new release? |
Yes, a new opam version would be good---Alasdair did a lot of work on the Compiler. |
Updating the union declaration fixes the error:
|
Updated to provide the PBMT bits (and other standard extension bits) along with the translation results to load/store/instruction-fetch. |
@martinberger - does this look good? Are further changes needed? |
@ved-rivos LGTM (modulo trimming trailing whitespace etc to get past the code format checkers). We should try and get it in soon. |
ce59d0a
to
9919687
Compare
@Timmmm and I were thinking that it'd be better to convert the two PBMT bits directly at the source to a suitable symbolic representation and then send that to the PMA checks. That would give us stronger type-checks, and, at the same time, serve as documentation. How about this:
|
The code presently provides all the extended PTE bits along. The PBMT bits have been checked for reserved encodings at the source. The expectation is that at the destination - such as PMA checks - the extended PTE bits will intrepreted as PTE_Ext_Flags and then mapped to the symbolic name. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me. There are some minor style issues but easy to fix.
model/riscv_sys_regs.sail
Outdated
@@ -837,6 +849,7 @@ register senvcfg : SEnvcfg | |||
function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { | |||
let v = Mk_MEnvcfg(v); | |||
let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; | |||
let o = [o with PBMTE = if haveSvpbmt() then v[PBMTE] else 0b0]; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Minor style thing but you can just add this into the previous line like
[o with
FIOM = ...,
PBMTE = ...
]
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
updated.
model/riscv_vmem.sail
Outdated
@@ -151,7 +152,10 @@ function pt_walk(sv_params, | |||
let mask_bits = level * sv_params.pte_PPN_j_size_bits; | |||
// Clear the lowest `mask_bits` bits. | |||
let ppns_masked = (ppns >> mask_bits) << mask_bits; | |||
if not(ppns == ppns_masked) then | |||
if haveSvnapot() & ext_pte_flags[N] == 0b1 then | |||
// Superpage NAPOT PTEs are invalid |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would it make more sense to pass the level
to pte_is_invalid
and do this check there?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
updated.
model/riscv_vmem.sail
Outdated
// Only 64K NAPOT PTEs are valid | ||
PTW_Failure(PTW_Invalid_PTE(), ext_ptw) | ||
} else { | ||
let final_ppn : bits(64) = match (haveSvnapot(), ext_pte_flags[N]) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I really think an if
is clearer for these sorts of things. Also you can just reuse the ppns
name. And use @
instead of append
.
let ppns = if haveSvnapot() & ext_pte_flags[N] == 0b1
then ppns[63 .. 4] @ vpn_j[3 .. 0]
else ppns;
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
updated.
model/riscv_vmem_pte.sail
Outdated
bitfield PTE_Ext_Flags : extPte = { | ||
N : 9, | ||
PBMT : 8 .. 7, | ||
RSVD : 6 .. 0 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Minor but can we style this like reserved
so it doesn't look like it is an actual field?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
updated.
@@ -275,8 +286,8 @@ function write_pte forall 'n, 'n in {4, 8} . ( | |||
// Result of address translation | |||
|
|||
// PUBLIC | |||
union TR_Result('paddr : Type, 'failure : Type) = { | |||
TR_Address : ('paddr, ext_ptw), | |||
union TR_Result('paddr : Type, 'ext_pte_bits : Type, 'failure : Type) = { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ext_pte_bits
is always extPte
- is there any point parameterising it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
please explain more.
model/riscv_vmem_pte.sail
Outdated
@@ -51,10 +58,33 @@ function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0) | |||
& (pte_flags[W] == 0b0) | |||
& (pte_flags[R] == 0b0) | |||
|
|||
// Extension hooks can request standard PTE validity checks by returning Ext_PTE_Std | |||
union Ext_isInvalPTE_Check = { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
enum
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
updated.
pte_ext_flags[N] != 0b0 | pte_ext_flags[PBMT] != 0b00)) | ||
} | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this can be simplified a bit. Here's our version, IIRC I based it on yours.
function pte_is_invalid(pte_flags : PTE_Flags, pte_ext : PTE_Ext) -> bool =
match ext_pte_validity(pte_flags, pte_ext) {
Ext_PTE_Invalid => true,
Ext_PTE_Valid => false,
Ext_PTE_Std =>
pte_flags[V] == 0b0
| (pte_flags[W] == 0b1 & pte_flags[R] == 0b0)
// These bits must be zero unless the relevant extension is supported
// and this is a leaf node.
| pte_ext[N] != zeros() & (not(haveSvnapot()) | pte_is_ptr(pte_flags))
| pte_ext[PBMT] != zeros() & (not(haveSvpbmt()) | pte_is_ptr(pte_flags))
// PBMT 0b11 is always reserved. This applies even without PBMT support.
| pte_ext[PBMT] == 0b11
// Reserved bits must be 0.
| pte_ext[reserved] != zeros()
}
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This version is missing a few things:
- A, D, and U flags are reserved in non-leaf PTEs
- PBMT is reserved if menvcfg.PBMTE is 0
- N bit is reserved for superpage leaf PTEs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
updated.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@Timmmm - let me know if any other changes are needed.
75d7b42
to
4ba998f
Compare
No description provided.