verylogic Sail ISA Workspace
Understand why the workspace uses an executable ISA language, then choose an instruction-set module to run its model, learn its machine contract, and study its supporting tools.
Why an ISA language?
Sail occupies the boundary between an architecture manual and a processor implementation. It makes instruction semantics executable without turning one pipeline, simulator, or proof system into the architecture itself.
Compare Sail with prose, C/C++, Verilog/SystemVerilog, and proof assistants →
Common teaching contract
ISA modules share source directives, bit-exact and ordered assertion rules, opening annotated machine-image manifest blocks, runtime override precedence, comment levels, strict reload, and staged publication.
Read the common teaching contract →
ISA modules
Hack
The 16-bit teaching computer from nand2tetris, modeled in Sail with an assembler, runnable programs, source assertions, and end-to-end tests.
Inside an ISA module
Each module starts with an overview and tutorial, continues with the ISA guide, and places implementation-heavy assembler and execution material under Toolchain internals. The common teaching contract defines shared source/artifact behavior; ISA pages focus on target syntax, encoding, completion, and model semantics.
Repository setup
Installation, supported platforms, workspace commands, and the convention for adding another ISA are maintained in the workspace README.