I need to write a property to check for a signal valid toggling between req and ack for atleast 10 cycles(not consecutively). The actual number of toggle varies per request so we can not constraint it. I tried following property but it doesn’t finish and report pass or fail at the end of simulation.
(vld[=2] ##[1:$] rose(ack)); // is same as
!vld[*0:] ##1 vld ##1 !vld[*0:] ##1 vld ##1 !vld[*0:] ##[1:$] rose(ack)
I am puzzled on (vld[=2] ##[1:] $rose(ack)) because it should fail with 3 vld before ack.
I’ll work on this with my full version of the simulator (rather than the eda version).
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
The comments in the code below explain why
THUS: vld[=2] ##[1:$] rose(ack))) is equivalent to
vld[->2] ##[1:] $rose(ack))) */
// 2 vld between req ack
module m;
bit clk, vld, req, ack, rst_n=1;
int count=2, pass1, pass2, pass3,pass4, pass5, err1, err2, err3, err4, err5;
initial forever #10 clk = !clk;
// number of vld is dynamic
property vld_tog_chk (req, ack, vld, count);
int v;
@(posedge clk) disable iff (!rst_n)
##1 ($rose(req), v=count) |-> //( //strong(
first_match((vld[->1], v=v-1)[*1:$] ##1 !vld[*1:$] ##0 $rose(ack)) ##0 v>=0;
endproperty: vld_tog_chk
ap_vld_tog_chk: assert property(vld_tog_chk(req, ack, vld, count)) pass1=pass1+1; else err1=err1+1;
// Correctly using the Non-consecutive repetition, Boolean [=n]
ap_vldack_ok: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong( says after 2 vld an ack
(vld[=2] ##1 $rose(ack)) ##0 !vld)) pass2=pass2+1; else err2=err2+1;
// Correctly using the goto, Boolean [->n]
ap_vldack_ok2: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong( says after 2 vld an ack
first_match(vld[->2] ##1 !vld[*1:$] ##1 $rose(ack)) ##0 !vld)) pass3=pass3+1; else err3=err3+1;
// Incorrectly using the Non-consecutive repetition, Boolean [=n]
ap_vldack_bad: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong(
vld[=2] ##[1:$] $rose(ack))) pass4=pass4+1; else err4=err4+1;
// Equivalencey to the Non-consecutive repetition, Boolean [=n]
ap_vldack_bad_equiv: assert property(@(posedge clk) disable iff (!rst_n)
##1 $rose(req) |-> ( //strong(
vld[->2] ##1 !vld[*0:$] ##[1:$] $rose(ack))) pass5=pass5+1; else err5=err5+1;
// consequent is equivalent to
/* vld[->2] ##1 !vld[*0] ##[1:$] $rose(ack) or // Thread1
vld[->2] ##1 !vld[*1] ##[1:$] $rose(ack) or ...
Considering thread1 only, the assertion will will be satisfied (a pass) with the sequence
... vld ... vld .. ... %rose(ack) // because
vld[->2] ##1 !vld[*0:$] ##[1:$] $rose(ack) // is same as
vld[->2] ##1 !vld[*0] ##1 $rose(ack) or // <<<---- ThIS THREAD
vld[->2] ##1 !vld[*0] ##2 $rose(ack) ##1 $rose(ack) or
..
// Consider just THIS THREAD
vld[->2] ##1 !vld[*0] ##1 $rose(ack) // it simplies to just
vld[->2] ##1 $rose(ack) // thus,
Two vld (the vld[->2]) folowed $rose(ack) satifies the consiquent
THUS: vld[=2] ##[1:$] $rose(ack))) is equivalent to
vld[->2] ##[1:$] $rose(ack))) */
initial begin :init1
$dumpfile("dump.vcd"); $dumpvars;
repeat (1) @(posedge clk);
req <= 1'b1;
repeat(2) begin :rpt1
@(posedge clk);
vld<= 1; req<=0; ack <=0;
@(posedge clk);
vld<= 0; req<=0;
repeat(2) @(posedge clk);
end :rpt1
ack <=1;
@(posedge clk) req<=1; ack<=0;
repeat(3) begin
@(posedge clk);
vld<= 1; req<=0; ack <=0;
@(posedge clk);
vld<= 0; req<=0;
repeat(2) @(posedge clk);
end
ack <=1;
repeat(2) @(posedge clk);
$finish;
end
endmodule
In reply to ben@SystemVerilog.us:
A very useful comment by a colleague who particularly does not like the use of the first_match.
Ben, providing a solution with parameterized number vld is a good idea, but not using first_match. I recommended not using it previously. Even PSL does not have the operator. It’s implementation is costly and in formal may not be supported.
The consequent w/o first_match might look like this:
(vld[->1] ##0 (v>0, v=v-1))[*1:] ##1 !vld[*1:] ##0 $rose(ack) ;
Thanks for providing the detailed solution, I tested the model for valid cycles less than 2 or 0 and none of the assertions are reporting failure. The relationship requirement between these 3 signals were that vld must occur atleast 10 (or 2 in your model) times between req and ack. To satisfy this I used the strong in consequent but it doesn’t work as expected. Can you please help on how to solve this?
vld must occur at least 10 (or 2 in your model) times between req and ack.
// v is initialized to a max count; let count==2 as an example
(vld[->1] ##0 (v>0, v=v-1))[*1:$] ##1 !vld[*1:$] ##0 $rose(ack);
// passes if 1 vld then an ack, or 2 non-sequential vld then ack,
// fails if 3 vld in any order before an ack .
// At every vld, v=v-1. Two sequential vld followed by a $rose(ack) do not make a pass.
// vld 0 0 1 0 0 x
// ack x x x 0 1 <--- PASS here
//
// vld 0 0 1 1 0 x
// ack x x x 0 <-- FAIL here, v is decremented by 2
// other threads are still tested until v<0
If you want vld must occur at least 2 in my model, between req and ack.
you’ll need to tune the conditions. Also, making a requirement that ack and vld are not in the same cycle.
See my next reply that is a modification to your approach
module m;
bit clk, vld, req, ack, rst_n=1;
int err1, err2, pass1, pass2;
initial forever #10 clk = !clk;
property p1; // need 2 or more vld in this example
int count = 0;
@(posedge clk) disable iff(!rst_n)
$rose(req) |=>
((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)##1
$rose(ack) && !vld [->1] );
endproperty
assert property (p1) pass1=pass1+1; else err1=err1+1;
// Above assertion misses the condition of a ack and a vld in the same cycle
// particularly if this should be an error
// The following des check for this.
// I don;t think you need the first_match here
// but I believe the simulator will not try the other threads
property p2;
int count = 0;
@(posedge clk) disable iff(!rst_n)
$rose(req) |=>
first_match((vld && $changed(vld)[->1],count++)[*1:$] ##0 (count >= 2)) ##1
$rose(ack) && !vld [->1];
endproperty
assert property (p2) pass2=pass2+1; else err2=err2+1;
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?
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.
3)Third doubt is regarding continuous repetition.The condition you have used
(vld && $changed(vld),count++) - this condition may or may not be continuous. So, why did you use * instead of = or → ?
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. 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?
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
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
Hi Ben,
Thank you so much. Finally, it’s clear. Few things I misunderstood. That changed[->1] then [+] or [*1:].
Now coming to my logic I used (vld!=$past(vld) , count++) because the question is related to toggling and I thought it would be 1->0 and 0->1 both. This expression is equivalent to $changed(vld) , yeah true. I totally forgot about it. And the last thing regarding illegal attempts.On that thing, I missed out. Thanks for mentioning here.
I believe, most appropriate way would be -
property p1;
@(posedge clk)disable iff(!rst_n)
$rose(req) |=>(vld != $past(vld)[->1],count++)[*] ##1 ($rose(ack),$display("count is:%0d and time is:%0t",count,$realtime))) ##0 (count >= 2);
// [*] is equal to [*0:$] : I've seen it somewhere.
// I saw somewhere that b[->2:$] = (b[->1])[*2:$] or (!b[*] ##1 b)[*2:$].
// I read somewhere that in case of "=" and "->" minimum number would 1.We cannot do a[->0:$].
// I don't see the impossibility.Cause this one says (a[->1])[*] or (!a[*] ##1 a)[*].This is possible , right ?????
endproperty