A formal specification of XISA (Xsight Labs' X-Switch Instruction Set Architecture) written in Sail.
This project models XISA revision 1.20 (document TD-402-00, January 27, 2026). The spec PDFs (current and previous revisions) and pointers to all source documents are in references/.
XISA defines packet processing for the X-Switch family of programmable network switches. This project provides a machine-readable, executable formal model of the ISA, inspired by the Sail RISC-V model.
Alongside the Sail model there is a Rust playground (validated against the model by differential tests) with an assembler for the official XISA syntax and a full-PFE simulator (Programmable Forwarding Engine: parser → MAP): a raw packet runs through a parser program, hands off to a MAP program, and produces the egress — the official Xsight example programs in examples/ assemble verbatim and run end to end. A web playground runs both ISAs and the full PFE flow interactively in the browser.
Requires the devcontainer CLI.
# Build the dev container
devcontainer build --workspace-folder .
# Configure and build
./dev.sh cmake -B build
./dev.sh cmake --build build
# Run tests
./dev.sh ctest --test-dir build --verboseSee docs/commands.md for the full commands reference.
See the spec coverage page for spec coverage and docs/todo.md for known issues.