Trouble with eventual operator

[rsh...@vt.edu]

Hi,

I have a Verilog module, one of whose inputs is A, and there is a register "next_state". I am trying to verify the following property.

assert property (A |-> ##[1:$](next_state == 3'b111));

As per how my FSM works, the input A is required to be kept asserted for next_state to eventually get to 3'b111. I therefore included an "assume property " statement just to ensure that A is kept at "1", and just wish to verify if next_state eventually goes to 3'b111.

My assertion fails with the following counter-example.

Transition System State 0

A = 1

next_state = 3'b11 (011)

Transition System State 1

A = 1

next_state = 3'b111 (111)

Transition System State 2

A = 1

next_state = 3'b0 (000)

(and few more Transition states...)

Since next_state takes the appropriate value of 3'b111 at Transition state 1, what I intend to verify does happen. The assertion is however flagged as a failure. Am I missing something here? I'd really appreciate any help I can get on this.

(In case it helps, next_state is modeled as combinatorial logic inside an always@* block, with a sequential register "current_state" taking the value of next_state at every clock cycle. I'm not certain if this matters in the aforementioned assertion statement.)

Thanks,

Shashank