The language · the verifier

How designs are proven

sysr does not simulate a design to find out whether it works. It turns every place the design could go wrong into an obligation and proves each one for every reachable state, by k-induction with the z3 solver. An obligation either is proven, or fails with a trace from reset, or is reported as not inductive, with the state that breaks the proof. This page explains what is proven, how, and how to read the answer.

Obligations

The verifier (sysr/verify.rkt) collects one obligation per place, per module, and proves each in every cycle:

An obligation inside an if branch is required only when that branch is taken, and one in a later operand of and, or or => only when the earlier operands do not already decide the result: the encoder carries a guard down the expression, so (if (== count 9) 0 (+ count 1)) asks for count + 1 to fit only where count is not 9. Expressions inside properties carry no obligations of their own. A module's own requires and assumes are assumed in every cycle; every assume is listed in the summary (W001). Before anything is proven, the verifier checks that the requirements can hold at all in the first cycle after reset: if they contradict each other, every property would be vacuously true, and the module gets V005 instead. A query z3 cannot decide within the time limit (--timeout-ms, 10,000 by default) is never a pass: in a base case it is V010; in a step it only keeps the obligation from being proven at that depth.

A module as a transition system

Each module, once per parameter set, is a transition system. Its registers are the state; their reset values are the initial state; inputs are free in every cycle. Cycle −1 is the reset cycle: rst is high there in the base case, and low in every cycle after it, since a later reset only returns the design to the state every run starts from. A memory has no reset value, so its contents after reset are unknown and nothing is proven from them. The encoder writes, for each cycle, every let, output and next register value as an SMT-LIB bit-vector term; array registers become SMT arrays and structs are split into their fields.

k-induction

For k = 1, 2, … up to the depth (--depth, 8 by default), with the obligations not yet proven or refuted:

1. Base case. From reset, does each obligation hold in cycle k−1, given that every obligation not yet refuted held in cycles 0 … k−2? Each k adds one cycle, so after depth K every cycle up to K−1 has been checked from reset. If z3 finds a run where it fails, that is a real bug: the obligation is refuted with a trace from reset.
2. Step. Take any k+1 consecutive states, pairwise distinct, the first of which has a predecessor. If every candidate obligation holds in the first k of them (and the ones already proven hold in all of them), does each hold in the last? The verifier looks for the largest set of candidates that is k-inductive together: it drops every candidate z3 finds a counterexample for and asks again, until none fails. Those that remain are proven at depth k.

This is sound because the base case has checked every obligation from reset up to the same depth: assuming all of them in k cycles to prove each in the next covers every reachable state. The depth in the summary line is the deepest k at which some obligation was proven. What is still neither proven nor refuted after depth K is V007, not inductive, with the last step's trace.

The counter, under k-induction

Step through the proof. The figure runs the algorithm above on the counter, with the counter's state (sixteen values of count, one bit of en) small enough to search by hand in this page instead of with z3. Pick one of three versions: the tour's counter.sysr; the same counter with both its properties taken out, leaving only the overflow obligation of (+ count 1); and counter-bug.sysr, which wraps after 10. Change the depth to see when each answer appears.

the reset stateany state: possibly unreachablewhere the obligation fails

Three things to take from it. Without properties, the overflow is still proven, but at depth 6: the step must rule out chains of states that count up to 15, and it can only do so once the chain is longer than the longest one that exists (10 to 15; nothing counts up into 10, because 9 wraps to 0). With the invariant (<= count 9), every step starts from a state with count ≤ 9, the chains vanish, and everything is proven at depth 1. An invariant is how a designer tells the verifier which states matter; in this counter the ensures says the same thing, since q is count. In counter-bug.sysr, the ensures first fails in cycle 10 after reset; at the default depth the base case does not get that far, so the answer is V007, and from depth 11 on it is a real trace from reset. These outcomes agree with what sysr check reports; the two runs of counter-bug.sysr are shown under the figure when its depth is 8 or 12.

Reading "not inductive"

A V007 trace begins in cycle 0 with any state that satisfies every property, and the verifier cannot tell whether a run from reset can reach it. So the message says possibly unreachable, and the fix it suggests is an invariant that excludes the starting state. There are two cases, and they need different fixes, which is why V007 is a code of its own:

• The start is unreachable. The property is true but too weak to carry itself from one cycle to the next. Add an invariant that says what is true of the state. The reference's pair example is the extreme case: two registers counting together, and a promise that holds for up to 15 steps from a state where they differ, so no depth proves it; (invariant (== x y)) does, at depth 1. The corpus has another: a FIFO without its count invariant, whose unreachable counts 5, 6 and 7 step among themselves.
• The start is reachable, only far away. A real bug that needs more cycles than the depth to show. Raise --depth: the base case reaches it and the code becomes the real one (V002, V004, …) with a trace from reset, as counter-bug.sysr does at depth 12.

Distinct states, and why past drops them

The step asks for states that are pairwise distinct. For a property that depends only on the current cycle this loses nothing: a counterexample that visits a state twice can have the loop between the visits cut out, and what is left is still a counterexample. It also makes the method complete for finite systems in principle, since a deep enough step runs out of distinct states, which is exactly what proves the bare counter at depth 6.

(past e) breaks that argument. A property with past reads the previous cycle's values, inputs included, and inputs are not part of the state, so cutting a loop can change what the property sees. The loop can even be the whole counterexample: in tests/corpus/v006_past_selfloop.sysr a register stays put while an input is 0, and the invariant fails in a run where the state repeats. Feature 003 found the constraint unsound there, since it hid failures like this one; now verify.rkt drops the constraint for any module whose properties, or whose instances' contracts, use past. A property with past is checked from the second cycle after reset.

Instances: assume-guarantee

A child module is verified on its own. In its parent it is replaced by its contract: its outputs are fresh values in every cycle, constrained only by its ensures. The parent must prove the child's requires on what it connects, in every cycle (V001, with the requirement's own line as related information), and may then assume the child's ensures for everything else. One exception keeps this from being circular: a requirement is never proven from the same instance's guarantee in the same cycle. tests/corpus/v001_circular.sysr is the case it rules out: an instance whose input is its own output, required to be 1 and promised to be 1. Proofs stay local and fast, at a price: a parent sees only what a child promises, so a child needs ensures that say what its parents need.

Traces, waveforms and replay

When z3 finds a counterexample, the verifier reads the model back cycle by cycle (read-cycles): each input, each register with a reset value (memories are left out), and each instance's outputs, with enum values shown by variant name. make-trace in sysr/trace.rkt packs them with the trace's kind (from-reset or induction), its depth and the cycle where it fails; this is the trace of a diagnostic in --json, and the indented cycle lines of the text report. With --vcd DIR, write-vcd also writes one waveform per trace, for any wave viewer: scalar and vector signals, ten time units per cycle (arrays, structs and enums are left out). tx->text, also in trace.rkt, prints typed expressions back as sysr text for messages and obligations.

A trace from reset is a claim about the hardware, and the tests check it: tests/codegen-test.rkt takes every trace from reset in the corpus, for designs without instances or memories, drives the trace's inputs into the generated Verilog in Icarus, and requires every register to match the trace in every cycle.

How z3 is driven

sysr has no solver interface of its own. sysr/shared.rkt loads sysp's reader and z3 driver unchanged from a sysp checkout beside sysr (or wherever SYSP_ROOT points), with dynamic-require, and stops with a message naming the missing file if it is not there. The driver starts one z3 process per run, with the timeout set; the verifier declares each variable once, prefixed per module and per cycle so that one process serves every module, and asks each question inside a push that it pops afterwards. Hardware arithmetic is modular, so bit vectors are exact; an addition's carry, for instance, is read off one extra bit:

Each definition is tagged with the last cycle it mentions, and a query up to cycle L asserts only those tagged L or earlier. The answers do not change, and z3 does not build the logic of cycles a query does not reach; on the core's multiplier this took the proof from about three minutes to one second. SYSR_PROFILE=1 prints every query that takes over a second.

The tests that hold it

tests/verify-test.rkt runs every verification design of the corpus (those whose names start with v and a digit, or ok_) and requires exactly the codes its first line expects, each in under ten seconds. It checks that a real failure is a trace from reset that ends where the obligation fails, that a property true but not inductive is V007 with an induction trace and an invariant fix (and that the same FIFO with its invariant is proven at depth 1), that an instance's requirement is proven where it is used, that a requirement is not proven from the same instance's same-cycle guarantee, that assumes are listed, and that the FIFO of the grammar contract is proven at depth 1.