Yosys: a proof with no obligations always passes

A formal verification run is evidence only if the properties reach the solver. In August 2026 I found a Yosys path where they did not: write_smt2 and write_btor skipped $check cells, the cell type the Verilog frontend emits for assertions. The exported model had zero proof obligations, and any solver run on it reported PASS because there was nothing to disprove. I reported it in Yosys issue #6108. The fix, written by @Zaneham and merged in Yosys PR #6117, makes both exporters stop with an error instead.

A failing design that proved clean

The reproduction is a 4-bit counter that wraps to 15, with an assertion that it never reaches 15:

module counter(input clk, input rst, output reg [3:0] count);
    always @(posedge clk) begin
        if (rst) count <= 4'd0;
        else count <= count + 4'd1;
    end
    assert property (count != 4'd15);
endmodule

The assertion should fail. Exported after the usual prep, the SMT2 output contained no assertion at all:

yosys -p 'read_verilog -sv counter.v; prep -nordff; write_smt2 out.smt2'
grep -c 'yosys-smt2-assert' out.smt2
0

Lowering the formal cells first produced the expected obligation:

yosys -p 'read_verilog -sv counter.v; prep -nordff; async2sync; chformal -lower; write_smt2 out.smt2'
grep -c 'yosys-smt2-assert' out.smt2
1

Why nothing complained

The frontend represents SVA-style properties as $check cells. The SMT2 and BTOR backends looked only for $assert, $assume and $cover, with no branch for anything else, so a $check cell was never visited and never written. No warning was printed.

Other parts of Yosys were louder. sat -prove-asserts on the same design stops with No SAT model available for cell ... ($check). My report also listed write_smv; the fix author found that it already rejected unhandled cells. The two exporters most likely to feed an external solver were the quiet ones.

The symptom had surfaced before. Issue #4381 reported a BTOR file with no bad properties in 2024, and the advice then was to prepare designs with SBY, which runs the passes these backends expect. That advice is right for anyone using SBY. A script that called the backend directly, without those passes, got an empty proof and a PASS. The SMT2 backend's shipped example did not run them either.

The accepted fix

The change in #6117 adds four lines to each backend and a regression test for each. When write_smt2 or write_btor meets an unlowered $check cell, it now stops with an error that names the cell and says to run async2sync or clk2fflogic first. Designs prepared that way export exactly as before.

My report offered two options: handle $check directly, or refuse it. The accepted change refuses it. That makes the gap impossible to miss and leaves working flows untouched.

The same failure in AI evaluation

This is the hardware version of a pattern I study in AI evaluation: a verifier reports success on evidence it never received. An LLM judge with no verdict that is counted as a pass, and a test harness that trusts a PASSED line, fail the same way. In each case the repair is to make "nothing was checked" a different outcome from "the check succeeded".

That distinction matters more as language models write formal-verification scripts. Before this fix, a generated flow that skipped the lowering passes would have read back PASS.

Source record

This note describes the report and the accepted change. It does not claim that flows which lower $check cells before export, including SBY's, were affected.