Quiz setup for: https://twitter.com/zipcpu/status/1033328682461478915

formal.ys

read_verilog -formal quiz_4.v
prep -top quiz_4 -nordff
opt_clean
write_smt2 -wires quiz_4.smt2

Makefile

PROJECT=quiz_4

check: $(PROJECT).smt2
        yosys-smtbmc -s z3 -t 25 --presat --dump-smt2 $(PROJECT)_bmc.smt2 --dump-vcd $(PROJECT)_bmc.vcd $(PROJECT).smt2
        yosys-smtbmc -s z3 -i -t 25 --presat --dump-smt2 $(PROJECT)_tmp.smt2 --dump-vcd $(PROJECT)_tmp.vcd $(PROJECT).smt2

$(PROJECT).smt2: $(PROJECT).v
        yosys -s formal.ys

clean::
        rm -f $(PROJECT)_*.* $(PROJECT).smt2

quiz_4.v

`default_nettype none

module quiz_4(input wire i_start_signal, input wire i_clk);

reg [5:0] counter;
initial counter = 0;

reg dummy;
initial dummy = 0;

always @(posedge i_clk)
  if ((i_start_signal)&&(counter == 0))
    counter <= 23;
  else if (counter != 0)
    counter <= counter - 1'b1;

always @(*)
    assert(counter < 24);

always @(*)
    assume(!i_start_signal);

always @(posedge i_clk) begin
    dummy <= $past(counter == 0);
    assert($past(counter == 0));
end

endmodule