I am trying to write assertion for the following requirement,
When req is asserted, ack should follow within 10 cycles and ack should go low next clock cycle and stay low for the rest of the time
Thanks Ben. This is very helpful.
According to this, “Assertion of this property terminates, when antecedent matches and one of the consequent threads match”. In that case, technically below assertion will terminate if ack stays low for 1 or 2 or 3 or 4… cycles right. How does it make sure that ack stays low for rest of the simulation. Example: A scenario where ack stayed low for 2 cycles, and then went high in 3rd cycle. But assertion would have terminated. Is it because there is no expression after !ack[*1:] in this case?
// after the ack, you always after every cycle need the !ack
a_p2: assert property(
@(posedge clk) disable iff (!rst_n)
$rose(req)|->##[1:10]ack #=# always @(posedge clk) !ack);
Thanks for the explanation . This makes sense. Last question, is it all right to use |=> in place of #=# ?
// You are suggesting changing this:
$rose(req)|->##[1:10]ack #=# always @(posedge clk) !ack);
// To
$rose(req)|->##[1:10]ack |=> always @(posedge clk) !ack);
// The issues here are VACUITY and meeting requirements
// If ack==0 for all 10 cycles, then the assertion is vacuously true.
The followed-by operator in the consequent concatenates a sequence and a property.
In this example, if ack==0 for all 10 cycles then the assertion fails.
In reply to Yuankun:
The reason I initially used the always @(posedge clk) !ack is because I was not sure without doing some 1800 research of the clock flows through from the sequence to the property, so I took the safe mode.
Many many years ago, when I was learning VHDL, I had lots of syntax/legality questions. Finally, my mentor got fed up with me and said the following:
If you are in doubt about what is legal or illegal, write a test code and simulate it.
I can assure you, the simulator tool knows the LRM much better than you.
:)
Here, I followed that advice instead of digging into 1800, and the answer is YES.
The clock does flow through from the sequence to the followed-by property
$rose(req)|->##[1:10]ack #=# always !ack); // WORKS OK, IS LRGAL
Will the above solutions work if requests come in back to back. In the case of back to back requests, the $rose will not fire for the 2nd request, correct ?
In reply to ben@SystemVerilog.us:
Hi Ben,
Will the above solutions work if requests come in back to back. In the case of back to back requests, the $rose will not fire for the 2nd request, correct ?
If signal “a” is the sequence 0 0 1 1 1 0 1 1
All attempts where a==0 are vacuous.
In the above sequence you have 2 $rose(a) and with each of them a successful attempt.
I went through the paper that you mentioned above. Thanks for the detailed explanation on what happens underneath the hood for multiple threads.
I do want to specifically bring up the last 2 examples that you specified in this paper :
(1) first_match operator :
first_match(rose(a) ##[1:] b) |-> ##3 c;
(2) Goto operator
$rose(a) ##1 b[->1]) |-> ##3 c; // Use the goto operator
I want to explore the use of the above for this simple case : “Write an assertion for a transaction where a request is followed by an ack in 1-3 cycles”. Now if I use the same style solution as above :
$rose(req)|->##[1:3]ack
If my requests on each posedge are in the order you specified :
Posedge# Req Ack Comment
Posedge0 0 0
Posedge1 1 0 Request#1
Posedge2 1 0 Request#2
Posedge3 1 1 Request#3 and Ack for Req #1. But this ack will satisfy #Request2 too !!!.. How do you filter this out ? Using the first_match operator ?
Posedge4 0 1 Ack for Req #2
Posedge5 1 1 Ack for Req #3
Posedge6 1 1 Ack for Req #4
Posedge7 0 1 Ack for Req #5
My concern again is that the above assertion will fire for the 1st posedge and 5th posedge only and won’t fire for the other requests.
Now, if I were to rewrite this assertion as follows : Level sensitive ( not really ideal because of performance issues)
req |-> ##[1:3]ack
Here, I would fire a thread each time request was high, but then if you look at posedge #3, how do I avoid NOT counting the ack for request#1 towards request #2 ? Do I use the first_match operator here ? Should I rewrite it like this :
first_match(req |-> ##[1:3]ack)
Can you please clarify ? Sorry if this has already been addressed in other threads in this forum. I did search to see if I could find a similar discussion, but I could not find it.
Thanks Ben. That one nails it. I am so frustrated that this solution ( using the power of a local variable) eluded me this past week. But this solution you mentioned -
It does open up a new concept for me - that I can bundle up function calls in an antecedent too… I never thought we could do this. But now that I see it, it of course makes sense.