SVA

EDAboard.com Forum Index -> ASIC Design Methodologies & Tools (Digital) -> SVA

Author

Message

vizpal

Joined: 26 Apr 2007
Posts: 43

03 Oct 2007 13:21 formality vs magellan equivalence checking

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

avimit

Joined: 16 Nov 2005
Posts: 417
Helped: 69
Location: Fleet, UK

03 Oct 2007 13:30 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

Joined: 26 Apr 2007
Posts: 43

03 Oct 2007 14:05 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

Joined: 16 Nov 2005
Posts: 417
Helped: 69
Location: Fleet, UK

03 Oct 2007 14:07 Re: SVA

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

vizpal

Joined: 26 Apr 2007
Posts: 43

04 Oct 2007 6:43 Re: SVA

Are u sure that Formal does'nt make use of Assertions !!!
You might want to read this....
http://www.eetimes.com/news/design/showArticle.jhtml?articleID=16504695

avimit

Joined: 16 Nov 2005
Posts: 417
Helped: 69
Location: Fleet, UK

04 Oct 2007 14:43 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

Joined: 03 Sep 2007
Posts: 1050
Helped: 62

04 Oct 2007 14:54 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

Joined: 16 Nov 2005
Posts: 417
Helped: 69
Location: Fleet, UK

04 Oct 2007 14:59 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

Joined: 27 Dec 2001
Posts: 20

11 Oct 2007 21:15 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

Joined: 14 Jul 2007
Posts: 26

25 Nov 2007 9:18 SVA

Assertions can not be synthesized

boardlanguage

Joined: 06 Apr 2007
Posts: 96
Helped: 4

10 Jan 2008 0:19 Re: SVA

optronic wrote:

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

Joined: 10 Sep 2004
Posts: 640
Helped: 72
Location: Bangalore, India

13 Jan 2008 17:17 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

Joined: 06 Apr 2007
Posts: 96
Helped: 4

16 Jan 2008 17:12 Re: SVA

aji_vlsi wrote:

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

Joined: 10 Sep 2004
Posts: 640
Helped: 72
Location: Bangalore, India

17 Jan 2008 0:25 Re: SVA

boardlanguage wrote:

aji_vlsi wrote:

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 Smile

Ajeetha, CVC
www.noveldv.com

Google
AdSense
Google Adsense

17 Jan 2008 0:25 Ads

natg9

Joined: 17 Jul 2008
Posts: 57
Helped: 7

16 Mar 2009 8:23 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

Joined: 05 May 2008
Posts: 533
Helped: 12
Location: Shang Hai

17 Mar 2009 4:54 Re: SVA

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

sunilbudumuru

Joined: 08 Oct 2008
Posts: 113
Helped: 18
Location: Hyderabad

09 Apr 2009 10:06 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

Joined: 20 Nov 2006
Posts: 12

21 Apr 2009 19:09 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.