yosys/tests/verilog/past_signedness.ys

logger -expect-no-warnings

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

    always @(posedge clk) begin
        if (ready)
            assert ($past(value) == -1);
        ready <= 1;
    end
endmodule
EOT

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

design -reset

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

    always @(posedge clk) begin
        if (ready)
            assert ($past(value + 4'b0000) == 15);
        ready <= 1;
    end
endmodule
EOT

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