write_smt2 silently drops assertions ($check cells not handled)

[john-kearney]

write_smt2, write_btor, and write_smv do not handle $check cells, which are the only cell type the Verilog frontend emits for assertions. The cells are silently dropped, producing formal output with zero proof obligations. Any solver run on the result reports PASS because there is nothing to disprove.

Found on 0.67+ (b8e7da6f40), macOS.

Reproduction

A counter that wraps to 15, with an assertion that should fail:

counter.v

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

Without chformal -lower (assertion silently dropped):

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

Output: 0

With chformal -lower (assertion correctly emitted):

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

Output: 1

The inconsistency is visible with sat too. The sat command fails loudly on $check:

yosys -p 'read_verilog -sv counter.v; prep -nordff; sat -prove-asserts'

Output: ERROR: No SAT model available for cell $assert$counter.v:5$3 ($check).

Expected behavior

write_smt2 should either handle $check cells directly (dispatching on the FLAVOR parameter to assert/assume/cover) or emit a warning/error when it encounters a $check cell it does not handle. As it stands, write_smt2 produces a proof artifact with no obligations, and a solver run on it will report PASS unconditionally.

Actual behavior

write_smt2 emits zero proof obligations. No warning. The SMT2 output does not contain main_a or any yosys-smt2-assert annotation. A solver run on this file would report PASS unconditionally.

Cause

The frontend emits $check for all assertions (frontends/ast/genrtlil.cc:876, 919, 2095, 2120). The SMT2 backend only matches $assert/$assume/$cover (backends/smt2/smt2.cc:1110). Same for backends/btor/btor.cc and backends/smv/smv.cc - none reference $check.

prep does not lower $check to $assert. The workaround is to run async2sync; chformal -lower before write_smt2, but the shipped example (backends/smt2/example.ys) does not do this.

Workaround

Run async2sync; chformal -lower (or clk2fflogic; chformal -lower) before write_smt2 / write_btor / write_smv.