In the JSON backend, pulling the "formal model"/implementation/pseudocode from the Sail parser, as is currently done, already munges the code a bit. For example, riscv_insts_base.sail, addiw looks like:
{
let result : xlenbits = sign_extend(imm) + X(rs1);
X(rd) = sign_extend(result[31..0]);
RETIRE_SUCCESS
}
but as currently parsed, appears like:
{
let result : xlenbits = add_bits(sign_extend(64, imm), rX_bits(rs1)) in {
wX_bits(rd, sign_extend(64, subrange_bits(result, 31, 0)));
RETIRE_SUCCESS
}
}
In the JSON backend, pulling the "formal model"/implementation/pseudocode from the Sail parser, as is currently done, already munges the code a bit. For example,
riscv_insts_base.sail
,addiw
looks like:but as currently parsed, appears like:
There might be some way to leverage the work being done by the "Sail to Asciidoc" project (https://github.com/Alasdair/asciidoctor-sail) for better parsing of some of the content. [Related talk: Sail to Asciidoc]