Question: how to make implementation-defined behaviour customisable

[Timmmm]

In the RISC-V spec there are many places where there's a choice about how to behave. In this model there are already a few flags that encode those choices in riscv_platform.sail, e.g. plat_mtval_has_illegal_inst_bits or plat_enable_dirty_update.

However as far as I can see all of the existing options are essentially booleans. That works when the spec says "implementations must always do either A or B", but there are plenty of places where it says "the behaviour is implementation defined", or "implementations can do A or B depending on X". Stuff that can't be encoded with a boolean.

I couldn't find anywhere in the current model that handles those things. I was thinking the obvious solution is to move the customisable functionality into its own function and put that function in its own file. That way if people want to change it they just write a new version of the function in another file and then edit the Makefile. Kind of like the ..._ext.sail files.

Does that seem reasonable? Do you have a plan for this?

[billmcspadden-riscv]

Hi Tim. Good question, and one that is being worked on. As you pointed out, the current method for configuring the model with command line switches is limited. Another option would be to use the RISCV-Config structures (YAML files) that are used by the ACTs for configuration. Please see #175 for my proposal as to how this could be done for runtime configuration. I think we'd like to avoid compile-time configuration, if possible. The complexities of building the Sail model has been an issue with the Sail model for many of our customers; I don't think we want to go that route. But it is an option. Bill Mc.

…

On Tue, Jun 27, 2023 at 3:51 AM Tim Hutt ***@***.***> wrote: In the RISC-V spec there are many places where there's a choice about how to behave. In this model there are already a few flags that encode those choices in riscv_platform.sail, e.g. plat_mtval_has_illegal_inst_bits or plat_enable_dirty_update. However as far as I can see all of the existing options are essentially booleans. That works when the spec says "implementations must always do either A or B", but there are plenty of places where it says "the behaviour is implementation defined", or "implementations can do A or B depending on X". Stuff that can't be encoded with a boolean. I couldn't find anywhere in the current model that handles those things. I was thinking the obvious solution is to move the customisable functionality into its own function and put that function in its own file. That way if people want to change it they just write a new version of the function in another file and then edit the Makefile. Kind of like the ..._ext.sail files. Does that seem reasonable? Do you have a plan for this? — Reply to this email directly, view it on GitHub <#278>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLODFU643NSBKKODYMUDXNKNJHANCNFSM6AAAAAAZVIRX3Q> . 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

[Timmmm]

I agree, building the Sail model is quite a pain due to the use of OCaml (we ended up storing the generated C in Git so only people editing the model need OCaml & Sail). But I don't see how you can avoid compile-time configuration in some cases because the range of possible behaviours is too large.

For example for WARL CSRs the spec says:

Implementations can return any legal value on the read of a WARL field when the last write was of an illegal value, but the legal value returned should deterministically depend on the illegal written value and the architectural state of the hart.

A runtime option can't cover all the possible implementations here. In cases like these would you say the approach of putting the implementation function (e.g. legalize_somecsr()) in its own file would be the least bad option?

I guess an alternative is to give up on trying to cover all the possible implementations, and just have a set of predefined implementations, and maybe add more if people implement behaviours that aren't on the list?

I'm mainly asking so we can keep our modifications as upstreamable as possible.

[billmcspadden-riscv]

WARL CSRs are indeed a pain. And I've been using them as the pathological (ie - most difficult) case for configuration development. I think there are solutions to the problem. Seeing that you've been working on this problem, it might be good for us to chat and share ideas. I'd like to hear more about what you're doing. I'll start a new email thread (one not attached to this PR) to discuss a possible meeting. Bill Mc.

…

On Tue, Jun 27, 2023 at 7:06 AM Tim Hutt ***@***.***> wrote: I agree, building the Sail model is quite a pain due to the use of OCaml (we ended up storing the generated C in Git so only people editing the model need OCaml & Sail). But I don't see how you can avoid compile-time configuration in some cases because the range of possible behaviours is too large. For example for WARL CSRs the spec says: Implementations can return any legal value on the read of a WARL field when the last write was of an illegal value, but the legal value returned should deterministically depend on the illegal written value and the architectural state of the hart. A runtime option can't cover all the possible implementations here. In cases like these would you say the approach of putting the implementation function (e.g. legalize_somecsr()) in its own file would be the least bad option? I guess an alternative is to give up on trying to cover *all* the possible implementations, and just have a set of predefined implementations, and maybe add more if people implement behaviours that aren't on the list? I'm mainly asking so we can keep our modifications as upstreamable as possible. — Reply to this email directly, view it on GitHub <#278 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOGRFSKLEFKUXNZIBPDXNLEEFANCNFSM6AAAAAAZVIRX3Q> . You are receiving this because you commented.Message ID: ***@***.***>

-- Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309

[PeterSewell]

On Tue, 27 Jun 2023 at 13:06, Tim Hutt ***@***.***> wrote: I agree, building the Sail model is quite a pain due to the use of OCaml (we ended up storing the generated C in Git so only people editing the model need OCaml & Sail). But I don't see how you can avoid compile-time configuration in some cases because the range of possible behaviours is too large. For example for WARL CSRs the spec says: Implementations can return any legal value on the read of a WARL field when the last write was of an illegal value, but the legal value returned should deterministically depend on the illegal written value and the architectural state of the hart. A runtime option can't cover all the possible implementations here. In cases like these would you say the approach of putting the implementation function (e.g. legalize_somecsr()) in its own file would be the least bad option? I guess an alternative is to give up on trying to cover *all* the possible implementations, and just have a set of predefined implementations, and maybe add more if people implement behaviours that aren't on the list?

y - I don't have any sense of the range of behaviour implementations are actually using, but I'd hope that the above would in practice converge pretty quickly. I don't know why the prose spec is this loose, but naively it seems excessively so - as a matter of taste and testability, and because it would make it hard for s/w to reason about information flow, and, more particularly, because the prose lets the return value depend on the architectural state at a higher privilege level. Perhaps there is now enough experience with what's used in practice that it could be tightened up? p Though really, the spec seems excessively loose

…

I'm mainly asking so we can keep our modifications as upstreamable as possible. — Reply to this email directly, view it on GitHub <#278 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZXIJMNTDHLZQY2JYALXNLEEHANCNFSM6AAAAAAZVIRX3Q> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>