Help me understand verification in PSL

[salma ali bakr]

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

 

[Guru59]

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

 

[aji_vlsi]

Re: verification Q (PSL)

Hi,

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 ) );

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:

 always (END ->

After END is seen,

 next

From the NEXT clock cycle onwards

 ( 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

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

 

[salma ali bakr]

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

 

[aji_vlsi]

Re: verification Q (PSL)

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

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

Ajeetha, CVC
www.noveldv.com

 

[salma ali bakr]

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

 

[aji_vlsi]

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

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

 

[salma ali bakr]

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)

 

[aji_vlsi]

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?

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]

 

[salma ali bakr]

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

 

[aji_vlsi]

Re: verification Q (PSL)

Hi,

hi aji_vlsi,

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

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

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

 

[salma ali bakr]

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