Add initial Sail snippets

[Timmmm]

Add Makefile targets to download the Sail JSON bundle from Github releases (it's a few MB so this avoids bloating the repo).

I updated a few scalar crypto functions that already had copy & pasted Sail code to use the model source instead. The result is almost identical.

See #1369.

[Timmmm]

Note, @Alasdair has demonstrated a fancier version of this with syntax highlighting and hyperlinked code (e.g. so you can click on <<< to see what it means), but that isn't used here yet.

Before:

After:

(The Sail code has changed a little since that was copy/pasted.)

[wmat]

Question, do we need to care about the version of the SAIL model we're pulling the index from? I recognize SAIL isn't at v.1.0 yet so perhaps at this point we don't, but in the future should we? Or perhaps we pair a SAIL version with the riscv-isa-manual src when we build a release for publication?

[Timmmm]

There are a couple of aspects to that:

1. We obviously want to point to a fixed version so it is repeatable. We don't want to just always use master. That is covered here by the URL being version tracked in Git. We should maybe include the Git hash of the sail-riscv repo, or maybe the hash of the JSON file just in case (a URL can change or disappear). I don't think that is a blocker though.
2. The spec sometimes changes behaviour - sometimes in backwards incompatible ways - and currently the sail-riscv repo only implements one version. We obviously want the Sail code's behaviour to match the version of the ISA manual it is included in.

For the second point my vague plan was:

1. Finish adding a way to actually specify the spec versions to the Sail model. I made an attempt here but it needs to be reworked.
2. Once that is done, use Alasdair's fancy Sail-rewriting system to generate the code for the "current" spec version. Basically you can take code that is like:

if version == 1.12
   foo
else if version == 1.13
   bar
...

and you say "yeah but I know the version is 1.12", and then it will only insert foo.

I don't think Alasdair has published that yet so I'm not exactly sure what you have to do but it will probably end up with us having separate .json bundles for each version.

However, I also don't think that is a blocker. I would suggest initially we just use it for snippets where the behaviour has never changed and is unlikely to change in future.

[wmat]

Excellent, thanks Tim, I mostly wanted to be sure the versioning question was on the table for discussion. So thanks for confirming to me that it is indeed out there.

[nadime15]

I'm curious what parts of sail are actually supposed to be integrated into the risc-v manual? Are we just talking about the execution function of each instruction?

[Timmmm]

Mostly the execute clauses, but I think there are other bits too where the behaviour would be much clearer with the Sail code, e.g. interrupt handling:

/* Interrupts are prioritized in privilege order, and for each
 * privilege, in the order: external, software, timers.
 */
function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
  let ip = Mk_Minterrupts(ip);
  if      ip[MEI] == 0b1 then Some(I_M_External)
  else if ip[MSI] == 0b1 then Some(I_M_Software)
  else if ip[MTI] == 0b1 then Some(I_M_Timer)
  else if ip[SEI] == 0b1 then Some(I_S_External)
  else if ip[SSI] == 0b1 then Some(I_S_Software)
  else if ip[STI] == 0b1 then Some(I_S_Timer)
  else                        None()
}

/* Given the current privilege level, return the pending set
 * of interrupts for the highest privilege that has any pending.
 *
 * We don't use the lowered views of {xie,xip} here, since the spec
 * allows for example the M_Timer to be delegated to the S-mode.
 */
function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
  // mideleg can only be non-zero if we support Supervisor mode.
  assert(extensionEnabled(Ext_S) | mideleg.bits == zeros());

  let pending_m = mip.bits & mie.bits & ~(mideleg.bits);
  let pending_s = mip.bits & mie.bits & mideleg.bits;

  let mIE = (priv == Machine    & mstatus[MIE] == 0b1) | priv == Supervisor | priv == User;
  let sIE = (priv == Supervisor & mstatus[SIE] == 0b1) | priv == User;

  if      mIE & (pending_m != zeros()) then Some((pending_m, Machine))
  else if sIE & (pending_s != zeros()) then Some((pending_s, Supervisor))
  else None()
}

/* Examine the current interrupt state and return an interrupt to be *
 * handled (if any), and the privilege it should be handled at.
 */
function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege)) = {
  match getPendingSet(priv) {
    None()       => None(),
    Some(ip, p)  => match findPendingInterrupt(ip) {
                      None()  => None(),
                      Some(i) => Some((i, p)),
                    }
  }
}

(And I think this code could be improved a fair bit too before we include it, e.g. getPendingSet() could be inlined, not having variables called i etc.)

[AFOliveira]

@Timmmm I have a question on this. Can you pull Sail code per instruction? Or in case of switch-case style of Sail, you are pulling that whole block?

[Timmmm]

Yeah you can, though not in this PR. E.g. for this:

function clause execute (UTYPE(imm, rd, op)) = {
  let off : xlenbits = sign_extend(imm @ 0x000);
  X(rd) = match op {
    RISCV_LUI   => off,
    RISCV_AUIPC => get_arch_pc() + off
  };
  RETIRE_SUCCESS
}

You can say "show me the code for when op=RISCV_AUIPC and it will give you

function clause execute (UTYPE(imm, rd, op)) = {
  let off : xlenbits = sign_extend(imm @ 0x000);
  X(rd) = get_arch_pc() + off;
  RETIRE_SUCCESS
}

However I've only seen that in a prototype that @Alasdair showed. I don't know if it has made it into the Sail compiler or asciidoctor-sail yet.

Also someone brought up the valid point that it might be confusing to see synthetic code in the ISA manual that isn't literally in the Sail model. But... I think it is probably fine anyway. We can hyperlink to the place the code came from (also part of that prototype), and maybe even add a little disclaimer explaining the situation.

[nadime15]

You can learn more about the features of the asciidoctor-sail plugin here: https://github.com/Alasdair/asciidoctor-sail

[AFOliveira]

@Timmmm @Alasdair I am currently working in trying to get an index of all instructions into this manual, see #1603. Do you think that whenever I have that index, it would be as easy as a couple lines of code to get that Sail into the index?

[AFOliveira]

You can learn more about the features of the asciidoctor-sail plugin here: https://github.com/Alasdair/asciidoctor-sail

I've came across that before @nadime15, but is that where all this transformations @Timmmm mentioned is being done?

[wmat]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet.

[nadime15]

@AFOliveira The last chapter, Splitting Sail Definitions, seems to describe what @Timmmm demonstrated. However, I would double-check if it actually works as expected. For instance, when I tried pulling in Sail code, including the function header (function clause execute), I had to change it a bit to make it work, which differed slightly from the description in the PDF.

[AFOliveira]

@AFOliveira The last chapter, Splitting Sail Definitions, seems to describe what @Timmmm demonstrated. However, I would double-check if it actually works as expected. For instance, when I tried pulling in Sail code, including the function header (function clause execute), I had to change it a bit to make it work, which differed slightly from the description in the PDF.

I've tried this many months ago and I was also not able to do so. Thus, my question on individual instructions, rather than blocks. Isn't what @Timmmm was describing a new feature, that may not be on that repo yet?

[AFOliveira]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet.

Moreover, I see that as a problem given that the information is not going to be static in this manual, how would ratification look? Would the output pdf be ratified rather than the asciidoc source? Would we it be dependent on Sail being ratified and this tool?

Please don't misunderstand me, I think this is awesome work, I just want to poke around and understand how this process may happen.

[wmat]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet.

Moreover, I see that as a problem given that the information is not going to be static in this manual, how would ratification look? Would the output pdf be ratified rather than the asciidoc source? Would we it be dependent on Sail being ratified and this tool?

Please don't misunderstand me, I think this is awesome work, I just want to poke around and understand how this process may happen.

The thinking was/is that the SAIL index would be versioned at the time a riscv-isa-manual release was published with the SAIL index version described within the release as a point-in-time index. However, I don't believe a decision was ever made for how to do this. I was always hopeful that v1.0 of the SAIL model would be the first version included with a published ISA release.

[Alasdair]

Something to consider here is that the asciidoctor-sail plugin currently only targets PDF (as far as I know). It may be possible to transpile it to work with asciidoctor.js but I have not tried yet

It should just work with any Asciidoctor output format, for example the Sail manual is built with the plugin outputting to html. You only need asciidoctor.js if you want to build Asciidoc into html client-side right? Last I looked, the RISC-V manuals used quite a few other plugins like asciidoctor-bibtex and asciidoctor-mathematical, do those work with asciidoctor.js?

I've came across that before @nadime15, but is that where all this transformations @Timmmm mentioned is being done?

Currently the translation is done by Sail - provided it's explicitly requested with an annotation on the definition. Right now the structure of the Sail tries to follow the granularity of the unprivileged spec, so because 4.2.2 has a single section and encoding diagram for "Integer Register-Register Operations" which combines SLL, SRA, ADDW etc. we also do the same.

I think for the transformation to really work it might require the development version of the Sail compiler/plugin, as I had to implement additional annotations in the AST to correctly re-sugar the code after the constant-folding and constant-propagation passes are applied to simplify the definition. I'm planning a new release soon though.

[AFOliveira]

Currently the translation is done by Sail - provided it's explicitly requested with an annotation on the definition. Right now the structure of the Sail tries to follow the granularity of the unprivileged spec, so because 4.2.2 has a single section and encoding diagram for "Integer Register-Register Operations" which combines SLL, SRA, ADDW etc. we also do the same.

I think for the transformation to really work it might require the development version of the Sail compiler/plugin, as I had to implement additional annotations in the AST to correctly re-sugar the code after the constant-folding and constant-propagation passes are applied to simplify the definition. I'm planning a new release soon though

@Alasdair I may not have fully understood your answer, but from what you're saying, in cases like Integer Register-Register Operations, we can't split them apart for now, correct? Would the idea be to place them in the spec exactly where that text appears so they serve as complementary information?

I see how this approach might make merging into the spec easier in its current form, but I find the switch-case style of Sail somewhat problematic. The way the spec is written in those sections makes it difficult to locate information throughout the manual, and importing that structure into Sail seems to perpetuate that issue—would you agree?

I'm working on developing a well-structured instruction index (similar to what other ISAs have) to improve manual searchability. Ideally, I’d love to have Sail indexed per instruction, but I assume that isn't feasible yet. My questions were meant to clarify whether, regardless of the current Sail source code, we will eventually be able to see this information split. Is that something your new release will enable?

[Alasdair]

I see how this approach might make merging into the spec easier in its current form, but I find the switch-case style of Sail somewhat problematic. The way the spec is written in those sections makes it difficult to locate information throughout the manual, and importing that structure into Sail seems to perpetuate that issue—would you agree?

I would agree with this regarding the structure of both the Sail and the manual. We could re-factor the Sail, but I do think staying as close as possible to current manual is also important.

My questions were meant to clarify whether, regardless of the current Sail source code, we will eventually be able to see this information split. Is that something your new release will enable?

I hope so! I did some experiments a while ago where I generated a big html document of all the instructions in the Sail model with this splitting a while ago, and it seemed to work. Right now I'm quite focused on configurability and modularisation of the model, but this is something I'd like to re-visit.

[Timmmm]

Do you think that whenever I have that index, it would be as easy as a couple lines of code to get that Sail into the index?

Yes, should be.

asciidoctor-sail plugin currently only targets PDF (as far as I know)

It definitely works with HTML too. We've been using it for CHERI for a long time.

Moreover, I see that as a problem given that the information is not going to be static in this manual, how would ratification look?

It is static. sail.json.url links to a specific release. We could add a hash in there for double checking if you want.

When a new release of the Sail model happens there would be a PR to update the sail.json.url to that file, and at that point we would review the changes in the document (which may be a little tedious but we can cross that bridge later).

[AFOliveira]

Thank you all for the explanations!
Sorry if I deviated the PR discussion a bit, I'll see how I can integrate this with my work and further ask questions if I need :)

[Timmmm]

Who do we need to review this? There's loads of scope for improvements in future but I think we need to actually start somewhere and this feels like an uncontroversial first step.

[wmat]

@aswaterman any thoughts here?

[arichardson]

I was planning to submit a change that includes sail snippets, is there anything that can be done to move this forward?

[Timmmm]

Rebased & updated to the sail-riscv 0.7 release which I just published. Are there any meetings we could add this to the agenda for?

[arichardson]

This now looks better than the existing code since there is syntax highlighting :) (and it uses the new <<< operator).
SM3P1 before:

SM3P1 after:

[wmat]

So who would be responsible for adding any new include macros to add SAIL snippets in the appropriate places throughout the whole spec? Similarly, who will replace existing hard coded SAIL snippets?

[Timmmm]

I don't think it is anyone's specific responsibility. We should just try and get it done collaboratively in the usually open source way. I imagine it will be a relatively slow process since we'll probably want to change some of the Sail code to make it read, but that's fine.

[wmat]

Sounds good to me!

[aswaterman]

We are still trying to decide how best to integrate SAIL model snippets into the spec. The current thinking is to include them in an auto-generated, one-instruction-per-page appendix, not in the mainline spec. But the mechanism for that is TBD.

To allow progress to be made on contributing SAIL model snippets in the meantime, the proposal is to add them as ASCII text files in a new sail/ directory whose filenames correspond to the instruction mnemonics (e.g. sail/addi for ADDI). For the time being, they'll just be sitting in that directory with no function. But once we decide on a mechanism for including these snippets, we can easily do so in an automated fashion.

[gfavor]

Are these snippets also being auto generated and populated into the sail/ directory? If not, then how do these snippets in the sail/ directory stay up-to-date with the full SAIL model?

[aswaterman]

If we want to automate keeping the snippets consistent with the upstream SAIL model, that's fine with me, but it's seemingly an exercise outside the scope of this repo.

[allenjbaum]

Certainly there has been a proposal to add tags into Sail, and references to those tags in the asciidoc. How UDB figures into that is also a consideration,

…

On Tue, May 6, 2025 at 3:17 PM Andrew Waterman ***@***.***> wrote: *aswaterman* left a comment (riscv/riscv-isa-manual#1838) <#1838 (comment)> If we want to automate keeping the snippets consistent with the upstream SAIL model, that's fine with me, but it's seemingly an exercise outside the scope of this repo. — Reply to this email directly, view it on GitHub <#1838 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJTQRRCOIL53A3JQCWL25EYGFAVCNFSM6AAAAABWHQA6L6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDQNJWGI2DOMRSGQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[AFOliveira]

As @allenjbaum mentioned, UDB already is generating an "Instruction Appendix" - Sail could easily be added there if the Sail community is keen on joining efforts in that area. I tried to keep the appendix as minimal and "ratified" as possible, and so maybe waiting for Sail 1.0 would be wise. See the instruction appendix - instructions_appendix.pdf

[Timmmm]

That "instruction appendix" seems like it's going to end up duplicating a lot of the actual spec. For example look at this random vector instruction in the ISA manual. It's almost exactly the same information as in the instruction appendix. Are we going to duplicate it?

It seems to me that the main problem the instruction index addresses is the fact that lots of the ISA manual is written in prose and it is quite hard to read - see #1396. If it were all written in the style of the vector instructions I don't see why we'd need it in the manual.

To allow progress to be made on contributing SAIL model snippets in the meantime, the proposal is to add them as ASCII text files in a new sail/ directory whose filenames correspond to the instruction mnemonics (e.g. sail/addi for ADDI).

But we already have a better mechanism via the JSON bundle and sail-asciidoctor, as used in this PR?

[AFOliveira]

Yeah, that duplication issue happens mostly in the V extension, but only in the "description" field - there was an attempt at solving this by @drom by using something similar to this PoC in which the information there is fetched via regex instead of being handwritten.
However, for a lot of non-V instructions, the problem is more lack of information than duplication, because there are cases in which information is either scarce or - as you rightfully mention - written in a way that is hard to digest. All other ISAs have similar looking instruction appendix for this reason.

Now, for Sail, there is an instruction appendix version with Sail in an effort led by @ThinkOpenly, but if Sail has evolved and has a better way of fetching per-instruction Sail code, this is definitely something we (UDB and Sail community) should work together to achieve