sysr docs · start here

sysr, in levels

sysr is a hardware description language written for models to write and people to review. A design is typed s-expressions, with one defining form per signal and a width on every value. Before any Verilog exists, the checker proves every addition, every index and every stated property for all reachable states, by k-induction with z3, or rejects the design with a trace. Only then does the backend write Verilog-2005 for Yosys, Icarus and an FPGA. With it come an RV64IM core proven against a specification of the instruction set, the devices around it, a board build, and a benchmark of hardware tasks for models.

22hardware tasks in the benchmark, from a priority encoder to an instruction cache

34diagnostic codes, each with a stable meaning a program can act on

33spec functions in isa.sysr, the instruction set the core is proven against

2,700lines of Racket in the toolchain, checker, verifier and backend included

89test cases in make test, over a corpus of 48 designs

Two stacks, one language

Read each stack from the top: what is written is at the top, what runs is at the bottom. The first stack is any design, from its source to an FPGA. The second is sysr's own RISC-V system, built the same way, where the specification is itself sysr. Each arrow between levels is a translation or a proof, and the tools on the right are what checks it. Select a level to see what lives there and who vouches for it.

What checks each step

the source a person or a model writes proven, or checked on every build outside tools, trusted or tested the hardware

One design, through every level

The docs' example is counter: four bits that count from 0 to 9 while en is 1, then wrap to 0 (the tour writes it, breaks it and fixes it). Here is what happens to it on its way down, with what sysr printed when the docs were last built. Step through it, or play it.

The ideas behind sysr

One defining form per signal

A signal is defined once, by a let, a reg, a mem, a drive or an instance, and never assigned in pieces. So a latch cannot be written, and an output driven twice or not at all is an error the checker names.

Proofs first, simulation after

Widths, indices, overflow and every ensures and invariant are proven for all reachable states before a line of Verilog is written. A failure is a trace from reset, short enough to read. Simulation and synthesis still run, as checks on the backend and the tools.

Diagnostics as data

Every problem has a stable code, a span, the expected and actual types, the obligation, a trace and suggested fixes, as JSON with --json. A model reads them in its repair loop; Diagnostics lists them all.

The instruction set, written once

isa.sysr says what each RV64IM instruction does, as spec functions. The core's units are proven equal to them, and sysi's machine-code check reads the same file, so the compiler and the core agree on one meaning.

How to read these docs

To see sysr work, start with the tour: one design checked, broken, fixed and built, with real output. Writing hardware covers the language and how the toolchain reads it, How designs are proven the verifier, and Verilog out the backend. The core, its specification, its simulator, its devices and the board each have a page under "The core". For models, there are the benchmark and the diagnostics. The whole language is in the reference, which is also the model's system prompt. Every page ends with In the source: the files it explains, as they are in the code today. Words you don't know are in the Glossary.