counterexample

[Fuhj-better]

Hello,
I've encountered a rather peculiar issue. According to the code logic, when reset is set to 1, start_count, counter, start_count_del, and tx_ack should all be set to 0. However, the counterexample provided does not reflect this. Instead, it shows values that do not align with the code logic, leading to the assertion failure. I am quite puzzled as to why this is happening.
Here is the code:
ack_counter.zip

And here is the counterexample:

** Results:
[ack_counter.assert.1] always (ack_counter.reset == 1'b1 |-> ack_counter.counter >= 0 && ack_counter.counter <= ack_counter.max_count): REFUTED
Counterexample:

Transition system state 0
----------------------------------------------------
  ack_counter.clock = ?
  ack_counter.reset = 0
  ack_counter.ready = 0
  ack_counter.tx_start = 0
  ack_counter.max_count = 16'hFFFF (1111111111111111)
  ack_counter.tx_ack = ?
  ack_counter.start_count = 1
  ack_counter.start_count_del = 0
  ack_counter.counter = 0 (0000000000000000)

Transition system state 1
----------------------------------------------------
  ack_counter.clock = ?
  ack_counter.reset = 1
  ack_counter.ready = 0
  ack_counter.tx_start = 0
  ack_counter.max_count = 0 (0000000000000000)
  ack_counter.tx_ack = 0
  ack_counter.start_count = 0
  ack_counter.start_count_del = 1
  ack_counter.counter = 1 (0000000000000001)

Thank you for your help!

[kroening]

You are seeing the state before the first clock edge.

Either use initial to constrain that state, or disable iff to disable the check.

[kroening]

Or simply write |=> instead of |->.