package libsail

  1. Overview
  2. Docs
val max_unknown_integer_width : int

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.

val max_unknown_bitvector_width : int

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.

val union_ctyp_classify : Jib.ctyp -> bool

Some 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.

OCaml

Innovation. Community. Security.