The Sail instruction-set semantics specification language

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

50 points by weinzierl 6 days ago | 8 comments

▲ timhh 6 days ago | parent | next [-]

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.

▲

Y_Y 6 days ago | parent [-]

I see the RISC-V Sail repo mentions compiling to SystemVerilog. That would be amazing, if you could specify instruction semantics and have that transformed all the way into silicon.

	▲	aseipp 6 days ago \| parent \| next [-]
		It says they intend the backend to be used for FEC, so it's probably an untimed model that it outputs. Sail would probably generate bad SystemVerilog anyway even if it was timed/synthesizable because the language doesn't have any concepts to express things like pipelining or the necessary concurrency primitives or properly structured modules for the output netlists. If you want a high-level RTL with some of the dependent features of Sail, but for hardware that can generate good SystemVerilog, I think Bluespec is probably the best complement.
	▲	timhh 6 days ago \| parent \| prev [-]
		It's still kind of experimental. Also the purpose is more for formal verification against a real design. The RISC-V model doesn't have any microarchitectural features you'd need for a real chip - not even pipelining - so it would be very slow. Still... it is tantalisingly close to a really nice HDL for design purposes. I have considered trying to make a pipelined RISC-V chip in Sail with all the caches, branch predictor etc. One feature that makes it a little awkward though is that there isn't really anything like a class or a SV module that you can reuse. If you want to have N of anything you pretty much have to copy & paste it N times.

▲ Cieric 6 days ago | parent | prev | next [-]

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?

	▲	timhh 6 days ago \| parent \| next [-]
		Yeah you can describe basically any ISA including SIMD. The RISC-V model doesn't support packed SIMD (the P extension) but it does support Vector.
	▲	stolencode 3 days ago \| parent \| prev [-]
		This looks and feels like "Verilog Lite."

▲ tempodox 6 days ago | parent | prev [-]

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.