| 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, 56 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 |
SAHO
Senior
Joined: Oct 16, 2004
Posts: 24
|
 Posted: Sat Nov 06, 2004 8:18 pm Post subject: About PSL/Sugar for Formal and Dynamic Verification,2nd |
 |
|
hello PSL/Assertion guru:
Reading the text PSL/Sugar for Formal and Dynamic Verification,2nd, I got contradicting explanation on PSL construct.
I am using the the exact wordings taken from the book.
| Quote: | On page 43, it states that
The assertion
has the following behaviour
if a is TRUE, b will be checked.
if b is also TRUE, the assertion HOLDS.
if b is FALSE, the assertion FAILS.
if a is FALSE, the assertions HOLDS.
On page 67, it states that
| Code: | -- psl property ALWAYS_ABC is
-- always a -> next b -> next c Property 1
-- property p1 is
-- always {a;b;c}; Property 2
Property 1 is equivalent to Property 2. |
For these assertions not to fail, a must be true in the first in the first cycle in the simulation, b in the second and c in the third. |
Reading Cindy's posting (http://www.verificationguild.com/modules.php?name=Forums&file=viewtopic&t=543) suggests that Property 1 and Property 2 are DIFFERENT.
| Quote: | cindy
Senior
Joined: Aug 17, 2004
Posts: 28
Posted: Thu Sep 23, 2004 11:11 pm Post subject:
--------------------------------------------------------------------------------
alex,
Quote:
In you first example, the sequence was:
{ a ; b[*] ; c } ;
and the property: ( { a ; b[*] ; c } |=> { d } );
However, you also can expess this property as a sequence too, such as :
{ a ; b[*] ; c ; d} ; and use "assert always" right on this sequence.
this is incorrect. the two are not equivalent. let's examine them one by one. the property
Code:
{ a ; b[*] ; c } |=> { d } (property 200)
states that if "a" is asserted at the first cycle (note there is no always operator modifying the whole thing), and if "c" is asserted at some future time, and if "b" is asserted between the assertions of "a" and "c", then "d" is asserted the cycle after "c" is asserted.
if we put an "always" around it, like this:
Code:
always ({ a ; b[*] ; c } |=> { d }) (property 201)
then we get the same thing, except that the assertion of "a" does not have to be at the first cycle - any sequence of cycles such that "a" is asserted, "c" is asserted sometime after that, and "b" is asserted at all cycles in between will require that "d" be asserted the cycle after "c".
both properties 200 and 201 are different than this next:
Code:
always { a ; b[*] ; c ; d} (property 202)
property 202 states that at every cycle we must see the start of a sequence in which "a" is asserted, then "b" is asserted for some number of cycles, then "c" is asserted and then "d". in particular, "a" must be asserted at the first cycle, at the second cycle, at the third cycle, etc. etc. what is missing from property 202 is the if-then that you get with a suffix implication as in properties 200 and 201. this is why i said previously that a property of the form "always sequence" is not very useful.
hope that clears things up.
cindy. |
From explanation developed on page 43, Property 1 SHOULD have this behaviour (per every clocked cycle).
if a is TRUE, b will be checked.
if b is also TRUE, c will be checked.
if c is also TRUE, the assertion HOLDS (completes)
if c is FALSE, the assertion FAILS (completes)
if b is FALSE, the assertion HOLD (incompletes) .
if a is FALSE, the assertions HOLDS (incompletes) .
But, Property 2 requires that
a must be true in the first in the first cycle in the simulation, b in the second and c in the third
Please comment on this.
SAHO |
|
| Back to top |
|
 |
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Sun Nov 07, 2004 3:05 am Post subject: |
|
|
saho,
as one of the co-developers of the psl formal semantics, i am in a position to state categorically that your interpretation based on the text on page 43 is correct, and the statement on page 67 is wrong.
cindy. |
|
| Back to top |
|
|
SAHO
Senior
Joined: Oct 16, 2004
Posts: 24
|
| Posted: Sun Nov 07, 2004 7:02 am Post subject: |
|
|
Cindy:
Thank you for your reply. I am getting better with my PSL construct s' understanding  . I am finding some PSL properties expression can be mind boggling and hard to comprehend  .
I would like to suggest to Ben Cohen, Srini and Ajeetha to incorporate this errate on this website.
Have a nice day. I am learning more PSL construct each day.
SAHO |
|
| Back to top |
|
|
srini
Senior
Joined: Jan 23, 2004
Posts: 430
Location: Bengaluru, India
|
| Posted: Sun Nov 07, 2004 11:34 am Post subject: |
|
|
| SAHO wrote: | Cindy:
Thank you for your reply. I am getting better with my PSL construct s' understanding . I am finding some PSL properties expression can be mind boggling and hard to comprehend .
I would like to suggest to Ben Cohen, Srini and Ajeetha to incorporate this errate on this website.
Have a nice day. I am learning more PSL construct each day.
SAHO |
Hi Saho & Cindy,
Thanks for finding this "bug" - agreed it is an error and our errata will be appended soon.
Thanks and Regards,
Srinivasan
_________________
Srinivasan Venkataramanan
Chief Technology Officer, CVC www.cvcblr.com
A Pragmatic Approach to VMM Adoption
SystemVerilog Assertions Handbook
Using PSL/SUGAR 2nd Edition.
Contributor: The functional verification of electronic systems |
|
| Back to top |
|
|
vhdlcohen
Industry Expert
Joined: Jan 05, 2004
Posts: 1238
Location: Los Angeles, CA
|
| Posted: Sun Nov 07, 2004 2:02 pm Post subject: |
|
|
The following site has a list of the new errata for the book
Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004 isbn 0-9705394-6-0
http://members.cox.net/vhdlcohen/errata.pdf
also at front page http://www.abv-psl.org/
I would like to congratulate SAHO for delving into the book, and really demonstrating that he is understanding PSL.
I can say that the error was put in "on purpose" so that people get puzzled, and really get confused enough enough to really understand the language.
After all, our President does NOT admit to any error! He just puts spins on any mistakes 
Of course, that would be a lie. We did make some errors, and I apologize. Actually, most authors will honestly tell you that they make mistakes.
We are trying very very hard to minimize those mistakes, and our next upcoming SVA book (due late this month) went thru several iterations, revisions, and reviews and hopefully will have fewer errors.
Cindy may disagree with me on this, but on PSL I recommend to avoid non-SERE properties, and to stick to SEREs instead for the following reasons:
* A property may easily be updated to a sequence as the requirements change. For example:
| Code: |
instead of always (ready -> next req -> next ack)
use always {ready; req} |=> {ack};
If the problem changes to after a ack, wait until a done after 16 cycles, then this can be updated to:
always {ready; req} |=> {ack; [*16]; done};
|
* Easier translation to SVA, if that ever becomes necessary.
* A simpler subset to maintain.
Note that SVA got away from this idea of non-SEREs, and everything is a SERE, thus eliminating the need for the {{{{...}}}}
In SVA, for those interested, the above property can be expressed as:
| Code: | property pHandshake;
@ (posedge clk) disable iff (!reset_n)
ready ##1 req |=> ack ##17 done;
endproperty : pHandshake |
_________________
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 |
|
|
SAHO
Senior
Joined: Oct 16, 2004
Posts: 24
|
| Posted: Sun Nov 07, 2004 5:26 pm Post subject: You are thoughtful |
|
|
hello Ben, Srini:
First of all, I MUST congratulate you in composing such a great book to read on PSL. I have gain tons of working knownledge of PSL, simply reading and "delving" into the PSL expressions used in the book. To me, PSL is very very RICH and can take long time to master it. Having said that, once the working mechanism of PSL is understood (sampling point, boolean operator, temporal operator, and verification operator), one can "easily" write and understand PSL construct rather fast.
I am still a newbie in this field; been using mainly VHDL most of the time. The main reason in learning a new language (i.e., PSL) is to enable me to target our verification bottleneck, simply assisting engineers to locate the errors at/near the root.
Should I find more potential "bugs" in your book, I will raise it for discussion.
Thank you for your thoughfulness. You have been great teachers.
SAHO |
|
| Back to top |
|
|
|
|
You can post new topics in this forum
You can 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
