-
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
Svadu support #260
base: master
Are you sure you want to change the base?
Svadu support #260
Conversation
I left a couple of comments but mostly looks good to me 👍 |
model/riscv_sys_regs.sail
Outdated
if high == false & sizeof(xlen) == 32 then | ||
c | ||
else { | ||
// If 32bit, then high is true |
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.
Comments are C-style
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.
Changed to C++ style
model/riscv_sys_regs.sail
Outdated
register menvcfg : MEnvCfg | ||
|
||
function legalize_menvcfg(c : MEnvCfg, high : bool, value : xlenbits) -> MEnvCfg = { | ||
if high == false & sizeof(xlen) == 32 then |
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.
not(...)
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.
did not(high)
as requested
32 => value @ 0x0000_0000 | ||
}; | ||
let c = update_HADE(c, [full[61]]); | ||
c |
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 feel like there must be a better way to write all this... is this the first *h CSR we've implemented that's not just a stub 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.
I can't say I'm anywhere close to a SAIL expert. I'm all ears on suggestions here. Thank you!
model/riscv_vmem_sv32.sail
Outdated
@@ -214,6 +210,9 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = | |||
MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") | |||
}; | |||
TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw) | |||
} else { |
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.
Inverting these is a little gratuitous, though perhaps it makes more sense
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.
Changed back the if/then ordering
model/riscv_vmem_tlb.sail
Outdated
|
||
function should_update_PTE_bits() -> bool = { | ||
plat_enable_dirty_update() | (plat_enable_svadu() & menvcfg.HADE() == 0b1) | ||
} |
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.
Missing newline
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.
Added newline back
Your comments appear to be missing |
model/riscv_vmem_sv48.sail
Outdated
/* pte needs dirty/accessed update but that is not enabled */ | ||
TR_Failure(PTW_PTE_Update(), ext_ptw) | ||
} else { | ||
if should_update_PTE_bits() then { |
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.
Is there any reason to swap branch order here instead of using not(should_update_PTE_bits())
? Not objecting to this just wondering why.
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 it's slightly nicer to avoid the not
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 changed it back, figuring that without a clear consensus, I'd minimize the diff.
32 => value @ 0x0000_0000 | ||
}; | ||
let c = update_HADE(c, [full[61]]); | ||
c |
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 let c = ... in c
could just be update_HADE(c, [full[61])
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 tried this, but got an error. So, leaving the let c =
in
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 show the error; it should work just fine
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.
Type error:
model/riscv_sys_regs.sail:585.4-30:
585 | update_HADE(c, [full[61]]);
| ^------------------------^
| No overloading for update_HADE, tried:
| * _update_MEnvCfg_HADE
| MEnvCfg is not a subtype of unit
Any help appreciated!
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.
You need to remove the semicolon at the end because you're returning the value from update_HADE
.
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.
Did you try:
update_HADE(c, [full[61]]);
c
Because that would result in the error you posted, what I meant was:
update_HADE(c, [full[61]])
As the last expression in the block
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.
That did it! Seems obvious now, sorry. Will post a new patch set later, just wanted to quickly share that this did work as you suggested. Thanks!
model/riscv_sys_regs.sail
Outdated
c | ||
else { | ||
// If 32bit, then high is true | ||
let full : bits(64) = match (sizeof(xlen)) { |
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 the brackets around sizeof are not-needed
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.
removed
I'm not very familiar with the RISC-V address translation scheme, but looking a bit deeper at the functionality, I think you also need to update the lookup case for a TLB miss (the None() branch with the Obviously not a task for yourself, but I don't think we need multiple files for the differently sized translations - unless there is significantly differing behaviour I think it could be a single size-polymorphic function. I'm also not sure we are implementing step 7 of the translation process as written in the priv spec, at least I'm not seeing how that is done in the code? I'm wondering about this because the Svadu extension seems to modify this check slightly to avoid a page fault, but I don't see where that is being done. Edit: After some more reading it seems like the A/D bits update is being done in update_PTE_bits in riscv_pte.sail. I am wondering if that needs to be updated (specifically the check on line 147) for this paragraph in the Svadu document?
|
I think we've adjusted the code to handle the additional cases Alasdair raised. Thanks very much for the reviews! |
model/riscv_vmem_tlb.sail
Outdated
@@ -120,3 +120,7 @@ function flush_TLB_Entry(e, asid, addr) = { | |||
& not(e.global)) | |||
} | |||
} | |||
|
|||
function should_update_PTE_bits() -> bool = { | |||
plat_enable_dirty_update() | (plat_enable_svadu() & menvcfg.HADE() == 0b1) |
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 wonder if the logic should be changed such that enable-dirty-update
implicitly enables svadu and sets the initial value of menvcfg.HADE to 1? In that case this function could be simplified to plat_enable_svadu() & menvcfg.HADE() == 0b1
. I believe the --enable-dirty-update flag was only added because there was no Svadu at the time and some operating systems expect the PTE updates.
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.
No, because then you can't configure the model to be an implementation that does A/D updates but doesn't have Svadu, a privileged spec option which was ratified years ago.
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.
That is true, but looking at this PR there are no observable behaviour changes for plat_enable_svadu()/not(plat_enable_svadu()) when plat_enable_dirty_update() is also true? Does this mean we need to also guard write access to menvcfg.HADE by plat_enable_svadu()? Those older implementations should have that bit hardwired to zero (well most likely not have the register at all)?
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.
Yes, HADE shouldn't exist when Svadu isn't enabled, and needs to be legalised as 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.
That makes sense and I agree we should have two separate options to allow matching those implementations.
model/riscv_sys_regs.sail
Outdated
64 => value, | ||
32 => value @ 0x0000_0000 | ||
}; | ||
let c = update_HADE(c, [full[61]]); |
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.
Looking at the Svadu spec I see: When menvcfg.HADE is zero, the implementation behaves as though Svadu were not implemented. If Svadu is not implemented, menvcfg.HADE is read-only zero.
so I believe this needs to be guarded by plat_enable_svadu()
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.
Thanks! I needed to move plat_enable_svadu()
out of riscv_platform.sail
and added a note similar to the one by get_16_random_bits
explaining it, but I made this change
model/riscv_sys_regs.sail
Outdated
64 => value, | ||
32 => value @ 0x0000_0000 | ||
}; | ||
if not(plat_enable_svadu()) |
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.
Isn't this inverted? We should be able to toggle HADE if svadu is enabled.
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.
Good catch. I inverted this and cleaned up the legalize_menvcfg
function. Thank you!
model/riscv_sys_regs.sail
Outdated
function legalize_menvcfg_high(c : MEnvCfg, value : bits(32)) -> MEnvCfg = { | ||
/* Subtract 32 from bit offsets as we only have high half here */ | ||
if plat_enable_svadu() | ||
then update_HADE(c, [value[61 - 32]]) | ||
else c | ||
} |
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.
function legalize_menvcfg_high(c : MEnvCfg, value : bits(32)) -> MEnvCfg = { | |
/* Subtract 32 from bit offsets as we only have high half here */ | |
if plat_enable_svadu() | |
then update_HADE(c, [value[61 - 32]]) | |
else c | |
} | |
function legalize_menvcfg_high(c : MEnvCfg, value : bits(32)) -> MEnvCfg = { | |
let newval = Mk_MEnvCfg(value @ to_bits(32, 0)); | |
if plat_enable_svadu() | |
then update_HADE(c, newval.HADE()) | |
else c | |
} |
How about the following to avoid the subtraction (which will become awkward once we add more fields here.
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.
Thanks! Made the edits and credited you
@adlr - the extension name was changed from Svadu to Svhad. The fields in CSRs continue to be HADE. Just extension name changed. |
Co-authored-by: Aaron Durbin <[email protected]> Co-authored-by: Alex Richardson <[email protected]>
Draft change for Svadu support. I appreciate any feedback on this change. Thank you!
No tests were broken in the
test/run_tests.sh
suite.