search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
429 stars 158 forks source link

Commandline options or parsing yaml #148

Open allenjbaum opened 2 years ago

allenjbaum commented 2 years ago

Feature request: There are many architectural options in RISC-V. Many of them cannot be derived from examining processor state (including CSRs and eventually config ), but must be tested ( try something, see what answer you get). Entering them as individual command line options is unwieldiy, considering their number.
A better option is to have Sail read and parse the risc-config format YAML file to assign variable values used to configure the csim, . Spike already has this option, though from a device-tree formatted file. Another approach is to write a program that reads the YAML and produces the command line option string. This may b a better option because we would then have access to open source YAML parsers, and we can then more easily examine the options produced.

This approach has been used to create the Sail code that reads and writes CSRs (as opposed to producing commandline strings) (ref PR#128), This is being reconsidered to instead provide the parameters to a Sail CSR access function instead, which could . This could easily be extended to cover other variables, e.g. PM granularity, the number of PMP entries supported, unaligned access support, partial unaligned store support, trap cause priorities, and many, many others.

abukharmeh commented 2 years ago

Or maybe we can make CSIM read the YAML files and extern the needed values directly to SAIL instead of passing them as command line args ?! I

jrtc27 commented 2 years ago

That's what the first option says

abukharmeh commented 2 years ago

Sail read and parse, I proposed to make the C simulator read the YAML file instead of SAIL code.

jrtc27 commented 2 years ago

Nobody's suggesting you write the parser in Sail, as a language it'd be terrible for writing that kind of code. The C parts of the C emulator are still part of the overall Sail compiled model, so it'd be just like how we use the soft-float C library rather than write that in Sail. The wording could perhaps have been clearer but I can guarantee that Allen did not mean what you think he did.

abukharmeh commented 2 years ago

This made me think that Allen meant to say that the actual SAIL code parses YAML in his first option : Another approach is to write a program that reads the YAML and produces the command line option string. This may b a better option because we would then have access to open source YAML parsers. Otherwise he would not have emphasised on it in the second option ?

Anyways, if that's the first option, then I vote for that !

allenjbaum commented 2 years ago

I actually hadn't considered inserting the parser into the csim, to be frank, as opposed to a separate program that would generate the command line arguments that would be compiled in as constant values. (as opposed to trying to write in Sail, which sounds...hard). So, writing it in Sail may have been the first thing I mentioned, but it certainly wasn't my first preference. I think a separate program offers several advantages - you can easily see the commandline arguments that Sail will use to generate the Csim, it will be easier to debug, and the Csim is likely to run faster and be smaller because the options will be compile time constants instead of runtime variables. I see no downside to that approach.

I'm hoping that Sail is at least flexible enough to handle parsing the description of CSR WARL field mapping (after pre-parsing using this approach)

martinberger commented 2 years ago

I agree that Sail should not parse YAML.

Isn't the natural approach to have a top-level script that parses YAML and then configures and executes the building of the C simulator from Sail (this might require linking in additional libraries, when compiling the generated C, where required)?

abukharmeh commented 2 years ago

I think that the cleanest solution would be CSIM parses YAML file, and expose some sort of structure to the compiled Sail code.

Having a top level script that parses YAML and does something with it is not far from what #128 does AFAIK, though there it appears to generate SAIL code for the configuration (I think it could be argued that this is less deterministic).

I am not sure about passing configuration as command line argument, because that would expose an external interface that could/would be changed and people will cling to, the model at the moment initalise all global variables before parsing command line arguments, and that means we could not use cmd line args to pass all options without changing the way the model is initalised, and also I am not sure how far we can extend command line args until it becomes too much.

martinberger commented 2 years ago

I wonder if one could not also argue that the Golden Model code is not, and should not be, concerned with implementation details of testing (such as: how to configure the extensions of interest?), as long as the model does not prevent any specific configuration. The purpose of the model is to express, as clearly and simply as possible, the ISA semantics of RISC-V.

As RISC-V becomes more popular we will get more and more requests to augment the Golden Model with this / that / the-other feature, which will all be jolly useful to somebody, but at the same time compromise the simplicity, readability and verifiability of the model. In particular, I expect to see requests for tracing all manner of model internal state during execution, so as to make it easier to compare the state of the Golden Model execution in a step-wise manner with RTL implementations. I expect the Golden Model to evolve over time, to accommodate such requests, but I think a systematic approach is required, and needs some thought. In the mean time, maybe we should be conservative and try and augment the model from the 'outside'.

allenjbaum commented 2 years ago

The way that the csim is currently configured is to pass command-line arguments to Sail, and Sail compiles the csim appropriately. I am suggesting that we don't change that. What we are changing is how our framework gets the configuration and formats it so that it can be passed on the command line. That separation seems to me to be cleaner, and more easily debugged, than embedding it. We could, of course, change that and embed it inside the Sail csim - but what would the advantage of that be?

I'm also suggesting that #128 https://github.com/riscv/sail-riscv/pull/128 does same thing (if that is doable; I think it is more problematic than other architectural options simply because WARL is not architecturally constrained) The other problem we have is that some behaviors are non-deterministic, but that isn't solvable no matter how perform configuration (e.g. the poster child of them: misaligned accesses, which can trap or be performed, depending on non-ISA microarchitectural state that Sail can't know about)

On Thu, Feb 3, 2022 at 3:20 AM Martin Berger @.***> wrote:

I wonder if one could not also argue that the Golden Model code is not, and should not be, concerned with implementation details of testing (such as: how to configure the extensions of interest?), as long as the model does not prevent any specific configuration. The purpose of the model is to express, as clearly and simply as possible, the ISA semantics of RISC-V.

As RISC-V becomes more popular we will get more and more requests to augment the Golden Model with this / that / the-other feature, which will all be jolly useful to somebody, but at the same time compromise the simplicity, readability and verifiability of the model. In particular, I expect to see requests for tracing all manner of model internal state during execution, so as to make it easier to compare the state of the Golden Model execution in a step-wise manner with RTL implementations. I expect the Golden Model to evolve over time, to accommodate such requests, but I think a systematic approach is required, and needs some thought. In the mean time, maybe we should be conservative and try and augment the model from the 'outside'.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/148#issuecomment-1028882870, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJQRHJOXG5M6VLDAHQTUZJQHLANCNFSM5NMZAUOQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you authored the thread.Message ID: @.***>

abukharmeh commented 2 years ago 
We could, of course, change that and embed it inside the Sail csim - but
what would the advantage of that be?

I don't have a strong preference on either option, but I am not sure how scalable its to pass all options we want to configure the model with via cmd line args, you know much better than me the extent we like to configure the model with and all possible options. At the moment the model is barely configurable, and most options we have are switched on and fixed on by default. I just thought its neater to parse and pass data directly to the compiled Sail code. 

The way that the csim is currently configured is to pass command-line
arguments to Sail, and Sail compiles the csim appropriately.

image

Maybe I misunderstood you, but at the moment as far as I know, Sail compiler compile the Sail code into C/ Ocaml code that contains both options and then the c simulator switch a flag to either enable this or that configuration, this happens in runtime as shown in this picture. Some options like XLEN get configured at compile time, but that's the Makefile selecting the correct files for a given configuration.

allenjbaum commented 2 years ago

The difference is if the flag is a constant that is in the csim c-code, or a variable that is evaluated after the csim model is built and compiled. In the former case, the csim will be run through the compiler, and the option not selected will be eliminated completely. In the latter case, it is evaluated after csim is compiled, so both options are present and it has to read the value and branch to correct code. In effect, one has a custom simulator targeted to a specific implementation, vs. a generic one that has to continually test and select the code that it runs.

This is pretty easy for options that have two, or perhaps 3 possibilities, e.g. C-ext is either implemented (all C-extension code is present and unconditional), or is not implemented (all C-extension code is removed), or is implemented but can be disabled (all C-extension code is present, but can't be used if misa.c==0)

That depends on when the YAML parsing occurs; If it is called from the csim itself, it's runtime. If it's parsed ahead of time then the result of the parsing is passed as command line options that set constant values, and the compiler takes it from there.

On Thu, Feb 3, 2022 at 10:54 AM Ibrahim Abu Kharmeh < @.***> wrote:

We could, of course, change that and embed it inside the Sail csim - but what would the advantage of that be?

I don't have a strong preference on either options, but I am not sure how scalable its to pass all options we want to configure the model with via cmd line args, you know much better than me the extent we like to configure the model with and all possible options. At the moment the model is barley configurable, and most options we have are switched on and fixed on by default. I just thought its neater to parse and pass data directly to the compiled Sail code.

The way that the csim is currently configured is to pass command-line arguments to Sail, and Sail compiles the csim appropriately.

[image: image] https://user-images.githubusercontent.com/24764074/152409458-c36f1b7f-2111-4e74-9db2-a778cddd58d5.png

Maybe I misunderstood you, but at the moment as far as I know, Sail compiler compile the Sail code into C/ Ocaml code that contains both options and then the c simulator switch a flag to either enable this or that configuration, this happens in runtime as shown in this picture. Some options like XLEN get configured at compile time, but that's the Makefile selecting the correct files for a given configuration.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/148#issuecomment-1029299312, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJXALS47AVEVJUGQP5TUZLFPPANCNFSM5NMZAUOQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you authored the thread.Message ID: @.***>

abukharmeh commented 2 years ago

a variable that is evaluated after the csim model is built and compiled. Yes, this is what I meant to say, all of the options we currently have are evaluated at runtime of the simulator, and not fixed before dead code elimination when they are inputted to the C/ OCAML compiler. image

allenjbaum commented 2 years ago

OK, I learned something new, that the options are input to csim, not an input to Sail that builds the csim. That means there is only one version of csim - which is golden, and not multiple versions depending on options. That's both good and bad. It also makes the arguments against generating specific per/implementation Sail code for CSR WARL field access stronger.

It doesn't really change whether the c-code that parses YAML and sets specific variables should be directly called by the csim, or a separate program that generates command line options. I still think the separate program has more flexibility and observability.

That's a minor issue compared to the complexity of WARL fields, though.

On Fri, Feb 4, 2022 at 2:18 AM Ibrahim Abu Kharmeh @.***> wrote:

a variable that is evaluated after the csim model is built and compiled. Yes, this is what I meant to say, all of the options we currently have are evaluated at runtime of the simulator, and not fixed before dead code elimination when they are inputted to the C/ OCAML compiler. [image: image] https://user-images.githubusercontent.com/24764074/152511047-dd043486-c462-465c-9e6a-4f4a1ab74d62.png

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/148#issuecomment-1029835214, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJSN6KB6H24U5LLMJITUZORW3ANCNFSM5NMZAUOQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you authored the thread.Message ID: @.***>

allenjbaum commented 2 years ago

I'm replicating this comment from PR#128: (because I'm an incompetent GIT user - I'm sure there's a better way) There are currently 3 proposals on the table for handling Sail configuration via the riscv-config YAML file:

Note that all 3 proposals do the bulk of their parsing in a separate bit of (non-sail) code; the primary difference is whether individual Sail functions per CSR are generated, individual Sail types per CSR are generated, or text strings per CSR are generated.

One unknown to me is whether making changes enabling a single csim will affect other uses of the formal model; that is, does the "data dependency" of using a string (or any other basic data type) to legalize CSR writes mean that theorem proving becomes impossible? Does it affect the OCaml model?

martinberger commented 2 years ago

> does the "data dependency" of using a string (or any other basic data type) to legalize CSR ...

String is a bad data-type for communicating information in Sail because you get little support from the type checker. Using parameterised sum types like enumerations / unions is much better because the type checker can do e.g. exhaustiveness checks. Using sum types is perfectly compatible with theorem proving (a sum types is closely related to logical disjunction).

martinberger commented 2 years ago

> Spike already has this option, though from a device-tree formatted file.

If Spike already does this, maybe the Sail model should do the same, for uniformity?

martinberger commented 2 years ago

> * c.3 + no new types are needed,

There is no problem with defining new types. On the contrary, if we could use types to constrain the handling architectural options, that would be helpful because the type-checker might aid us in bug-prevention.

allenjbaum commented 2 years ago

I had guessed that a string is a bad data type for this, which is why I pointed it out. I'd really like to be able to pass types rather than a string; I just don't know how to do that, or what it means to do that.

If we have a type struct which is a list that contains a list as one of its members - how to we get that into the csim from the command line? The command line argument is a string, so some level of parsing is needed to turn it into a type - but you're still starting with a string, which is where I was coming from.

It's either my ignorance or just the point of view I'm using. Both probably. But if we can do what you are saying, I'd be really pleased.

My main point was that we don't literally need to have an enormous string of command line options, as opposed to pointer to a file that has an enormous string of command line options; that was probably a bit too obvious.

Spike has a somewhat limited capacity for configuration compared to what we think is necessary. I don't have an opinion whether we should br using DT format or riscv-config format, but we probably need a conversion tool. Not that typically, the device tree is built by boot code that (among other things) will look at the config-struct, and we do want to be compatible with that (at least by having a conversion tool).

martinberger commented 2 years ago

@allenjbaum We do not need enormous string of command line options. We can ask the C simulator to take an additional command line argument, which might take a file name as argument. IIRC this requires changing [1]. The file given as argument needs parsing and the information in the file needs to be converted into a form that the C, which is compiled from Sail, can handle.

Parsing, conversion etc is not a difficult problem. The most interesting problem is how best to represent the configurations in Sail, ideally in a typed manner, and localised manner. @PeterSewell made some suggestions previously about this. How much Sail needs to to be hard-coded for special cases remains to be seen.

Maybe a next step could be to look at and list all existing legalisation function and see how the can be most naturally expressed in Sail?

[1] https://github.com/rems-project/sail/blob/sail2/lib/rts.c#L604

allenjbaum commented 2 years ago

That's exactly what I had in mind; I guess I'm not explaining myself well. The legalization functions are easy; delimiting the size and position of the implementation defined subfields are what I think of as the difficult part.

Mapping that to the type that we need (if the type system is as flexible as we need, as opposed to multiple types) is the part I'm unclear about. I proposed mapping all of the struct elements to fixed sized integers or lists of bitstrings because otherwise we'd have hundreds or even thousands of types, and we'd have to dynamically choose them. I wasn't under the impression that we could define new types at run time, as opposed to filling the value of an existing type at run time. Specifically something like: { [boolean COND], int6 FLD_HI,[int6 FLD_LO], {bitfield64 VAL_HI,[bitfield64 VAL_LO] }, enum MAPFUNC}. where (I'm making this syntax up) { } surrounds a list of arbitrary size, [ ] surrounds an optional subfield, int6 is a 6bit integer, bitfield64 is a 64bit bitfield. (use int5 and bitfield32 for RV32) will work for every CSR I can think of offhand (one of the MAPFUNC enums is MSKVAL where VAL_HI is the mask and VAL_LO is the background value) We can generate 4 or 8 separate types if optional subfields aren't allowed (*2 for RV32 vs RV64)

On Mon, Feb 21, 2022 at 11:52 AM Martin Berger @.***> wrote:

@allenjbaum https://github.com/allenjbaum We do not need enormous string of command line options. We can ask the C simulator to take an additional command line argument, which might take a file name as argument. IIRC this requires changing [1]. The file given as argument needs parsing and the information in the file needs to be converted into a form that the C, which is compiled from Sail, can handle.

I think parsing, conversion etc is not a difficult problem. The most interesting problem is how best to represent the configurations in Sail, ideally in a typed manner. @PeterSewell https://github.com/PeterSewell made some suggestions previously.

[1] https://github.com/rems-project/sail/blob/sail2/lib/rts.c#L604

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/148#issuecomment-1047185149, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJUXGADAXGYP7WAPT5TU4KJWPANCNFSM5NMZAUOQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>

martinberger commented 2 years ago

Luckily Sail can define option types [1] and they are widely used in the RISCV model [2]. It looks like the type you are sketching is a list of 4-tuples, like so:

list( ( option(bool), int6, option(int6), T, mapfunc ) )

where the second to last component is a list of 2-tuples, like so:

type T = list( ( bitfield64, option( bitfield64 ) ) )

I'm not totally sure what the type mapfunc is going to be. Did I get this roughly right?

> opposed to multiple types

It might be advantageous for better type-checking the we do use multiple types, and let dependent types disambiguate btween them.

[1] https://github.com/rems-project/sail/blob/sail2/lib/option.sail#L76-L79

[2] https://github.com/riscv/sail-riscv/blob/master/model/prelude.sail#L72

martinberger commented 2 years ago

> define new types at run time

We cannot define Sail types at (Sail or C) run-time.

allenjbaum commented 2 years ago

That is what I thought, and makes perfect sense.. What you describe above is what I was thinking of, except I think we can't deal with the condition field as part of this type. The condition bool is a little tricky; in theory, it's a function of any implementation defined architectural state, but a) I don't think it's possible to express that in Sail, and b) in reality it is a function of architecturally defined architectural state. So, the CSR_WRITE function must be passed the name of the CSR, a predefined list of booleans, and the typed variable: list( ( int6, option(int6), T , enum )

I need to think about how we apply the booleans to the list elements. It's not a very common case, and it's possible it would be a 1:1 map, but, because of WARL, we have to pre-define the number of booleans, but can't predefine the number of list elements of the type (an implementation might split an WARL field across multiple list elements (e.g. a CSR containing addresses could be split into

There would be two different types: , one for RV64, and one for RV32. So the remaining part is exactly the format of the commandline argument that the csim will be presented with, which needs a CSR nsme, and the assignment. There would be separate list elements for each subfield for a CSR (delimited by the 2 or 1 int6s), and then the legal values for that subfield (a list of ranges or explicit values, or treating it like mask/value pair, depending on the enum

The code for this should be pretty simple, just applying a standard function to each named CSR for each list element, and for each T-subelement for that element. The pre-parser would sort and validate the list elements (ensuring that field definitions can't overlap, for example) to produce these types from the YAML.

On Mon, Feb 21, 2022 at 2:46 PM Martin Berger @.***> wrote:

> define new types at run time

We cannot define Sail types at (Sail or C) run-time.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/148#issuecomment-1047277348, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJUYHHPXS3NAK5W63MLU4K6DDANCNFSM5NMZAUOQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>

PeterSewell commented 2 years ago

On Mon, 21 Feb 2022 at 22:46, Martin Berger @.***> wrote:

define new types at run time

We cannot define Sail types at (Sail or C) run-time.

And nor, as far as I can see, do we have any need to. Let's look back again at Robert Norton-Wright's earlier version (I'm sure that would need to be extended or adapted, but one should start from that and a clear understanding of what more is needed, rather than trying to start from scratch). First, he defines some fixed types for the configuration parameters of that version of the model, in:

https://github.com/riscv/sail-riscv/blob/rv_config/config/riscv_config2sail/sail/riscv_config_types.sail

e.g. struct WARL_bitmask = { mask : nat, / XXX consider using bits('n) / default_val : nat }

struct isa_config = { I : bool, / The base integer ISA (always true because E is not implemented yet) / M : bool, / mul / div/ F : bool, / floating point / A : bool, / atomic memory / D : bool, / double floating point / C : bool, / compressed instructions / S : bool, / supervisor mode / U : bool, / user mode / Zicsr : bool, / control and status registers / Zifencei : bool / instruction fetch fence / }

struct riscv_isa_config = { ISA : isa_config, hw_data_misaligned_support : bool, xlen : nat, / XXX 32, 64, 128 / misa : misa_config, mvendorid : id_reg_config,

Second, he has a standalone OCaml program to read YAML and produce a Sail file defining several top-level configuration values such as isa_config, of those types.

Third, the model uses those values in various places, e.g.

https://github.com/riscv/sail-riscv/blob/rv_config/model/riscv_sys_regs.sail#L176 function legalize_misa(m : Misa, v : xlenbits) -> Misa = { if sys_enable_writable_misa () then { l = [v with 25..0 = legalize_warl_bitmask(v[25..0], isa_config.misa.Extensions)];

using a fixed legalize_warl_bitmask function that takes the relevant config value to tell it how to legalize this field. These legalize functions are in:

https://github.com/riscv/sail-riscv/blob/rv_config/model/riscv_sys_regs.sail#L88 e.g. / THIS(current_val, written_val, legal_range) legalizes a WARL field according to given legal_range of values and legalising mode. / val legalize_warl_range : forall 'n, 'n > 0 . (bits('n), bits('n), WARL_range) -> bits('n) effect {escape} function legalize_warl_range(current_val, written_val, legal_range) = { if (is_value_in_range(unsigned(written_val), legal_range.rangelist)) then written_val else match(legal_range.mode) { WARL_Unchanged => current_val, WARL_Largest => to_bits('n, WARL_range_max(legal_range.rangelist)), WARL_Smallest => to_bits('n, WARL_range_min(legal_range.rangelist)),

So what would have to change? AFAICS (though I say this without being familiar with what's in the later versions of the YAML):

Peter

— Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you were mentioned.Message ID: @.***>

allenjbaum commented 2 years ago

What is in the newer version is that the legalization function is not fixed, and the format of WARL fields are not fixed; they can be broken up into an arbitrary number of subfields which each have separate legalization requirements - and those legalization requirements can also be an arbitrary number of ranges (or individual values).

So (and this is just me speaking, and I am very, very far from being competent in Sail) the legalization function (that I've proposed) takes a descriptor type (a list of 4-tuple rules, one of which is a list of 2-tuples) and applies it to each WARL field (at least, each that is larger than a bit or is conditional). Each list element is the MSB:LSB position of the field - or subfield, a list of value ranges , and an enum that chooses the legalization function

A CSR like MTVEC is architecturally 2 separate WARL fields, but it would be completely reasonable to expect that the larger WARL field is built up of 1,2, or 3 subfields, each with their own legality, and each of those can have implementation defined boundaries. So MTVEC_MODE(mtvec.mode, write_val, legal_range) becomes MTVEC_MODE(mtvec.mode, write_val.mode, THIS_WARL_DESCRIPTOR) where the descriptor is one of the 4 tuples corresponding to that field. The legalization function iterates through the ranges until it either

My proposal doesn't even bother splitting the CSR into separate fields If you have the subfields MSB:LSB, you may as well just apply all them to the entire register, and each will only affect the corresponding subfield defined by its MSB:LSB. Non-WARL fields are defined by an overall mask and value (where mask applies to RW bits, and value applies to RO and WARL fields), and the WARL_DESCRIPTOR is the list of 4-tuples, each of which is applied sequentially as above.

I'm not sure I understand "- one would prefer the functions of the model to be explicitly rather than implicitly parameterised on the config value, but I think that's what we want to do also

I am not sure what you're thinking of when you say

For the conditional cases: we are only going to support architecturally defined conditions, not implementation defined conditions, so we aren't deciding on the state, the spec will. It is permissable for an implementation to decide use arbitrary architectural state, but I can't expect Sail to support that.

I think we have to re-define the 4-tuple in the config struct to be a 5-tuple with a condition as the [optional] added parameter (If the parameter doesn't exist, it defaults to true.) A CSR that has two formats depending on the value of some specific state (or combination of state) would have two sets of rules, one with the condition and the other with its inverse (or, if there are cases with more than two, then 3 rules, and only one of them has a condition evaluating to true) I'm just not sure now to do the mapping of condition to a specific CSR in the code in a clean way, but it would be fixed, at least.

On Mon, Feb 21, 2022 at 11:34 PM Peter Sewell @.***> wrote:

On Mon, 21 Feb 2022 at 22:46, Martin Berger @.***> wrote:

define new types at run time

We cannot define Sail types at (Sail or C) run-time.

And nor, as far as I can see, do we have any need to. Let's look back again at Robert Norton-Wright's earlier version (I'm sure that would need to be extended or adapted, but one should start from that and a clear understanding of what more is needed, rather than trying to start from scratch). First, he defines some fixed types for the configuration parameters of that version of the model, in:

https://github.com/riscv/sail-riscv/blob/rv_config/config/riscv_config2sail/sail/riscv_config_types.sail

e.g. struct WARL_bitmask = { mask : nat, / XXX consider using bits('n) / default_val : nat }

struct isa_config = { I : bool, / The base integer ISA (always true because E is not implemented yet) / M : bool, / mul / div/ F : bool, / floating point / A : bool, / atomic memory / D : bool, / double floating point / C : bool, / compressed instructions / S : bool, / supervisor mode / U : bool, / user mode / Zicsr : bool, / control and status registers / Zifencei : bool / instruction fetch fence / }

struct riscv_isa_config = { ISA : isa_config, hw_data_misaligned_support : bool, xlen : nat, / XXX 32, 64, 128 / misa : misa_config, mvendorid : id_reg_config,

Second, he has a standalone OCaml program to read YAML and produce a Sail file defining several top-level configuration values such as isa_config, of those types.

Third, the model uses those values in various places, e.g.

https://github.com/riscv/sail-riscv/blob/rv_config/model/riscv_sys_regs.sail#L176 function legalize_misa(m : Misa, v : xlenbits) -> Misa = { if sys_enable_writable_misa () then { l = [v with 25..0 = legalize_warl_bitmask(v[25..0], isa_config.misa.Extensions)];

using a fixed legalize_warl_bitmask function that takes the relevant config value to tell it how to legalize this field. These legalize functions are in:

https://github.com/riscv/sail-riscv/blob/rv_config/model/riscv_sys_regs.sail#L88 e.g. / THIS(current_val, written_val, legal_range) legalizes a WARL field according to given legal_range of values and legalising mode. / val legalize_warl_range : forall 'n, 'n > 0 . (bits('n), bits('n), WARL_range) -> bits('n) effect {escape} function legalize_warl_range(current_val, written_val, legal_range) = { if (is_value_in_range(unsigned(written_val), legal_range.rangelist)) then written_val else match(legal_range.mode) { WARL_Unchanged => current_val, WARL_Largest => to_bits('n, WARL_range_max(legal_range.rangelist)), WARL_Smallest => to_bits('n, WARL_range_min(legal_range.rangelist)),

So what would have to change? AFAICS (though I say this without being familiar with what's in the later versions of the YAML):

  • one would prefer the functions of the model to be explicitly rather than implicitly parameterised on the config value, passing down a single parameter (of a top-level struct type containing all the config) rather than referring to global identifiers. That gives us a single executable and also a single mathematical model for any proof
  • one would like the config value to be constructed at runtime, by the C or OCaml interpreter, by parsing some YAML (or whatever)
  • the Sail type and the structure of the YAML file should (and should be required to) exactly correspond for each version of the model
  • the parsing can be pretty much generic in that structure
  • the details of the allowed shapes of config values probably need to be generalised in some way (I don't know what), adding more cases to the Sail types describing them (e.g. WARL_bitmask above)
  • in the cases where legalisation depends on other system state, you need to decide what state, and pass that into the uses of the relevant legalisation functions

Peter

— Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you were mentioned.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/148#issuecomment-1047503674, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJSQ4WL6CPR43DOPKVTU4M377ANCNFSM5NMZAUOQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>