Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronic 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

The relation between assertions and Formal Verification

Status
Not open for further replies.

vizpal

Member level 2
Joined
Apr 26, 2007
Messages
44
Helped
1
Reputation
2
Reaction score
0
Trophy points
1,286
Activity points
1,519
Are Assertions Synthesisable... ???
If not the how come Formal Verification possible...???
 

avimit

Banned
Joined
Nov 16, 2005
Messages
413
Helped
91
Reputation
182
Reaction score
23
Trophy points
1,298
Location
Fleet, UK
Activity points
0
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

Member level 2
Joined
Apr 26, 2007
Messages
44
Helped
1
Reputation
2
Reaction score
0
Trophy points
1,286
Activity points
1,519
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

Banned
Joined
Nov 16, 2005
Messages
413
Helped
91
Reputation
182
Reaction score
23
Trophy points
1,298
Location
Fleet, UK
Activity points
0
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
 

Joined
Sep 3, 2007
Messages
853
Helped
66
Reputation
132
Reaction score
16
Trophy points
1,298
Activity points
0
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

Banned
Joined
Nov 16, 2005
Messages
413
Helped
91
Reputation
182
Reaction score
23
Trophy points
1,298
Location
Fleet, UK
Activity points
0
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

Newbie level 6
Joined
Dec 27, 2001
Messages
13
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
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

Junior Member level 1
Joined
Jul 14, 2007
Messages
16
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
1,330
SVA

Assertions can not be synthesized
 

boardlanguage

Full Member level 1
Joined
Apr 6, 2007
Messages
96
Helped
7
Reputation
14
Reaction score
1
Trophy points
1,288
Activity points
2,083
Re: SVA

optronic said:
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

Advanced Member level 2
Joined
Sep 10, 2004
Messages
646
Helped
85
Reputation
170
Reaction score
12
Trophy points
1,298
Location
Bangalore, India
Activity points
4,975
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

Full Member level 1
Joined
Apr 6, 2007
Messages
96
Helped
7
Reputation
14
Reaction score
1
Trophy points
1,288
Activity points
2,083
Re: SVA

aji_vlsi said:
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

Advanced Member level 2
Joined
Sep 10, 2004
Messages
646
Helped
85
Reputation
170
Reaction score
12
Trophy points
1,298
Location
Bangalore, India
Activity points
4,975
Re: SVA

boardlanguage said:
aji_vlsi said:
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

Member level 3
Joined
Jul 17, 2008
Messages
56
Helped
7
Reputation
14
Reaction score
0
Trophy points
1,286
Activity points
1,588
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

Advanced Member level 3
Joined
May 5, 2008
Messages
972
Helped
80
Reputation
162
Reaction score
55
Trophy points
1,308
Location
Shang Hai
Activity points
4,679
Re: SVA

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

sunilbudumuru

Full Member level 2
Joined
Oct 8, 2008
Messages
123
Helped
41
Reputation
82
Reaction score
17
Trophy points
1,298
Location
Hyderabad
Activity points
2,219
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

Newbie level 6
Joined
Nov 20, 2006
Messages
12
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
1,401
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.
 

Status
Not open for further replies.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Top