The relation between assertions and Formal Verification

[vizpal]

Are Assertions Synthesisable... ???
If not the how come Formal Verification possible...???

 

[avimit]

ifv bei sva

Assertions are not synthesizable.
And I dont see any relation between assertions and formal verification. Pls let me know what is the relation between assertions and formal verification.
Kr,
Avi
http://www.vlsiip.com

 

[vizpal]

sva example

I havent done any Formal Verification yet, but my understanding is that Formal Verification is based on Assetions and synthesisable code.
My doubt is -> Does this mean that assertions must be synthesisable??????

 

[avimit]

Re: SVA

Formal verification is NOT based on assertions. I hope it clears your doubt.
Kr,
Avi
http://www.vlsiip.com

 

[vizpal]

Re: SVA

Are u sure that Formal does'nt make use of Assertions !!!
You might want to read this....
**broken link removed**

 

[avimit]

Re: SVA

Well, its a good article, but it is too much into the future. At present as a part of my job, I do FV to verifiy RTLvsNetlist using synopsys's formality. As far as FV as of now is concerned, there is no relation of assertions and FV.
Kr,
Avi
http://www.vlsiip.com

 

[master_picengineer]

SVA

Hi all,
There is a techniques of formal verifiation based on assertion called Assertion based Verification (ABV). In is used nowaday in several company.

 

[avimit]

Re: SVA

Sorry, I didnt knew that. I am working with synopsys' formality, and I only know formality has no relation with AVB
But I wonder if AVB is parallel to todays FV.
If AVB is verifying funtionality, then it would be different from what FV is doing, because FV is only comparing two designs, it does not funtionally verify anything.
Can you name any tool using ABV, and a company using it?
Kr,
Avi
http://www.vlsiip.com

 

[optronic]

Re: SVA

Hi,

with Formality you make an equvalence check: Netlist against RTL, based on
formal methods, no assertion here.

The other think is called Static or Dynamic Formal Verification, and here
you need to define assertions (based on properties) that these tools try to formally
proove for the RTL design. Tools are Magellan (synopsys) or 0-in (mentor)
for example.
Assertions are also used in ABV in tools like QuestaSim (mentor)
or VCS (synopsys).

Hope that helps,
op

 

[ecikin]

SVA

Assertions can not be synthesized

 

[boardlanguage]

Re: SVA

Hi,
with Formality you make an equvalence check: Netlist against RTL, based on
formal methods, no assertion here.

The other think is called Static or Dynamic Formal Verification, and here
you need to define assertions (based on properties) that these tools try to formally
proove for the RTL design. Tools are Magellan (synopsys) or 0-in (mentor)
for example.
Assertions are also used in ABV in tools like QuestaSim (mentor)
or VCS (synopsys).

Please tell me more!
During a Synopsys seminar, I think they discussed Dynamic Formal Verification. Basically, the designer wants to check a statement...like "The ACK signal always fires exactly 10-cycles after REQ is asserted."

Then you enter some "initial-conditions", to kick-off a hypothetical analysis, and the Verification-tool searches for a 'counterexample' to your statement. More often than not, the tool fails ... in other words, it can't disprove your statement (either because your statement is too broad, or because the design's behavior truly agrees with your statement.)

Is it something like that?

 

[aji_vlsi]

Re: SVA

Folks,
Under Formal Verification there are few techniques:

1. Equivalence Checking (EC) - tools like LEC, Formality
2. Model Checking (MC) - Magellan, IFV,
3. Hybrid Formal - Magellan, 0-in
4. Theorem Proving - more at research level.

Out of these, MC and Hybrid use SVA/PSL as specification. We showed this with examples in our PSL & SVA books (www.systemverilog.us). I also cover these topics in great detail in our CFV course, see: www.noveldv.com for details.

Regards
ajeetha, CVC
www.noveldv.com

 

[boardlanguage]

Re: SVA

Folks,
Under Formal Verification there are few techniques:

1. Equivalence Checking (EC) - tools like LEC, Formality
2. Model Checking (MC) - Magellan, IFV,
3. Hybrid Formal - Magellan, 0-in
4. Theorem Proving - more at research level.

Out of these, MC and Hybrid use SVA/PSL as specification. We showed this with examples in our PSL & SVA books (www.systemverilog.us). I also cover these topics in great detail in our CFV course, see: www.noveldv.com for details.

Thanks again, aji_vlsi!

Are these listed in order of popularity/application-use? (I assume equivalence-checking is the most popular use for Formal Verification.)

 

[aji_vlsi]

Re: SVA

Folks,
Under Formal Verification there are few techniques:

1. Equivalence Checking (EC) - tools like LEC, Formality
2. Model Checking (MC) - Magellan, IFV,
3. Hybrid Formal - Magellan, 0-in
4. Theorem Proving - more at research level.

Out of these, MC and Hybrid use SVA/PSL as specification. We showed this with examples in our PSL & SVA books (www.systemverilog.us). I also cover these topics in great detail in our CFV course, see: www.noveldv.com for details.

Thanks again, aji_vlsi!

Are these listed in order of popularity/application-use? (I assume equivalence-checking is the most popular use for Formal Verification.)

Order was not intended to, but it does match the order of popularity. A good point/bullet for my training slide

Ajeetha, CVC
www.noveldv.com

 

[natg9]

Re: SVA

Hi friends

i am looking for some material to study System Verilog Assertions
please share if you have any documents

thanks in advance

regards
natg

 

[ljxpjpjljx]

Re: SVA

SVA is a method for you to check the design bug more efficiently , it can't be synthesis!

 

[sunilbudumuru]

Re: SVA

Hello Friends,

Assertions for sure not synthesizable.

FYI.

Synopsys Formality tool latest versions are supporting assertion based designs also. But limited constructs. May be in coming releases they will incorporate the rest of SV constructs.

How it works?

In the reference design if the FV tool found any tool supported assertions, Formality converts these assertions into design constraints during the set_top command.

Forgot to mention tht you need to set "hdlin_enable_assertions" variable to true during formal verification.

Note: If assertions found in implementation it just ignores.

Cheers

Sunil Budumuru
www.asic-dft.com/

 

[anassar]

Re: SVA

Some subset of assertion languages (SVA/PSL) can be synthesized. Actually, assertion-based verification had been done using finite-state machines before SVA/PSL/Sugar were invented. Modern-day tools (like Cadence Incisive) can synthesize assertions and verify them on hardware-accelerated verification platforms.

See what Cadence says on Acceleration-Based Verification and Assertion-Based Verification.

 

[ljxpjpjljx]

Re: SVA

SVA is so useful for detect error in DUT!