Sail has arbitrary precision integers, but in order to generate pure bitvectors we must constrain them to some upper bound. As described above, we can insert dynamic checks to ensure this constraint is never violated at runtime.
If we have a Sail type bits('n), where 'n is unconstrained, then we cannot know how many bits to use to represent it. Instead we use a bitvector of this length, plus a width field. We will generate runtime checks to ensure this length is sufficient.
If we have a generic vector, vector('n, 'a), where 'n is unconstrained, then we represent it as a vector of at most this length.
val union_ctyp_classify : Jib.ctyp -> boolSome SystemVerilog implementations (e.g. Verilator), don't support unpacked union types, which forces us to generate different code for different unions depending on the types the contain. This is abstracted into a classify function that the instantiator of this module can supply.
val register_ref : string -> Smt_exp.smt_expHow we handle register references differs between backends