| Login | | Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. | |
| Who's Online | There are currently, 47 guest(s) and 0 member(s) that are online.
You are Anonymous user. You can register for free by clicking here | |
 | |
|
Verification Guild: Forums |
|
| View previous topic :: View next topic |
| Author |
Message |
tzar
Senior
Joined: Nov 28, 2007
Posts: 69
|
 Posted: Mon Mar 12, 2012 5:02 am Post subject: Help in understanding an assertion |
 |
|
Hi all,
I have no doubt that this is a classic gotcha I have fallen into but I am falling to understand the way the following assertion works:
| Code: |
property pTEST;
@(posedge CLK)
$rose(A) |-> ##[0:$]$rose(B) ##4 $rose(C);
endproperty
aTEST: assert property(pTEST);
|
What I was hoping this assertion would do was, after the rising edge on A, it would check for the 1st rising edge on B and the make sure that 4 cycles after B that C occurred. The assertion works fine (passes) if this occurs but does not fail if B is not followed by C. What actually happens if C does not follow B is that it waits for the next occurrence of B, checks if C occurs after that, if not it waits for the next occurrence of B and checks for C after than, and so on. That is, the assertion never fails.
I have no doubt that this is expected behavior but I would like to understand why as intuitively I think the assertion looks correct.
Just to note that I have rewritten the assertion as follows which does do what I require:
| Code: |
property pTEST;
@(posedge CLK)
$rose(A) |-> !B[*0:$] ##1 B ##4 $rose(C);
endproperty
aTEST: assert property(pTEST);
|
Thank all. |
|
| Back to top |
|
 |
vhdlcohen
Industry Expert
Joined: Jan 05, 2004
Posts: 1240
Location: Los Angeles, CA
|
| Posted: Mon Mar 12, 2012 9:56 am Post subject: |
|
|
| Quote: | | but I would like to understand why as intuitively I think the assertion looks correct. |
a |-> ##[0:$] seq; // seq is some sequence
is same as
a |-> (##0 seq) or (##1 seq) or (##2 seq) or .... (##n seq);
// where n is infinity, and "or" is the sequence or operator.
the a |-> b[->1] ##4 c; // is the same as your solution where you're looking for the first occurrence of b and then 4 cycles later b. That can fail if b occurs.
_________________
Ben Cohen http://www.systemverilog.us/
* SystemVerilog Assertions Handbook, 3rd Edition, 2013
* A Pragmatic Approach to VMM Adoption
* Using PSL/SUGAR ... 2nd Edition
* Real Chip Design and Verification
* Cmpt Design by Example
* VHDL books |
|
| Back to top |
|
|
tzar
Senior
Joined: Nov 28, 2007
Posts: 69
|
| Posted: Mon Mar 12, 2012 11:17 am Post subject: |
|
|
| Ah, now it makes sense. Perfect and simple explanation. Thanks. |
|
| Back to top |
|
|
|
|
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
| |
|
|
Forum FAQ
Search
Usergroups
Profile
Digest
Log in
