The Sail instruction-set semantics specification language (alasdair.github.io)

I've used this a lot via the RISC-V Sail model: https://github.com/riscv/sail-riscv

It's a really nice language - especially the lightweight dependent types. Basically it has dependent types for integers and bit-vector lengths so you can have some really nice guarantees. E.g. in this example https://github.com/Timmmm/sail_demo/blob/master/src/079_page... we have this function type

  val splitAccessWidths : forall 'w, 0 <= 'w . (xlenbits, int('w)) ->
    {'w0 'w1, 'w0 >= 0 & 'w1 >= 0 & 'w0 + 'w1 == 'w . (int('w0), int('w1))}

Which basically means it returns a tuple of 2 integers, and they must sum to the input integer. The type system knows this. Then when we do this:

  let (width0, width1) = splitAccessWidths(vaddr, width);
  let val0 = mem_read_contiguous(paddr0, width0);
  let val1 = mem_read_contiguous(paddr1, width1);
  val1 @ val0

The type system knows that `length(val0) + length(val1) == width`. When you concatenate them (@ is bit-vector concatenation; wouldn't have been my choice but it's heavily OCaml-inspired), the type system knows `length(val1 @ val0) == width`.

If you make a mistake and do `val1 @ val1` for example you'll get a type error.

A simpler example is https://github.com/Timmmm/sail_demo/blob/master/src/070_fanc...

The type `val count_ones : forall 'n, 'n >= 0. (bits('n)) -> range(0, 'n)` means that it's generic over any length of bit vector and the return type is an integer from 0 to the length of the bit vector.

I added it to Godbolt (slightly old version though) so you can try it out there.

It's not a general purpose language so it's really only useful for modelling hardware.

I really like the idea of this. I wonder if I can convince my work to use it for our hardware. Are things like SIMD, SIMT, and other weird formats easy to represent in this kind of language? Or should I just assume anything describable in Verilog/HDL can be described in this language.

This also brings up another question if anyone knows. Is there a term for hardware description languages similar to turning complete for programming languages, or is there a different set of common terms?

This looks like it could help with formal verification of instruction set semantics (something that hasn't been done for x86). That would be highly interesting.