async2sync fails on check cells with async reset

[georgerennie]

Version

Yosys 0.49+3 (git sha1 9d46304, g++ 14.2.1 -fPIC -O3)

On which OS did this happen?

Linux

Reproduction Steps

The following SBY file declares an assertion that should only be triggered when rst_n is high within a block triggered asynchronously by posedge clk and negedge rst_n. This should be supported in multiclock off mode as async2sync should be able to handle a single async reset, converting it to a sync reset.

[options]
mode bmc

[engines]
smtbmc

[script]
read -sv test.sv
prep -top top

[file test.sv]
module top(input wire clk);
	always_ff @(posedge clk or negedge rst_n) begin
		if (rst_n) begin
			assert(1'b1);
		end
	end
endmodule

Expected Behavior

SBY/Yosys accept the design and the proof passes. This happens fine with 9f27923, a commit from just before $check cells were added. Although I haven't bisected to determine exactly when this issue was introduced, I assume its with $check cells as they are not able to be lowered correctly in this case.

Actual Behavior

SBY reports an error from async2sync:

ERROR: $check cell _witness_.check_assert_test_sv_4_2 with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic.

This is because the trigger input is {rst_n, clk}. It would be good to be able to support this case otherwise embedding assertions within async reset blocks is broken.