yosys/tests/verilog/unreachable_case_sign.ys

logger -expect-no-warnings

read_verilog -formal <<EOT
module top(input clk);
    reg good = 0;

    always @(posedge clk) begin
        case (4'sb1111) 15: good = 1; 4'b0000: ; endcase
        assert (good);
    end
endmodule
EOT

prep -top top
async2sync
sim -n 3 -clock clk

design -reset

read_verilog -formal <<EOT
module top(input clk);
    reg good = 1;
    reg signed [1:0] case_value = -1;

    always @(posedge clk) begin
        case (4'sb1111) 4'b0000: ; case_value: good = 0; endcase
        assert (good);
    end
endmodule
EOT

prep -top top
async2sync
sim -n 3 -clock clk