This is a quick write-up about Sail. Sail seems like an interesting project to specify ISA instructions in a formal, machine-readable way.

Documentation Link to heading

From 4, we get the basic blurb of Sail:

Sail is a language for expressing the instruction-set architecture (ISA) semantics of processors.

Vendor architecture specification documents typically describe the sequential behavior of their ISA with a combination of prose, tables, and pseudocode for each instruction.

Then, it describes how it works as follows:

A Sail specification will typically define an abstract syntax tree (AST) of machine instructions, a decode function that takes binary values to AST values, and an execute function that describes how each of those behaves at runtime, together with whatever auxiliary functions and types are needed.

Installation Link to heading

Sail is written in OCaml. So, it needs the package manager for OCaml opam.

sudo apt install libgmp-dev opam z3 # or brew install opam gmp
opam init
opam install sail

To see opam paths, opam env can be used to export environment variables.

eval $(opam env)
export SAIL_DIR=`opam var sail:share`

First example Link to heading

This example is adapted from the Sail manual introduction. It demonstrates basic Sail features including type synonyms, register state, scattered definitions, and the instruction decode/execute pattern.

default Order dec

$include <prelude.sail>

// Type synonyms
type xlen = 64
type xlenbits = bits(xlen)
type regbits = bits(5)

// Extension functions
val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
function EXTZ(m, v) = sail_zero_extend(v, m)

val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
function EXTS(m, v) = sail_sign_extend(v, m)

// Registers
register PC : xlenbits
register Xs : vector(32, dec, xlenbits)

// Register access with overloading
val rX : regbits -> xlenbits
function rX(r) = match r { 0b00000 => EXTZ(0x0), _ => Xs[unsigned(r)] }

val wX : (regbits, xlenbits) -> unit  
function wX(r, v) = if r != 0b00000 then { Xs[unsigned(r)] = v; }

overload X = {rX, wX}

// Scattered union for instructions
scattered union ast
val decode : bits(32) -> option(ast)
val execute : ast -> unit

// ADDI instruction
union clause ast = ITYPE : (bits(12), regbits, regbits)

function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
  = Some(ITYPE(imm, rs1, rd))

function clause execute (ITYPE (imm, rs1, rd)) = {
  X(rd) = X(rs1) + EXTS(imm)
}

function clause decode _ = None()
end ast
end decode
end execute

val main : unit -> unit
function main() = {
  // Initialize register x1 with value 10
  X(0b00001) = 0x000000000000000A;
  
  // Decode and execute ADDI x2, x1, 5 (add immediate 5 to x1, store in x2)
  // Instruction encoding: imm=5, rs1=x1, rd=x2, opcode=0010011
  let inst_bits : bits(32) = 0b00000000010100001000000100010011;
  
  match decode(inst_bits) {
    Some(instr) => {
      execute(instr);
      print_bits("x1 = ", X(0b00001));
      print_bits("x2 = ", X(0b00010));
    },
    None() => print("Failed to decode instruction")
  };
  
  ()
}

sail -c 1.sail -o out
gcc out.c $SAIL_DIR/lib/*.c -lgmp -lz -I $SAIL_DIR/lib/ -o out
# or
gcc out.c $SAIL_DIRlib/*.c -I/opt/homebrew/include -L/opt/homebrew/lib -lgmp -lz -I $SAIL_DIR/lib/ -o out 

./out

Output:

x1 = 0x000000000000000A
x2 = 0x000000000000000F