Tracking issue: Polymorphic bitfields and other bitfield improvements.

[Alasdair]

Issue

It recently came up in the RISC-V meeting that the bitfield syntax is limited when we want bitfields with fields that can vary in width depending on XLEN, or the virtual memory translation scheme.

bitfield <name> : <bitvector_type> = {
   <fields>
}

I propose allowing type parameters on bitfields, with one of the following syntaxes:

Either with parameters like other data type definitions, which could have the constraint like:

bitfield <name>(<params>) : <bitvector_type>, <constraint> = {

}

or like so (perhaps allow either?):

bitfield <name>(<params>), <constraint> : <bitvector_type> = {

}

Alternatively we could go with function type quantifier style:

bitfield <name> forall <params>, <constraint> : <bitvector_type> = {

}

I think the second is probably the best and most consistent with the rest of the language.

Desugaring would be fairly straightforward

struct <name>(<params>), <constraint> = {
    bits : <bitvector_type>
}

Notice however, this means that many of the type parameters can end up becoming phantoms when desugared, and this has historically caused problems for some of our backends - we might need to carefully erase phantom type parameters to make this work.

The fields could reference type parameters, so we could have something like:

struct foo('n) : bits(xlen) = {
    field : 'n .. 16
}

The question here is the 'n .. 0 should imply that 'n < xlen and 'n <= xlen. We would generate these constraints during desugaring and add them to the struct type.

Open questions

Should we add syntax for constructing bitfields directly? It occurs to me we don't have this. Proposed syntax would mirror structs:

let bar = bitfield { field = 0xFFFF };

However, the question is what happens when the fields do not cover all the bits in the bitfields? Maybe we allow specifying the initial bits like:

let bar = bitfield { zeros() with field = 0xFFFF };

I am slighly wary of this as it is more non-intuitive syntax that would need to be explained and learned. A better solution may be to allow default values for bits in the type definition, perhaps:

struct foo('n) : bits(xlen) = {
    default zeros(),
    field1 : 'n .. 16,
    field2 : 7 .. 0 = 0xFF,
}

There would need to be a check that fields with default values are consistent if they overlap, which would require a fairly sophisticated check if we wanted to allow this, so maybe it is better to just check that fields with default values do not overlap.

A side point relevant here, is would it be useful to have SystemVerilog style operators +: and -: in Sail? These would be useful when a parameter specifies a width, i.e. rather than x[hi .. lo] it's x[low_start_bit +: width].

[martinberger]

Could we not, as an intermediate step, allow named fields in a bitvector of length 0 or even of negative length (where negative length is counted as length 0, too)? Then a bitfield like this

bitfield BFF : bits(3) = {
    A : 2 .. 0,
    B : 0 .. 1,
    C : 0 .. 17
} 

would be isomorphic to

bitfield BFF : bits(3) = {
    A : 2 .. 0
} 

but it would still have update functions update_B and update_C which must be the identity function. This could be a stopgap solution, helping with bitfield definitions that work for RV32 and RV64, where a field is zero-length in RV32 and non-zero in RV64. We can then use the same update_... function for legalisation in RV32 and RV64.