Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Register Log in

Help me understand verification in PSL

Status
Not open for further replies.
salma ali bakr

salma ali bakr

Advanced Member level 3
Advanced Member level 3
Joined
Jan 27, 2006
Messages
969
Helped
104
Reputation
206
Reaction score
21
Trophy points
1,298
Activity points
7,491
verification Q (PSL)

i'm reading in a tutorial now and there is something confusing me:

a property is as follows:

ERROR must not be asserted between an END and the following START ( from one cycle after the END until one cycle after the START )

and it's written as follows in PSL:
assert always (END -> next ( START before ERROR ) );

but i don't think it's written correctly, cause this description doesn't imply the fact of "from one cycle after the END until one cycle after the START"

can anyone explain this for me please???

thanks,
Salma:)
 

Re: verification Q (PSL)

In this forum itself there is member by name aji_vlsi her name being Ajeetha Kumaari ..........


just ask her .......she has written a book on PSL............


good luck
 
Re: verification Q (PSL)

Hi,

salma ali bakr said:
i'm reading in a tutorial now and there is something confusing me:

a property is as follows:

ERROR must not be asserted between an END and the following START ( from one cycle after the END until one cycle after the START )

and it's written as follows in PSL:
Code: 
assert always (END -> next ( START before ERROR ) );
Click to expand...

Why do you think it doesn't capture it? Looks to me like it does, I hope this is a clocked property. One way to understand the above PSL code is:

Code: 
 always (END ->

After END is seen,

Code: 
 next

From the NEXT clock cycle onwards

Code: 
 ( START before ERROR ) );

Guarantee that I see a START BEFORE the ERROR signal.

but i don't think it's written correctly, cause this description doesn't imply the fact of "from one cycle after the END until one cycle after the START"

can anyone explain this for me please???

thanks,
Salma:)
Click to expand...

I believe part of the problem is natural languages such as English (or any other) is ambiguous and can be left to interpretation, This is really where PSL/SVA is proving very very beneficial. There are chances that the above PSL code doesn't comply to your requirement, that's due to the vague description in English than the PSL itself.

This is really where simulating with traces help - create those traces where you believe this PSL code does NOT work as expected, then we can help you arrive at correct PSL Code. Not just via English description.

Also, explore formal tools to provide traces - such as Magellan (www.synopsys.com) or IFV (cadence.com), Averant's Solidify etc. can all generate traces for your PSL code thereby eliminating the need for you to write testbench.

HTH
Ajeetha, CVC
www.noveldv.com
 
Re: verification Q (PSL)

Thanks alot :)

Surely you are right about the confusion in the interpretation from english to PSL, also the writing of the english specification itself can be misleading and vague, and depending on each engineer's analysis.

for instance, in this example, I think they meant "look for (start before error) one cycle after end" , which would be written in spec as ((from one cycle after the end)) and thus eliminating (( and one cycle after the start ))

Well, about applying the sense of True implies True and False implies both True and False (when testing properties), can you make it more clear for me please ?

Thanks,
Salma :)
 

Re: verification Q (PSL)

salma ali bakr said:
Thanks alot :)

Well, about applying the sense of True implies True and False implies both True and False (when testing properties), can you make it more clear for me please ?

Thanks,
Salma :)
Click to expand...

Amazingly confusing line in English, sorry to say. You need to make it more clear before I can help

Ajeetha, CVC
www.noveldv.com
 

Re: verification Q (PSL)

hehe, sorry

it's just somehow allllll confusing :)

i wanted to understand more the sense of the directions in a property
the enabling condition (LHS) and the fulfilling condition (RHS)
True for LHS means True for RHS
but False for LHS means True or False for RHS

i hope it's more clear now :)
if not, then there is something i'm missing

Salma
 

Re: verification Q (PSL)

salma ali bakr said:
hehe, sorry

it's just somehow allllll confusing :)

i wanted to understand more the sense of the directions in a property
the enabling condition (LHS) and the fulfilling condition (RHS)
True for LHS means True for RHS
but False for LHS means True or False for RHS

i hope it's more clear now :)
if not, then there is something i'm missing

Salma
Click to expand...

I believe you are referring to the "Implication operator" and the "vacuity" associated with it. PSL/SVA has impleication operator that has a form:

LHS |-> RHS

This says "if LHS is true, check that RHS is also true" (LHS & RHS can be temporal sequences as well, not just booleans). Now the question is "what is LHS is not true"? In that case - we can't declare a failure b'cos the spec says "if LHS then..", at the same time it is not a true pass/success either. Such a condition is called "Vacuous success". We have good examples of it in our PSL & SVA books, see www.noveldv.com for "Latest Books" section.

HTH
Ajeetha, CVC
www.noveldv.com
 
Re: verification Q (PSL)

well, i was just confused regarding the truth table of "implies" or ->

if we say A->B
the truth table is:
A B A->B
-----------------------
F F T
F T T
T F F
T T T

So I just didn't get the idea of having A->B as True, when A is false
i guess it's said: the property is True trivially :)
isn't this right?

but if the property is true, how will we be sure that it's trivially true or actually true?

Regards,
Salma:)
(thanks for the link)
 

Re: verification Q (PSL)

salma ali bakr said:
well, i was just confused regarding the truth table of "implies" or ->

if we say A->B
the truth table is:
A B A->B
-----------------------
F F T
F T T
T F F
T T T

So I just didn't get the idea of having A->B as True, when A is false
i guess it's said: the property is True trivially :)
isn't this right?

but if the property is true, how will we be sure that it's trivially true or actually true?
Click to expand...

This is precisely what a "vacuous success" is. Do you have a simulator say NC/MTI/VCS? Read in their docuemntation. VCS has a run time option to filter these vacuous success.

simv -assert filter

HTH
Ajeetha, CVC
www.noveldv.com
Regards,
Salma:)
(thanks for the link)[/quote]
 
Re: verification Q (PSL)

hi aji_vlsi,

i'm very thankful for your replies
they helped me alot
also the page of noveldv is veryyy useful
thanks alot

i just want to be clear on something
i'm a bit confused about the types of functional verification
can we say there is static and dynamic verification
or is it simulation based, assertion based and formal
where does formal verification lie exactly
i'm just a bit confused about the hierarchy of everything :)
is there something i can read that tells this in short and brief
cause i've tried some books but nothing is showing this issue directly in simple words

thanks alot again
Salma :)
 

Re: verification Q (PSL)

Hi,

salma ali bakr said:
hi aji_vlsi,

i'm very thankful for your replies
they helped me alot
also the page of noveldv is veryyy useful
thanks alot
Click to expand...

Glad that it helped.

i just want to be clear on something
i'm a bit confused about the types of functional verification
can we say there is static and dynamic verification
or is it simulation based, assertion based and formal
where does formal verification lie exactly
i'm just a bit confused about the hierarchy of everything :)
is there something i can read that tells this in short and brief
cause i've tried some books but nothing is showing this issue directly in simple words

thanks alot again
Salma :)
Click to expand...

You are talking about the real pains of a practising verificaiton engineer and I have to agree with you that not a single book covers this clearly (atleast IMHO). This is precisely the reason why I created this course named CFV (see www.noveldv.com) and have heard some good feedback on the contents. Since you are based in France that information is not very useful to you right now. Several months down the line I'm planning to make that as a book as well, but given my current deadlines it is a dream project for now.

Your best bet for now is google and attend various seminars from EDA companies.


Good Luck
Ajeetha, CVC
www.noveldv.com
 
Re: verification Q (PSL)

well, thanks again

i've encountered a book called "using PSL/Sugar for formal and dynamic verification"
2nd edition

i think that u co-authored this book
it's got a very good intro regarding the issues i'm looking for
but it needs more on the dynamic verificaton part (simulation)

well, it looks like i've got to do further reading and reading and filtering of info to grasp a clear idea about verification as a whole

and i surely hope i would get a chance soon to travel to india and attend the courses :)

thanks again,
Salma
 

Status
Not open for further replies.

Similar threads

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top