opt_merge merges $assert cells

[KrystalDelusion]

Version

0.38+129

On which OS did this happen?

Linux

Reproduction Steps

Run script:

read_verilog -sv << EOF
module top (...);
input clk, a;
always @(posedge clk) begin
    assert_a1: assert (a);
    assert_a2: assert (a == 1);
end
endmodule
EOF

hierarchy
proc
async2sync
select -count t:$assert
opt_merge
select -assert-count 2 t:$assert

Expected Behavior

Script should pass, retaining both assert cells (even if they end up being identical).

Actual Behavior

Script merges assert cells, leaving only assert_a1 and select -assert_count fails.

When async2sync converts the check cells to assert cells they lose the 'keep' attribute, and while opt_clean checks if (cell->type.in(ID($assert), ...)), opt_merge only checks if (cell->has_keep_attr()).

[KrystalDelusion]

Discovered while testing the SBY fifo example where the aig flow merges the following assertions during a call to opt -full:

a_oflow2: assert (waddr < MAX_DATA);
a_full:  assert (!full || count == MAX_DATA);

The btor and smt2 flows don't call opt -full and retain both assertions while the aig flow drops a_oflow2.