[HN Gopher] The Sail instruction-set semantics specification lan...
       ___________________________________________________________________
        
       The Sail instruction-set semantics specification language
        
       Author : weinzierl
       Score  : 19 points
       Date   : 2025-07-26 19:59 UTC (3 hours ago)
        
 (HTM) web link (alasdair.github.io)
 (TXT) w3m dump (alasdair.github.io)
        
       | timhh wrote:
       | 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 wrote:
         | 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.
        
           | timhh wrote:
           | 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.
        
       ___________________________________________________________________
       (page generated 2025-07-26 23:00 UTC)