Added support of Smepmp in Sail RISCV #196
Conversation
|
You have tabs in your changes |
|
Should I remove tabs that are for indentation? |
|
Yes, as documented in CODE_STYLE.md indentation is two spaces (though some places currently use 4, so divergence to match surrounding style there is fine) |
|
Ok, I will remove them and what about other changes are they fine, and in addition "Do you not also need 0x757 on RV32 for mseccfgh?" I will come back to you about this question a little later. |
|
Added 0x757 on RV32 for mseccfgh. In addition removed the tabs spaces and added two spaces for block level indentation |
|
@marnovandermaas changes you are referring to regarding the MMLcheck function are fixed in a later commit as it was used just once so removed. In addition, the formatting changes are also fixed in a later commit. @jrtc27 @marnovandermaas To fix all problems related to formatting and functionality added that is 0x757 added later I am thinking of squashing two commits of formatting into my first commit and will separate the last commit(of 0x757 added) and its formatting too. As a result now as a final state, We will have only two commits
Please let me know so, I do that for clean commit history. |
HamzaKh01
force-pushed
the
master
branch
2 times, most recently
from
80d2c90 to
5fe3b59
Compare
|
No, RV32 support should be part of the first commit as without it it’s not a complete implementation |
|
@jrtc27 Done. |
Here you are referring to outdated file, in updated it is fixed moved in a single line |
It is fixed completely according to comments |
|
@jrtc27 kindly review this as soon as you get time so, I can wind this up. |
No I wasn't. I opened the up to date file in a text editor before commenting. You still have trailing whitespace, one instance of which is on the line associated with that comment. |
Fixed......... @jrtc27 Please see and let me know if everything is ok now ! |
|
Hi @jrtc27, if everything looks ok now, Can I mention Bill and Martin? because they asked me to inform them, once everything is resolved. Thank you |
Above table can be read as
Entry 1, 5 and 7 explanation from the table
NoteePMP switch is superset of pmp switch as you can infer from the results in table. If ePMP switch is On pmp switch is redundant. Kindly guide me do I have interpreted the behaviour right?? Description of switch provided Both pmp and epmp tests are not merged in the ACT repo, they are for the time being just PR's |
|
Strictly speaking, I think, this should be just like the D extension. IF D
extension is supported, and F-extension must also be supported.
I don't think there is a consistent story about how that is conveyed to
models though. E.g. if misa.F if off, then misa.D must be off, enforced by
hardware.
But there is no equivalent CSR for PMP or ePMP. The question is really -
from a command line perspective:
should ePMP should imply PMP, or must we explicitly list it (and,
therefore, if it isn't listed, riscv-config should report an error.
I don't have strong opinions one way or the other, but I think having it
imply PMP is the way to go.
So it should not be possible to run tests with ePMP support without PMP
support,
and ePMP tests should NOT be run without explicit ePMP support
- the RVTEST_CASE macro conditions should restrict those tests from being
run in that case.
…On Mon, Feb 13, 2023 at 5:15 AM HamzaKh01 ***@***.***> wrote:
-
Used *match* instead of if else at most places now
-
Asked to add command line switch for epmp by Bill, added the switch,
given table summarizes the behaviour of SAIL model
Serial no. Tests ran from ACT command line switch pmp command line switch
epmp No. of tests passed No. of tests failed
1 PMP tests Off Off 7 15
2 PMP tests On Off 22 0
3 PMP tests Off On 22 0
4 PMP tests On On 22 0
5 ePMP tests Off Off 8 63
6 ePMP tests Off On 71 0
7 ePMP tests On Off ModelStuck
8 ePMP tests On On 71 0 Above table can be read as
- As an example take entry 2, Ran PMP tests by turning on the PMP
switch from command line and ePMP switch is off meanwhile, and all of the
22 tests are passing
Entry 1, 5 and 7 explanation from the table
-
If I turn off both the switches then some of the pmp tests are still
passing the reason is these tests are checking maybe just the
configurations set in pmpcfg csr, Switch does not prevent writing these csr
it just prevent the effect of these written csr, if a test is checking
maybe configuration is written properly in the csr then it is passing
despite the switch being on or off (*That is the behaviour of model,
regarding pmp switch, that is already present*)
-
In entry 5 as *I added epmp switch* I infered the same behaviour of
model that exist for pmp switch as explained in above bullet. Some tests
are passing despite switch is off because they may be checking bits that
are set in mseccfg but the effect that these bits will cause is prevented
because switch is off
-
In entry 7 model is stuck because i am running epmp tests by turning
on pmp switch and turning off epmp switch. PMP extension does not translate
the pmpcfg csr as epmp extension does and tests are written to check epmp
behaviour that is why model is stuck in a test (Note it is expected
behaviour)
Note
ePMP switch is superset of pmp switch as you can infer from the results in
table. If ePMP switch is On pmp switch is redundant. Kindly guide me do I
have interpreted the behaviour right??
Description of switch provided I will add a command line switch,
"--Smepmp" that will enable the feature. Default behaviour is to NOT enable
the feature. I will export a function, "haveSmepmp()", to the Sail model
which will return true if the switch is set, false if it is not. You will
need to enable/disable based on this function's return value. Used
function haveSmepmp() in line 69 and 70 of riscv_pmp_regs.sail compiled
the model multiple times with true and false output to check behaviour
written in above table. One confusion is Do i have to keep lines 69 and 70
of riscv_pmp_regs.sail because for the moment I do not have the function
haveSmepmp() it will not compile without it. because I have used that at
numerous places
Both pmp and epmp tests are not merged in the ACT repo, they are for the
time being just PR's
—
Reply to this email directly, view it on GitHub
<#196 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJSVCIPIGUH7VUIIO6TWXIXYPANCNFSM6AAAAAAS7WSCWA>
.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
|
Note from the discussion this morning:
The switches that I proposed (--Smepmp and --Zicond) will not be
implemented.
Rather, we will follow the nomenclature the LLVM uses in the -march string.
The Sail functional interface will be the same as what I proposed.
Bill Mc.
On Tue, Feb 14, 2023 at 10:03 AM Allen Baum ***@***.***>
wrote:
… Strictly speaking, I think, this should be just like the D extension. IF D
extension is supported, and F-extension must also be supported.
I don't think there is a consistent story about how that is conveyed to
models though. E.g. if misa.F if off, then misa.D must be off, enforced by
hardware.
But there is no equivalent CSR for PMP or ePMP. The question is really -
from a command line perspective:
should ePMP should imply PMP, or must we explicitly list it (and,
therefore, if it isn't listed, riscv-config should report an error.
I don't have strong opinions one way or the other, but I think having it
imply PMP is the way to go.
So it should not be possible to run tests with ePMP support without PMP
support,
and ePMP tests should NOT be run without explicit ePMP support
- the RVTEST_CASE macro conditions should restrict those tests from being
run in that case.
On Mon, Feb 13, 2023 at 5:15 AM HamzaKh01 ***@***.***> wrote:
>
> -
>
> Used *match* instead of if else at most places now
> -
>
> Asked to add command line switch for epmp by Bill, added the switch,
> given table summarizes the behaviour of SAIL model
>
> Serial no. Tests ran from ACT command line switch pmp command line switch
> epmp No. of tests passed No. of tests failed
> 1 PMP tests Off Off 7 15
> 2 PMP tests On Off 22 0
> 3 PMP tests Off On 22 0
> 4 PMP tests On On 22 0
> 5 ePMP tests Off Off 8 63
> 6 ePMP tests Off On 71 0
> 7 ePMP tests On Off ModelStuck
> 8 ePMP tests On On 71 0 Above table can be read as
>
> - As an example take entry 2, Ran PMP tests by turning on the PMP
> switch from command line and ePMP switch is off meanwhile, and all of the
> 22 tests are passing
>
> Entry 1, 5 and 7 explanation from the table
>
> -
>
> If I turn off both the switches then some of the pmp tests are still
> passing the reason is these tests are checking maybe just the
> configurations set in pmpcfg csr, Switch does not prevent writing these
csr
> it just prevent the effect of these written csr, if a test is checking
> maybe configuration is written properly in the csr then it is passing
> despite the switch being on or off (*That is the behaviour of model,
> regarding pmp switch, that is already present*)
> -
>
> In entry 5 as *I added epmp switch* I infered the same behaviour of
> model that exist for pmp switch as explained in above bullet. Some tests
> are passing despite switch is off because they may be checking bits that
> are set in mseccfg but the effect that these bits will cause is prevented
> because switch is off
> -
>
> In entry 7 model is stuck because i am running epmp tests by turning
> on pmp switch and turning off epmp switch. PMP extension does not
translate
> the pmpcfg csr as epmp extension does and tests are written to check epmp
> behaviour that is why model is stuck in a test (Note it is expected
> behaviour)
>
> Note
>
> ePMP switch is superset of pmp switch as you can infer from the results
in
> table. If ePMP switch is On pmp switch is redundant. Kindly guide me do I
> have interpreted the behaviour right??
>
> Description of switch provided I will add a command line switch,
> "--Smepmp" that will enable the feature. Default behaviour is to NOT
enable
> the feature. I will export a function, "haveSmepmp()", to the Sail model
> which will return true if the switch is set, false if it is not. You will
> need to enable/disable based on this function's return value. Used
> function haveSmepmp() in line 69 and 70 of riscv_pmp_regs.sail compiled
> the model multiple times with true and false output to check behaviour
> written in above table. One confusion is Do i have to keep lines 69 and
70
> of riscv_pmp_regs.sail because for the moment I do not have the function
> haveSmepmp() it will not compile without it. because I have used that at
> numerous places
>
> Both pmp and epmp tests are not merged in the ACT repo, they are for the
> time being just PR's
>
> —
> Reply to this email directly, view it on GitHub
> <#196 (comment)>,
> or unsubscribe
> <
https://github.com/notifications/unsubscribe-auth/AHPXVJSVCIPIGUH7VUIIO6TWXIXYPANCNFSM6AAAAAAS7WSCWA
>
> .
> You are receiving this because you are subscribed to this thread.Message
> ID: ***@***.***>
>
—
Reply to this email directly, view it on GitHub
<#196 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AXROLOC76PXLZ57TAKDAFE3WXOUDNANCNFSM6AAAAAAS7WSCWA>
.
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
|
|
This:
Surely you can't have Smepmp without the base PMP? That is, surely
haveSmepmp should imply plat_enable_pmp and thus be redundant?
is an interesting point - does Smepmp require PMP, or does Smepmp imply
PMP? - from the point of view of Sail.
Another way of looking at this is: should Sail assume that configurations
passed in are legal, or must it check they are legal?
havePMP and have_SmePMP are passed into Sail - should Sail assume that
the combination have_SmePMP & !have_PMP will never passed in?
If so, then perhaps the answer is that there is a separate checking stage,
and when you get to this code, it is known that illegal combination can't
happen.
The next question is whether this separate checking stage is in Sail or
separate from it (e.g. the riscv-config tool that was designed to
explicitly check for this)
That would mean that Sail can use imply rather than require, which I think
is what Krste has stated in other discussions,
e.g. RV32IMAFD is redundant, because RV32IMAD implies the F.
How is this handled for F and D extensions in Sail?
…On Tue, Apr 25, 2023 at 12:26 AM Jessica Clarke ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In model/riscv_mem.sail
<#196 (comment)>:
> @@ -142,7 +142,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
/* PMP checks if enabled */
function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
- if (~ (plat_enable_pmp ()))
+ if (~ ((plat_enable_pmp ()) | (haveSmepmp())))
Surely you can't have Smepmp without the base PMP? That is, surely
haveSmepmp should imply plat_enable_pmp and thus be redundant?
------------------------------
In model/riscv_pmp_control.sail
<#196 (comment)>:
> + _ => false
+ },
+ (0b1, 0b1, 0b1, 0b1) =>
+ match acc {
+ Read(_) => true,
+ _ => false
+ },
+ (_, _, _, _) =>
+ if (priv == Machine) == pmpLockBit(ent)
+ then pmpCheckRWX(ent, acc)
+ else false
+ },
+ 0b0 =>
+ match priv {
+ Machine => if pmpLockBit(ent)
+ then pmpCheckRWX(ent, acc)
Indentation
------------------------------
In model/riscv_pmp_control.sail
<#196 (comment)>:
> @@ -217,10 +244,19 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) {
PMP_Success => true,
PMP_Fail => false,
- PMP_Continue => match priv {
- Machine => true,
- _ => false
- }
+ PMP_Continue =>
+ match priv {
+ Machine =>
+ if mseccfg.MMWP() == 0b1 & haveSmepmp() /* Make Read, Write and execute denied by default, if condition meets for M mode */
These would be clearer with explicit parentheses (even if in this case
only one association makes sense, since 1 & x is always just x)
------------------------------
In model/riscv_pmp_regs.sail
<#196 (comment)>:
> @@ -66,6 +66,9 @@
/* SUCH DAMAGE. */
/*=======================================================================================*/
+function haveSmepmp() -> bool =
+ return false
No need to return, and can just be a single line
------------------------------
In model/riscv_pmp_regs.sail
<#196 (comment)>:
> @@ -66,6 +66,9 @@
/* SUCH DAMAGE. */
/*=======================================================================================*/
+function haveSmepmp() -> bool =
+ return false
Also why isn't this with the other haveFoo functions?
—
Reply to this email directly, view it on GitHub
<#196 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJSVZ3C33GRO5CCY6ITXC54BBANCNFSM6AAAAAAS7WSCWA>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
|
I am confused by the history on this PR:
Is this PR final or should it have been marked as DRAFT? |
HamzaKh01
force-pushed
the
master
branch
2 times, most recently
from
35e0983 to
ae905fb
Compare
Surely all your concerns will not arise because we are not supporting the Smepmp switch at the moment now. The switch implementation is taking too long and this PR seems to be stalled despite being functionally correct. The way it will work now is, if pmp is enabled and mseccfg(CSR of Smepmp extension) is used then PMP permissions will behave as ePMP. |
For your context this PR was originally prepared to add just support for Smepmp extension. Later I was asked to modify the implementation to support as if it is controlled by the command line switch and I was just using API of that switch and compiling with true and false values to check my implementation not passing any value from command line and I was suppose to get this implementation of switch. That is why I said it is temporary thing because I have to define the variable to some value (True or False) otherwise build will fail.
I have addressed that in an above comment.
Yes, it is final. The reason why I have taken back switch implementation from this is here . Can you please review it or ask someone, if any feedback comes I will fix appropriately. |
|
@billmcspadden-riscv are you merging this PR in today's meeting? If no, then what deliverables are still required from our side. By looking at the latest comments of @HamzaKh01, this PR has no dependencies with switch implementation so it can be merged right away. |
I have replied to each comment separately and I believe pmpCheckPerms is correctly implemented for MML. I have noted your suggestions for adding comments in new line and adding some comments in code. Waiting for any other feedback from others will push the feedback fixes once review settles. |
Yes, you are right, but currently we only have 16 pmpcfg entries defined in the model. So, I am not hard-coding this to 16. Model has only the capability of adding up to 16 regions. If regions are increased up to 64 later only then this check can check 64 entries lock. I have still not understood your comment about how i avoid hard-coding up to 16 regions. The only solution which exists is to add support for up to 64 regions by increasing pmpcfg entries from 16 to 64 in the model as far as I know. |
|
This is a case where we need to add a command line (or YAML) parameter that indicates whether the DUT has 0, 16, or 64 PMP entries. This is going to permeate the existing PMP code, so it should be done as a separate PR |
|
Yes, agreed. |
billmcspadden-riscv
removed
the
tgmm-agenda
|
I've added the command line support for Smepmp. You can find my code on the The command line switch is: --enable-Smepmp I would suggest that you merge my code onto your branch and make |
|
@HamzaKh01 |
| 0x747 => p == Machine, // mseccfg | ||
| 0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh | ||
|
|
There was a problem hiding this comment.
We recently used this code and needed to make the following change so that mseccfg does not exist when PMP is disabled:
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index c3ac1fe..e5a8cf7 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -50,8 +50,8 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x3D @ idx : bits(4) => p == Machine & sys_pmp_max_count() > unsigned(0b10 @ idx),
0x3E @ idx : bits(4) => p == Machine & sys_pmp_max_count() > unsigned(0b11 @ idx),
- 0x747 => p == Machine, // mseccfg
- 0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh
+ 0x747 => p == Machine & sys_pmp_count() > 0, // mseccfg
+ 0x757 => p == Machine & (sizeof(xlen) == 32) & sys_pmp_count() > 0, // mseccfgh
0xB00 => p == Machine, // mcycle
0xB02 => p == Machine, // minstret
There was a problem hiding this comment.
I don't think that is strictly correct. You can have mseccfg without PMPs. Really we need a sys_has_mseccfg() flag or something like that, because it is optional. (As far as I remember anyway.)
There was a problem hiding this comment.
I think you're right. Either way this code needs to be altered before we can merge.
There was a problem hiding this comment.
For this file, we needed the following change:
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 7cca3ba..ce3b1b0 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -139,6 +139,8 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType =
function pmpCheck forall 'n, 'n > 0. (addr: int, width: int('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
+ if sys_pmp_count() == 0 then return None();
+
foreach (i from 0 to 3) {
let prev_pmpaddr = (if i > 0 then pmpReadAddrReg(i - 1) else zeros());
match pmpMatchEntry(addr, width, acc, priv, pmpcfg_n[i], pmpReadAddrReg(i), prev_pmpaddr) {There was a problem hiding this comment.
Hmm I think this is handled in phys_access_check() but maybe it makes more sense here.
There was a problem hiding this comment.
Ah, then I should probably be using that function in my work as well. Thanks! This can thus be marked as resolved with relation to this PR.
|
Perhaps we can discuss further in #601 |
Description
This PR includes the support of ePMP in sail risc-v. Model is verified by running the tests of ePMP (can be found here ) on the RiscOf environment which runs the tests on spike and sail and compare their signatures. So, it can be said that, this Sail model has a same behaviour for ePMP as of spike. Kindly review this PR. In addition the testplan for writting the tests is attached here