yosys/tests/verilog/sign_array_query.ys

logger -expect-no-warnings

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

    always @(posedge clk) begin
        case ($left(x) + zero) 36'shfffffffff: good = 1; 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 [-1:-1] x;
    reg good = 0;

    always @(posedge clk) begin
        case ($left(x)) 36'sh0ffffffff: good = 1; (32'h0 + $left(good)): ; 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 [-1:-1] x;
    reg good = 1;

    always @(posedge clk) begin
        case (36'sh100000000 + $left(x)) -1: good = 0; endcase
        assert (good);
    end
endmodule
EOT

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