SystemVerilog Generation - Missing Decoder Module

[NicolasVanPhan]

Hello Sail team,

I'm opening this discussion because I encountered an issue while generating SystemVerilog code from a RISC-V-based model written in Sail. In the generated SV code, I couldn't locate a decoder module or function.

This seems specific to the SystemVerilog generation, as:

• When generating a Coq model, the decoder appears as expected, with definitions for decoder, encdec_backwards, and encdec_forwards.
• Additionally, I generated the C emulator and ran some tests. While the results showed errors related to missing CSRs (which I removed), there was no indication of issues with the decoder, suggesting that the C backend likely supports its generation.

Is decoder generation supported for the SV backend? If so, could you advise on any troubleshooting steps or settings that might address this?

Thank you for your time and help!

Best regards,
Nicolas

[Alasdair]

I think the issue is you need to tell Sail to preserve it in the output. The --c-preserve flag works for this (somewhat confusingly, but the SV backend shares enough code with the C backend that it does).

However right now the generator gets stuck generating the decoder because of the size of the decoding logic. That's something I'm working on.

[NicolasVanPhan]

After some debugging, I discovered that the SV backend filters out Sail functions that are not present in the call graph. The call graph itself uses 'initial_calls' as its roots, and it did not include the decoder—changing decoder to ext_decoder fixed the issue by the way (see link to the relevant line).

Once I added it, I also observed that the compilation process gets stuck, which aligns with your observations.

Thank you for your help !

[Alasdair]

No problem, I am trying to fix the decoder generation issue right now.

It's fundamentally the same issue as #689. We don't have enough information about the mapping completeness, so the generation sees every sub-mapping in the encdec mapping and generates logic like 'if encdec_bop fails, then goto ...`. When you consider how many cases encdec has this generates a really complex control flow graph.

[NicolasVanPhan]

Got it, thank you for the clarification!

I also observed that the early mapping_patterns rewrite unrolls encdec_backwards into a large nested series of match {Some .. | None => } statements. Interestingly, it seems to only expand the "backwards" variant of the mapping and not the "forwards" one.

I am referring specifically to the Mappings.rewrite_ast function: https://github.com/NicolasVanPhan/sail/blob/sail2/src/lib/mappings.ml

Could you please explain the purpose of this rewrite?
Thank you in advance!

[Alasdair]

I think the comment at the top of that file kind of explains it in the best way - what we want to do is remove mapping invocations from within match patterns and turn them into regular function applications. In the example it's the mapping(A) pattern we want to remove. The reason we want to do this is that the targets we are generating code for don't support them so we have to get rid of them somehow. Doing this as an early Sail->Sail rewrite means all the backends can share the same code.

    $[<completeness>] match x {
      <pat> => <expr1>,
      mapping(A) => <expr2>,
      <rest>
    }

In the actual RISC-V spec, it might be a little more complicated because we could have something like 0xFF @ encdec_uop(op) @ 0x00 where the mapping (encdec_uop) is a sub pattern of a larger pattern, but the idea is the same. The rewrite takes the above and turns it into:

    let y = x in
    $[mapping_match] $[complete] match ($[complete] match y {
      <pat> => Some(<expr1>),
      z if mapping_forwards_matches(z) => $[complete] match mapping_forwards(z) {
        A => Some(<expr2>),
        _ => None(),
      },
      _ => None(),
    }) {
      Some(w) => w,
      None() => $[<completeness>] match y {
        <rest>
      },
    }

There are a few constraints that make this rewrite as tricky looking as it is:

• We don't want to duplicate any expression (<expr1> and <expr2>)
• We can't change the evaluation order, as this might change the observable side effects of the expression. This includes the order in which we evaluate mapping_forwards relative to all the other expressions.
• The scope of all pattern bindings should be preserved
• The match can be embedded in any context (so we can't use return)
• Mappings can be nested e.g. m1(m2(m3(<pattern>)))

When you have all those constraints I'm not sure there is a simpler rewrite that works in the general case. If we knew however that certain expressions are pure, or certain mappings are total, there are simplifications we could make on a case-by-case basis.