Properties and verdicts

Verify answers questions about every run of a circuit: every value of every input, at every step, however long the run. The questions are blocks of the Verification section of the palette.

The properties

Block	Its input	Verify answers
Assertion	a boolean that must hold at every step	holds: proved; or fails at step N, with a trace
Target	a condition to reach	reached at step N, with a trace; or unreachable: proved never to happen
Assume	a condition the inputs keep to at every step	nothing: it restricts the runs the others consider

An assertion and a target are two sides of one question: an assertion p holds exactly when a target not p is unreachable. Use whichever reads better: an assertion for what must always be so, a target for a situation that must be possible (that an alarm can sound), or one you want an example of.

Assumptions narrow the runs Verify and the MC/DC tests consider to those where every Assume block's input is true at every step. They say what the circuit's environment guarantees: a sensor's range, two buttons never pressed together. A wrong assumption hides real failures, so keep them few and true.

Verdicts

The Verify tab of the panel lists each property, its verdict, the engine that answered, and the time; the verdicts are written beside the blocks too.

• holds or unreachable: proved, for every run.
• fails or reached, at step N: a run of N + 1 steps shows it. A click on the row plays the trace on the canvas and in the scope, the cursor on the step where it happens; ← and → step through it. Use as stimuli, in the row's right-click menu, copies its inputs to the stimuli, so that ▶ Simulate replays it.
• unknown: no engine answered within the timeout, or within the depth given. Try a longer timeout, another engine, or a smaller circuit.

A result goes out of date as soon as the circuit changes.

The engines

The engine menu of the Verify tab chooses who answers:

Engine	What it does	Good at
portfolio	all of the engines below, side by side; the first answer wins	the default
bmc	bounded model checking: the runs of 0, 1, 2, … steps	counterexamples, the shortest first
kind	k-induction: bmc, and a proof that k steps without failure mean no failure ever	proofs of properties that are inductive after a few steps
br	backward reachability: from the failures back to the initial states	proofs, with an inductive invariant
pdr	property directed reachability (IC3)	proofs of harder properties, with an inductive invariant

timeout is the seconds each property may take, max depth the deepest bmc and kind go. The settings are saved with the circuit. A long run can be cancelled.

Proof certificates

Tick proof certificates in the Verify tab, and a property proved comes with its proof: an SMT-LIB 2 script, each of whose check-sat must answer unsat, that any SMT solver checks. Export proof…, in the row's right-click menu, saves it, and offers to check it with a solver found on the machine (z3, cvc5, bitwuzla, yices). Backward reachability and PDR prove with an inductive invariant, k-induction with its base cases and its step; the script says which, and why it is a proof. intrepid checks every proof before giving it. The tutorial shows one.