Read bounded checks, covers and induction results

Guide Last tested 25 October 2026

A formal result is meaningful only with its property, assumptions, starting states and proof mode. A bounded success says no counterexample was found within the checked steps; it does not establish the property forever. The three runnable examples below distinguish a deeper real failure, an assumption that prevents the relevant behavior, and a weak induction failure at length one that can be resolved by a longer induction or a stronger invariant.

Read the command before the verdict

This page uses the same Yosys 0.70+post binary and built-in SAT engine. The official v0.70 release tag points to 28ba3cb926fe376fa05ebfc1b921747d011d4557; the tested binary reports revision 0c11ea098be065e585a90a06e7b7da49936cf231. Those are different identifiers, so the record retains the tag and the binary banner separately rather than claiming a verified source-to-binary build¹. It does not use SymbiYosys, an external SMT solver or a commercial formal product. The exact command files, initialized registers and target signals are part of the result. The downloadable examples include every source and command file needed to repeat the eight checks.

The pinned sat help gives -seq two relevant meanings: it bounds an ordinary sequential query, but with -tempinduct it postpones the property until after that many steps. The corrected induction commands omit -seq 1, so their base checks include step one and the declared initial state. -prove names the property, -set-assumes enables assumption cells, and -maxsteps caps the induction length. A bounded target search remains a different question from an induction proof².

Use the following labels when recording these examples. They are descriptions of the actual command outcome, not interchangeable badges. In particular, the same words “no model found” occur in successful bounded property checks and in unsuccessful target searches. The question posed to the solver determines what the absence of a model means.

A bounded success can end one step before the bug

The first model has a three-bit initialized counter. Its deliberately bad condition becomes true when the counter reaches five. There are no environmental assumptions and no external input other than the abstract clock. The property asks that bad remain zero. Because step one observes the initial zero value, a five-step sequence contains counts zero through four; step six is the first checked state with count five.

// SPDX-License-Identifier: MIT
module late_bug(input clk, output bad, output [2:0] count);
  reg [2:0] cycles = 0;
  always @(posedge clk) cycles <= cycles + 1'b1;
  assign count = cycles;
  assign bad = cycles == 3'd5;
endmodule

bounded_5.ys reads the model, prepares its top and runs sat -seq 5 -prove bad 0 -show-ports. The literal result is SAT proof finished - no model found: SUCCESS!. deeper_6.ys changes the bound to six and records SAT proof finished - model found: FAIL!. The witness shows the counter reaching five and the property becoming false. The first success was valid for its bound; interpreting it as an unlimited proof would be the error.

The count and step relationship belongs to this initialized synchronous abstraction. It is not a measured number of nanoseconds or a claim about clock startup in a real circuit. When adapting the pattern to a resettable design, state exactly how reset enters the proof and whether the property is disabled while reset is active. A conveniently initialized register in a teaching example must not silently replace a required power-up or reset assumption in a production proof.

Ask whether an assumption removed the behavior you needed

The next model increments an accepted-operation count whenever fire is true. Its target is three accepted operations. The assumption !fire is intentionally wrong for a contract that permits operations: it prevents the counter from advancing. The cover statement names the situation the proof should be capable of exercising.

// SPDX-License-Identifier: MIT
module masked_bug(input clk, input fire, output target,
                  output [2:0] count);
  reg [2:0] accepted = 0;
  always @(posedge clk) if (fire) accepted <= accepted + 1'b1;
  assign count = accepted;
  assign target = accepted == 3'd3;
  always @* begin
    assume (!fire);
    cover (target);
  end
endmodule

With -set-assumes, the six-step check of target == 0 succeeds. That is not evidence that a working interface safely handles three operations; the assumption has forbidden every operation. A four-step target query under the same assumption finds no witness. Removing assumption enforcement from the target query produces the sequence zero, one, two, three, with fire asserted for the first three transitions. This is the behavior that the masked proof excluded.

The command files lower the formal cells, remove the declarative cover cell and implement its reachability question with an explicit final-step target constraint. This is a bounded cover query using the built-in SAT engine, not a SymbiYosys cover run. Both versions ask for the same target at step four; only assumption enforcement changes. That controlled difference makes the source of the misleading success visible.

The constrained target command is printed here as executed; its unmasked counterpart omits only assumption enforcement.

# SPDX-License-Identifier: MIT
read_verilog -formal -sv masked_bug.sv
prep -top masked_bug
chformal -lower
chformal -cover -remove
sat -seq 4 -set-assumes -set-at 4 target 1 -show-ports

An absent cover witness can also mean that the target needs a longer sequence, that an observation is wired incorrectly or that the configuration legitimately disables the feature. Here the unmasked witness isolates the assumption’s effect at the same bound. Do not generalize “cover did not hit” into “the feature is impossible” without a suitable proof. The coverage-hole example separates bounded stimulus evidence from a combinational contradiction: its full-and-empty expression is false for any two-state occupancy, without relying on reachability.

Increase induction depth or strengthen the invariant

The third model starts with both registers at zero. a copies b; b changes only if it is already nonzero and advance is asserted. Consequently, the initialized executions keep both registers zero. The weak property says only that a is zero. The stronger property also carries the fact that b is zero.

// SPDX-License-Identifier: MIT
module induction(input clk, input advance, output weak_ok, output strong_ok,
                 output [3:0] visible, hidden);
  reg [3:0] a = 0;
  reg [3:0] b = 0;
  always @(posedge clk) begin
    a <= b;
    if (b != 0 && advance) b <= b + 1'b1;
  end
  assign visible = a;
  assign hidden = b;
  assign weak_ok = a == 0;
  assign strong_ok = (a == 0) && (b == 0);
endmodule

At induction length one, the corrected base check includes the declared initial state and passes, but the weak inductive step fails. Its counterexample to induction starts with a = 0 and nonzero b, then copies that nonzero value into a. That starting state satisfies the weak property but is not reachable from the model’s initialized zero state. It therefore explains a gap in the induction hypothesis; it is not the same kind of counterexample as the earlier count-five failure.

For strong_ok, the same base-and-step flow completes at length one. The strengthened condition prevents the inductive step from beginning with an arbitrary nonzero b, and the transition preserves both zero values. Nothing was fixed in the design between these two runs. The change is the property being proved: the additional state relationship carries information that the weaker assertion omitted.

A longer induction is an alternative to strengthening this particular property. weak_induction_depth2.ys keeps weak_ok unchanged and raises -maxsteps to two. The rerun first fails the length-one step, then proves the base case and inductive step at length two. Thus weak_ok is not inherently unprovable without an added invariant; the one-step hypothesis was insufficient.

The successful strengthened command is also part of the reproducible example.

# SPDX-License-Identifier: MIT
read_verilog -formal -sv induction.sv
prep -top induction
chformal -lower
chformal -cover -remove
sat -tempinduct -maxsteps 1 -prove strong_ok 1 -show-ports

A strengthening invariant needs justification, not wishful restriction. Here the corrected command checks the initial state because it omits -seq 1, and the same run proves preservation. The earlier command deferred the property past step one and did not establish that initial-state claim. Adding assume(b == 0) would instead constrain the environment or state space and change the meaning of the argument. The two approaches can look similar in a short successful log but leave very different obligations for the engineer who relies on the result.

Keep rejected preparation steps in the record

The initial attempt to send the assumption directly to the SAT engine was rejected with ERROR: No SAT model available for cell $assume$masked_bug.sv:9$5 ($check). That attempt produced no proof result. The HDL was retained; adding Yosys’s documented chformal -lower conversion supplied the assumption-cell representation accepted by the SAT step. The original diagnostic and the succeeding commands are both in the run record³.

A preprocessing fix should be reviewed for semantic effect. In this case lowering changes the internal representation of the assumption, while the explicit -set-assumes option still controls whether the SAT query enforces it. Removing all assumptions simply to obtain a runnable command would pose a different problem. Similarly, ignoring unsupported cells could omit the very logic under examination; none of these runs uses an ignore-unknown-cells option.

Record a timeout, an unsupported construct and an incomplete induction attempt separately from a counterexample. The tool can exit successfully after printing a failed proof search, so a shell return code alone is not a verdict parser. The bounded failure here returns a model; the weak induction attempt returns a state that defeats the induction step; the preparation error cannot produce either. Preserve those distinctions in dashboards and handoffs.

Turn a result into a bounded engineering claim

For each property, retain the source hash, elaborated top, initialization, assumption set, command, tool revision and literal outcome. Then state the claim in terms of that configuration. This page supports statements about three small two-state digital models. It supplies no analog metastability argument, environmental contract validation, timing constraint check or exhaustive inventory of the properties a larger system requires.

A completed proof still needs the right question. The masked case shows how a property can be satisfied because the environment never asks the design to do useful work. The induction example shows why a failed proof attempt need not identify a reachable defect. Read an assertion alongside its activation evidence, as in the assertion-vacuity guide, before treating a collection of successful statuses as verification closure.

Not covered on this page

• Physical timing, power, analog behavior or metastability.
• External SMT solvers, SymbiYosys orchestration or commercial formal engines.
• Validating a real system’s assumptions and reset contract.
• Proof of every requirement in an integrated design.