Typechecking semantics of multidimensional types

[Jozott00]

I think we haven't discussed the typechecking semantics for accessing multidimensional types yet.

Consider the following example:

register A: Bits<5>
register X: Bits<5><32>

function t1 -> Bits<32> = X(A)
function t2 -> Bits<32> = X(A as Bits<2>)
function t3 -> Bits<32> = X(A as Bits<3>)

Register X has two dimensions, with an index dimension of size 5. This size can’t be represented by a concrete type as it is no power of 2.

Now the question is how to check access to such a register. t1-3 are functions with different index access types:

• t1 has an index type of Bits<5>, which may also contain values up to 31.
• t2 has an index type of Bits<2>, with a maximum value of 3, so it is always in range.
• t3 has an index type of Bits<3>, with a maximum value of 7. This is the next fitting type that can hold all values that can be used to access the index dimension. However, it may also hold values 5-7 which are out of range.

I think t2 must be definitely valid. t3 must also be valid; otherwise, there would be no way to access the outermost dimension 4.
IMO t1 should be valid as well, because it doesn’t differ from t3 which could also be out of range. Additionally, the user didn’t specify any concrete type for the index, so a type error would be pretty confusing.

This leaves us in a state where out-of-range access isn’t statically prevented, which causes undefined behavior. In the case of registers, the user could specify annotations that define the behavior on out-of-range accesses (read and write), e.g. raising an exception or returning some computed value.
However, it is hard to specify such behavior for generic multi-dimensional types (other than registers).

@AndreasKrall, @flofriday, @benedikt-l-huber, @kper What are your thoughts on this?

[AndreasKrall]

Currently we must allow all types for index access. If it cannot be statically determined (eventually with constraint annotations), that the index is in a valid range, a dynamic check has to be added in simulator and hardware either manually or from the generators, e.g. for CSR registers in RISC-V. If no correct constraint is defined, an error should be generated by the type checker.

In the long run I want to support subrange types. Then again it would be possible to statically check the correctness. Furthermore, it would be possible to use the relation notation for register file specification:

using Index = 0..5
using Word  = Bits<32>

register X : Index -> Word
register Y : Word<6>

X and Y have the same type.