Avery Design announced using formal to verify complex reset schemes PDF Print E-mail

Article Downloads

Using Formal to Verify Complex Reset Schemes

By Chris Browy and Kai-hui Chang, 10/04/09

Complex reset schemes can be difficult to verify dynamically because of the non-determinism caused by
unknowns (Xs) in the registers, and their unpredictable propagation. Here, we describe a formal approach to
X-verification of partial and full reset schemes, and a partial reset reduction methodology that reduces
the number of registers being reset while still maintaining the same reset state of the original design.



All * fields must be completed in order to submit this form.

First Name* :
Last Name* :
Title:
Company* :
Street Address:
City:
State/Province:
Zip/Postal Code:
Email* :
Phone:

Please let us know your design and verification situation.


What formal tools do you use today?

Jasper Gold
Cadence IFV
Synopsys Magellan
Synopsys Formality
Mentor
Real Intent
One Spin
Other
How large blocks do you perform formal analysis on (gate equivalents)?

less than 500K
500K to 1M
1M to 2M
2M to 4M
4M or more
What uses would you use formal for now or in the future?

Architectural model checking supporting behavioral formal analysis of protocols
System-level equivalency checking (arch vs RTL) using SystemC or SystemVerilog for high-level synthesis (HLS) flows
Sequential equivalency checking for re-pipelining and staging
RTL model checking of blocks
Reachability analysis of RTL code blocks, assertions, and cover properties
X-verification to identify sources of non-determinism and for design reset and software initialization or power state transitions in low power design.
Clock domain crossing
Interconnect checking
Logical equivalency checking
IP delivery will include support for formal to verify integration of IP into user designs and their interfaces
Improved coverage closure through more formal methods used in constraint solving
Limited register retiming for physical optimization
Post silicon debug

What languages and methodologies do you use?

Verilog
SystemVerilog
VHDL
SystemC
Vera or NTB
Specman
VMM
OVM
What languages do you write assertions with?

SVA
PSL
OVL
Do you use code coverage?

Yes
No
Do you use these types of coverage analysis?

cover property
coverpoint
scoreboard-based coverage

Personal Information Use
Avery will not share your personal information with anyone.