Make instruction formats extractable

[ThinkOpenly]

Instruction formats should be formalized in some consistent way. A cheap, but less robust means is via attribute:

$[format I]
mapping clause encdec = RISCV_JALR(imm, rs1, rd)
  <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111

In talking with Alasdair Armstrong, he suggested a much better way that requires a lot more effort. Per an email from Alasdair:

[...] maybe the best thing would be to do encdec in two steps, i.e. add a data-structure like:

union instruction_format = {
    RFormat : { funct7: bits(7), rs2 : regidx, rs1: regidx, funct3 : bits(3), rd : regidx, opcode : bits(7) }
    IFormat : { imm : bits(12), rs1 : regidx, func3 : bits(3), rd : regidx, opcode : bits(7) }
    /* and so on */
}

then have two mappings bits(32) <-> instruction_format and instruction_format <-> ast.

[ThinkOpenly]

I used "phone a friend" help (Alasdair again), and he showed me how to initialize one of the tagged union's structs:

let a0 : instruction_format = IFormat(struct { imm = 0b000000000000, rs1 = 0b00000, func3 = 0b000, rd = 0b00000, opcode = 0b0000000 })

Using this, I was able to get something much more useful to at least compile successfully:

val fmtencdec : ast <-> instruction_format
scattered mapping fmtencdec
mapping clause fmtencdec = UTYPE(imm, rd, op)
  <-> UFormat(struct { imm = imm, rd = rd, opcode = encdec_uop(op) })

val fmt2bits : instruction_format <-> bits(32)
scattered mapping fmt2bits
mapping clause fmt2bits = UFormat(struct { imm = imm, rd = rd, opcode = opcode })
  <-> imm @ rd @ opcode

end fmt2bits
end fmtencdec

If I understand things correctly, then, we'd need to add a mapping from the various formats to the final bits(32). This would be by extending fmt2bits mapping, above with an additional mapping per format (not per instruction group).

Then, for each instruction (group), we'd replace the current encdec mapping (ast <-> bits(32)) with a fmtencdec mapping (ast <-> instruction_format).

(And then find out what breaks.)