Assertion property to check for toggle count of a signal between two control signals

SystemVerilog
, ,
11

In reply to Shubhabrata:

In reply to ben@SystemVerilog.us:

  1. Why are we considering having ack and vld as a mistake?

ap_ack_vld: assert property(@(posedge clk)  not($rose(ack) && vld)) else err3=err3+1;

If both of them are becoming 1 at the same clk-cycle , we can discard the idea of vld signal getting toggled or consider that vld got changed but we won’t count it because the question says between these two signals. So simply ignore edge ones. Why is it necessary then?

I made the consideration of not having vld && ack as an inference from your trials. I do not know your requirements, but based on experience in designs saw the req as a start of a transaction, vld as an interim handshake signifying that something was done (like received a packet, but maybe more to com) and the ack as a completion signal. Thus, it is reasonable to assume that ack follows the vld. Again, I don’t know your requirements.

2)In the first two properties you have used goto operator for $changed(vld)[->1].What is the need of this ? you could have written vld && $changed(vld) . They mean same here , as we are checking for 1 clk-cycle.

You had (vld != $past(vld) meaning that at every transition of vld (from 1 to 0, or from 0 to 1). I don’t believe you want to count the negedge(vld). I interpreted, again an inference, that you are not counting 2 sequential vlds. If that is true, you should write a separate assertion on that. vld && $changed(vld) could have been written as $rose(vld).

3)Third doubt is regarding continuous repetition.The condition you have used


((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)
// or
first_match((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2))

(vld && $changed(vld),count++) - this condition may or may not be continuous. So, why did you use * instead of = or → ?

you provided half the code. the complete code for the consequent:


first_match((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)) ##1 
    $rose(ack) && !vld [->1];

Thus, upon an occurrence of the rose(vld) I wait for an occurrence of $rose(ack) && !vld [->1] that can occur in 0 to n cycles later.

4)The following is my solution. My logic was to check if vld!=$past(vld) and then count++. This operation will happen non-consecutive way.

So at every transition of vld. vld!=$past(vld) is same as $changed(vld).
It’s OK with me; that’s your requirements; a bit odd to me!

Now in the next cycle when the ack signal will go high, we’ll check if the count>=10 or not. Another thing I added to it. When the ack is rising along with checking the count I am also displaying the count which is not getting executed. Don’t know why?


$rose(req) |=> ((vld != $past(vld),count++)[->0:$] ##1 ($rose(ack),$display("count is:%0d and time is:%0t",count,$realtime))) ##0 (count >= 2);
  • Is it not satisfying the requirement? If not then I would like to know why? Where I am getting it wrong?

(vld != past(vld),count++)[->0:] is illegal, though the tools accept it.
use (vld != past(vld)[->0:],count++)


module m;
  bit a, b, c, e, clk;
  always #5 clk=!clk;
  // 1800'2017 page 393: For example, the following is a legal sequence expression:
  //  (b[->1], v = e)[*2]
  // but the following is illegal: (b, v = e)[->2]
  property p;
    bit v;
    @(posedge clk) a |-> (b, v = e)[->2];
  endproperty
  assert property (p);
  initial #100 $finish;
endmodule