Add configuration option for reserved mtvec[MODE] values - #1533
Merged
Merged
Conversation
Tim Hutt (Timmmm)
left a comment
Tim Hutt (Timmmm)
left a comment
Collaborator
There was a problem hiding this comment.
Probably should be Xtvec everywhere since it also applies to stvec?
Otherwise LGTM.
| TV_Direct => v, | ||
| TV_Vector => v, | ||
| _ => match mtvec_mode_reserved_behavior { | ||
| Mtvec_Fatal => reserved_behavior("Tried to write a reserved value to the MODE field of mtvec."), |
Collaborator
There was a problem hiding this comment.
Probably could add the value that was written?
|
|
||
| mapping MtvecModeReservedBehavior_str : MtvecModeReservedBehavior <-> string = { | ||
| Mtvec_Fatal <-> "Mtvec_Fatal", | ||
| Mtvec_UseOld <-> "Mtvec_UseOld", |
Collaborator
There was a problem hiding this comment.
Maybe Mtvec_Ignore? UseOld sounds a bit weird to me. Very minor though.
Collaborator
There was a problem hiding this comment.
Are these string mappings used anywhere?
| _ => [v with Mode = o[Mode]] | ||
| } | ||
| let v = Mk_Mtvec(v); | ||
| match (trapVectorMode_of_bits(v[Mode])) { |
Collaborator
There was a problem hiding this comment.
Suggested change
| match (trapVectorMode_of_bits(v[Mode])) { | |
| match trapVectorMode_of_bits(v[Mode]) { |
|
|
||
| mapping MtvecModeReservedBehavior_str : MtvecModeReservedBehavior <-> string = { | ||
| Mtvec_Fatal <-> "Mtvec_Fatal", | ||
| Mtvec_UseOld <-> "Mtvec_UseOld", |
Collaborator
There was a problem hiding this comment.
Are these string mappings used anywhere?
Collaborator
|
My Sail semantics is weak at best, but are you defining a specific
illegal->legal mapping for writing an illegal value to mtvec (UseOld)?
IT is a 2 bit fWAL ield , and that isn't the only possibility that an
implementation is allowed (it could keep the old value, ignore only the
write to bit 1, force mallest legal value, or force largest)
…On Fri, Feb 6, 2026 at 9:26 AM Prashanth Mundkur ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In model/core/sys_regs.sail
<#1533 (comment)>:
> @@ -578,12 +578,15 @@ register mtvec : Mtvec // Trap Vector
// PUBLIC: invoked from set_{ms}tvec() [exceptions/sys_exceptions.sail]
function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = {
- let v = Mk_Mtvec(v);
- match (trapVectorMode_of_bits(v[Mode])) {
- TV_Direct => v,
- TV_Vector => v,
- _ => [v with Mode = o[Mode]]
- }
+ let v = Mk_Mtvec(v);
+ match (trapVectorMode_of_bits(v[Mode])) {
⬇️ Suggested change
- match (trapVectorMode_of_bits(v[Mode])) {
+ match trapVectorMode_of_bits(v[Mode]) {
------------------------------
In model/core/platform_config.sail
<#1533 (comment)>:
> @@ -104,6 +104,17 @@ mapping XenvcfgCbieReservedBehavior_str : XenvcfgCbieReservedBehavior <-> string
}
overload to_str = {XenvcfgCbieReservedBehavior_str}
+enum MtvecModeReservedBehavior = {
+ Mtvec_Fatal,
+ Mtvec_UseOld,
+}
+
+mapping MtvecModeReservedBehavior_str : MtvecModeReservedBehavior <-> string = {
+ Mtvec_Fatal <-> "Mtvec_Fatal",
+ Mtvec_UseOld <-> "Mtvec_UseOld",
Are these string mappings used anywhere?
—
Reply to this email directly, view it on GitHub
<#1533 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJRRHCB7OT533UJFI5L4KTFDNAVCNFSM6AAAAACUFIYYZOVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZTONRUGMYTEMBRGY>
.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
Collaborator
|
Yeah it's defining the particular behaviour that the model already had hard-coded. We should probably decide how exactly we want to deal with all the WARL fields before adding more. |
Jiacheng Tong (challenger1024)
force-pushed
the
mtvec
branch
from
February 15, 2026 07:42
880d03f to
abd6314
Compare
Contributor
Author
|
I have changed UseOld to Ignore . |
Tim Hutt (Timmmm)
requested changes
Feb 25, 2026
Tim Hutt (Timmmm)
approved these changes
Feb 28, 2026
Tim Hutt (Timmmm)
left a comment
Tim Hutt (Timmmm)
left a comment
Collaborator
There was a problem hiding this comment.
Nice, thanks!
Tim Hutt (Timmmm)
changed the title
Jordan Carlin (jordancarlin)
approved these changes
Mar 1, 2026
Jordan Carlin (jordancarlin)
added
the
configuration
Tim Hutt (Timmmm)
added
the
will be merged
Prashanth Mundkur (pmundkur)
approved these changes
Mar 1, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Some mtvec[MODE] values are currently reserved. Add an option to configure what happens if a reserved value is written.