SV Assertions using $past()

SystemVerilog
,
1

I’ve this question. Please advise SV and SV experts.
I wanted to ask you a conceptual question on SVA that I’m facing.

The question is to write SVA for T FF with no reset or preset.

My approach:

property toggle_cond;

 @(posedge clk) t |=> q == ~($past(q, 1));

enproperty

property no_change;

 @(posedge clk)  (t==0) |=> q == $past(q, 1));

enproperty

NC : assert property(no_change);

NC1: assert property(toggle_cond);

I find my solution is correct, but when I check on Gemini/ChatGPT, it is saying that its incorrect. This is because Don’t use |=> and $past() in the same expression for simple flip-flop logic. It makes the code harder to debug.

According to my understanding of SVA fundamentals,
When t is LOW (ANTECEDENT is TRUE), then in the next clock cycle, check the CONSEQUENT where Q_next is complement of the Q_current. Isn’t this how we test T-FF functionality? Please correct me if I’m mistaken and there might be gap in my knowledge.

As per GPT it is suggesting I should use, overlapping operator. But, will it change the very definition of T-FF?

Please advise and correct me.

Thank you

2

I don’t see any issue with your code.

The only addition that I would do is to check that current and previous values aren’t X / Z

Note that the 2nd argument to $past has default value of 1.

So $past(q,1) and $past(q) are essentially the same

3

ChatGPT isn’t giving you absolutely correct advice. A |=> B is functionally equivalent to A |-> ##1 B. They’re not functionally equivalent without the 1 cycle delay.

The widely accepted recommendation is to use only the overlapping implication |-> to avoid any confusion.