Start · with real output

A tour

One small design, from an empty file to Verilog: a counter that counts from 0 to 9 and wraps. We check it, break it with an off-by-one, read what sysr says about the break at two depths, fix it and build it. Every output on this page is what sysr printed when the docs were last built.

1. Write the design

This is docs/site/examples/counter.sysr. A module lists its declarations as an unordered set: ports, a register, properties, a drive. Select a line to see what it says.

There is no clock or reset in the text. A module with a register has them implicitly, as the ports clk and rst (synchronous, active high), and no expression can name them. Nothing assigns count anywhere else: its reg form is its only definition, which is how sysr rules out latches and half-assigned signals.

2. Check it

bin/sysr is a shell script: it sets SYSP_ROOT (sysr loads sysp's reader and z3 driver from a checkout beside it) and runs sysr/main.rkt, which takes the subcommand check, build or fmt.

Three obligations: that (+ count 1) never carries out of four bits, that the ensures holds in every reachable cycle, and the same for the invariant. All three were proven at k-induction depth 1, the shallowest there is. "0 hole(s)" counts the ?name placeholders a design may still contain; a design with holes is type-checked, but neither verified nor built.

What happened in between is check-sources in sysr/driver.rkt. Step through its stages; the lines are quoted from the file as it is now.

Each stage runs only if the one before reported no error, so the verifier never sees a design with a type error, and a design with holes is not verified. check-sources never raises: an internal failure becomes the diagnostic I001. sysr check exits with 0 when the report is clean and 1 otherwise; --json prints the same report as JSON, the form a model reads.

3. Break it

Now the same counter with an off-by-one: it wraps after 10, not 9, and its invariant is gone. The ensures still promises q ≤ 9, which is now false: q reaches 10.

This is V007, not inductive, and the trace is not a run from reset. Read its header: cycle 0 is any state that satisfies every property, possibly one no run can reach. Here it is count = 2; eight cycles of en = 1 later, count is 10 and the ensures fails.

Why not a real trace? k-induction does two things for each k up to the depth (8 unless --depth says otherwise). The base case runs the design from reset and checks each of the first k cycles: from reset, count needs ten cycles of counting to reach 10, so no base case up to depth 8 can see it. The step starts from an arbitrary state: from count = 2 the property holds for eight cycles and then fails, so no step proves it. A property true as far as the base case looked, with no step that proves it, is reported as V007 with the step's trace. sysr cannot tell from this alone whether the starting state is reachable, so it says "possibly unreachable" and suggests an invariant.

The summary line says one of the two obligations was proven. That is the overflow of (+ count 1), at depth 5: without an invariant, the only way to reach count = 15 counting up is from 11, which nothing leads to. The step at depth 5 asks for six distinct states that count up to 15, and there are only five (11 to 15), so it succeeds there. The depth in the summary is the deepest k at which any obligation was proven. How designs are proven takes this apart.

4. Look deeper

A real bug that takes more cycles to show than the depth looks like V007. Give the base case enough cycles and it becomes a counterexample from reset:

Now the code is V002, ensures may not hold, and the trace starts at reset: count = 0, then ten cycles of counting, then 10. This trace is a real run, and the tests replay traces like it in Icarus on the generated Verilog to check that the hardware does the same. Which reading of a V007 is right, an unreachable start or a deep bug, is the question to ask of every one: here a deeper check settles it.

5. Fix it

Wrap at 9 again, and say what is true of the register: (invariant (<= count 9)). That is counter.sysr from step 1, which checks at depth 1. For this counter the invariant is belt and braces: q is count, so the ensures already says count ≤ 9 and is inductive by itself. In designs whose outputs show less of their state, an invariant like this one is what makes the step go through.

6. Build it

sysr build runs the same check, then writes Verilog, and only if everything is proven: a design with an error or a hole gets a report and no file.

Select a line on either side to see where it comes from or what it became.

Every compound expression is wrapped in { } so that Verilog sizes it by itself and each operation wraps at exactly the width sysr gave it. The initial line gives count its reset value at power-up, so on an FPGA the design starts in its reset state from configuration. The properties leave nothing in the Verilog: they were proven, not compiled. Verilog out has the rest of the backend.

Where to go next

The language in full is on Writing hardware and in the reference; the verifier on How designs are proven; every code the checker can report on Diagnostics. To see sysr at scale, read The RV64IM core, proven against isa.sysr. To see how models fare with it, the benchmark.