Design Article
Comment
Thomas.Anderson_#4
Rale
Actually, books about assertions claims about 1-2% of increased code size and ...
Top 10 Tips for Success with Formal Analysis – Part 1
Thomas Anderson, Verification Product Management Group Director, Cadence
12/12/2011 10:00 AM EST
Formal analysis, also known as property checking, has made significant progress in the last ten years in terms of ease of use, speed, capacity, and assertion-language standardization. Formal analysis has demonstrated clear value as an important component in the functional verification of both intellectual property (IP) and system-on-chip (SoC) designs. It complements RTL “lint” checking, simulation, simulation acceleration, in-circuit emulation (ICE), equivalence checking, and other verification techniques that are more widely adopted.
The use of formal analysis is not yet as widely adopted as its advocates once predicted it would be. In part, this is because many potential users have unrealistic expectations or try to deploy formal analysis in ways that do not play to its strengths. However, thousands of users on hundreds of IP and SoC projects have used formal analysis successfully, so it is clearly possible to apply the technology in appropriate ways to improve design quality and accelerate verification schedules. Knowing when, where, and how to apply formal analysis is the key.
This is the first in a series of three articles presenting the “top 10” tips for the successful use of formal analysis. These tips are based on more than a dozen years of experience with this technology, including most of the leading commercial formal products. The tips presume very little knowledge of formal tools or the assertions that drive them, and are discussed at a level of detail appropriate for both new users and current users looking for more advantage from their tools. Verification leads and project managers can also benefit from many of these tips.
Before starting the list, a quick review of formal analysis is in order. Fundamentally, a formal-analysis tool performs an exhaustive mathematical analysis of some statement about a design. For example, a designer might intend that a bus arbiter grants exactly one agent access to the bus at a time. If the designer specifies this design intent in the form of a “one-hot” assertion property, or more simply an assertion, a formal tool will attempt to prove that there is no way, under any possible legal sequence of inputs to the design, that this assertion can be violated.
If the result is a proof, the designer knows for sure that the arbiter has one-hot grants. Formal analysis may instead yield a counter-example, a test case showing a scenario under which zero or multiple grants can be asserted. This represents a bug in the design, an incorrect assertion, or inadequate assumption properties (also assumptions or constraints) on the inputs of the design. For an arbiter, one assumption might be that a request must stay asserted until it is granted. Generally, the designer does not care if a bug can be produced by an illegal input sequence, and the assumptions define the bounds of legal behavior.
Many formal tools can also analyze coverage properties (or covers), which are specified by the designer to pinpoint behavior that must be exercised for effective verification. In the case of an arbiter, the designer might want to ensure that every request is asserted at least once and that every grant is asserted at least once. When formal analysis encounters a cover, it attempts to produce a witness trace, a test case showing how the cover can be reached. Alternatively, formal analysis may prove that the cover is unreachable under all possible legal input sequences.
Thus, formal analysis attempts to violate assertions or prove them inviolable and to reach covers or prove them unreachable, all under the control of assumptions/constraints on the inputs. There are two main languages for specifying these three types of properties: SystemVerilog Assertions (SVA) [1] and Property Specification Language (PSL) [2]. Both are IEEE standards; numerous academic languages exist as well. There are also complementary assertion libraries available, most notably Accellera’s Open Verification Library (OVL) [3].
Formal analysis may have capacity limitations because of its exhaustive nature, so it is most often applied on blocks or chip sub-units rather than complete chips (with a specific exception discussed in Part 2 of this series). Formal analysis is also most often applied on designs dominated by control logic rather than datapaths or arithmetic elements. Assuming that formal analysis is being applied on a design of appropriate complexity and style, there are 10 tips that designers and verification engineers should keep in mind.
Tip 1: Involve designers in property specification and, whenever possible, in formal analysis
The preceding description of formal analysis is written from the standpoint of the designer, and indeed the designer is often the ideal person to specify properties. After all, the designer knows what the design is intended to do or not do (assertions), what interesting behaviors should be exercised (covers), and what rules adjoining blocks are expected to follow when driving the design’s inputs (assumptions). The designer must “simply” transfer this knowledge from his or her head into written properties, as in the FIFO example of Figure 1.
Of course, specifying properties is not always a simple task. Designers need to learn how to extract their own knowledge in the form of properties and must also learn enough SVA or PSL to be able to capture these properties. This effort takes additional time during the design capture (RTL coding) phase; industry consensus is that specifying properties adds 15-20% to the designer’s schedule. Ideally, design managers should require properties in RTL code and allocate time for adding them, or at the very least support the designers who perform this activity.
Unlike throwaway block-level testbenches, properties add value throughout the entire project. Assertions in higher-level simulation watch for bugs missed at the block level, assumptions check for disagreements on interfaces between adjoining blocks, and cover properties can be collected as part of overall coverage at any level. However, asking or requiring design engineers to do a task purely “for the good of the project” may not be an easy sale. In fact, that argument is not necessary; specifying properties actually saves designers time in their own schedules when properly applied.
Tip 2: Apply formal analysis early in the project so that engineers specifying properties see an immediate payoff
Most project teams require designers to perform at least a minimal level of verification, usually via block-level simulation with hand-generated test vectors or a very simple testbench. For appropriate blocks, formal analysis is a very attractive alternative, completely eliminating the need to develop a testbench or tests of any kind. If the designer runs formal analysis early and often during block development, he or she can detect bugs before any testbench is available, refine the assumptions to check the design’s inputs, and determine the reasons for unreachable covers.
It is a general rule in verification that effort and impact increase 10x for every stage at which a bug is discovered, from block-level verification to chip-level verification to ICE to prototype to field. It is always better to find a bug earlier. Specifically for the designer, bugs found during higher-level verification often require a lot of effort to understand. Many bugs are even directed to the wrong designers, resulting in time wasted on analysis before proper redirection. For these reasons, it is best for designers to run block-level formal analysis and find the bugs themselves.
Realistically, not all designers are interested in learning enough about formal analysis to be successful on their own. In such cases, a formal expert may work with the designer to ensure positive results, much as a verification engineer may work with the designer to develop a more sophisticated block-level testbench. In a recently published interview, formal expert Vigyan Singhal of Oski Technology discusses his experience working with a team at Cisco to formally verify a complex statistics block in only 3 months versus the 18 months projected for simulation [4].
Tip 3: Leverage all forms of automatic assertions, from basic design checkers through assertion synthesis
The discussion thus far has centered on designer-specified properties, which arguably provide the highest value since they represent design knowledge. Verification engineers will often write properties as well, especially for standard interfaces or design-library elements. Both design and verification engineers often question whether a tool “can specify my assertions for me” as an alternative to learning SVA or PSL. While not a complete alternative to user-specific assertions, there are certain types of assertions that can be automatically inferred from the design.
The most common automatic assertions are those derived from the design itself, including overflow and underflow checks for arithmetic expressions, bounds checks for arrays, checks for bus contention and floating buses, and checks for proper synchronization of asynchronous clocks. Some formal tools can also identify finite-state machines (FSMs) and generate assertions for dead-end or unreachable states. All these types of automatic assertions tend to be very accurate, requiring little review by the designer before being used.
Other automatic assertions are derived from the design and supplemental files that express some aspect of design intent. For example, Cadence® tools can generate assertions related to low-power operation from the combination of the design and a Common Power Format (CPF) power-intent file. Most recently, NextOp Software has developed an “assertion synthesis” approach that generates proposed assertions and covers (subject to designer review) from the combination of the design and simulation traces. Broadcom recently presented an interesting case study [5].
While no automatic assertion approach can completely replicate the information in the designer’s head, the combination of generated and hand-written properties is very valuable. The next installment in this series discusses the use of assertion libraries to help with property specification and delves deeper into the methodologies around effective use of formal -analysis tools. In the meantime, any comments, suggestions, or personal anecdotes on the use of properties and formal analysis are most welcome.
Editor’s Note: We expect to post subsequent parts of this article once a month, so look out for part 2 towards the middle of January 2012.
References
[1] “1800-2009 - IEEE Standard for SystemVerilog--Unified Hardware Design, Specification, and Verification Language” http://standards.ieee.org/findstds/standard/1800-2009.html
[2] “1850-2010 - IEEE Standard for Property Specification Language (PSL)” http://standards.ieee.org/findstds/standard/1850-2010.html
[3] “Accellera Standard OVL V2 Library Reference Manual” http://www.accellera.org/activities/ovl/
[4] “Vigyan Singhal interview by Richard Goering at DAC” http://www.youtube.com/watch?v=H-QNR8agW4A
[5] “NextOp BugScope Case Study” http://www.dvclub.org/images/Presentation/DVClub2011_broadcom.pdf
Thomas L. Anderson is Product Management Group Director, Advanced Verification Systems at Cadence. His previous positions include Director of Technical Marketing in the Verification Group at Synopsys, Vice President of Applications Engineering at 0-In Design Automation, and Vice President of Engineering at Virtual Chips. Mr. Anderson has presented more than 100 conference talks and published more than 150 papers and technical articles on such topics as advanced verification, formal analysis, SystemVerilog, and design reuse. He holds an MS in Electrical Engineering and Computer Science from MIT and a BS in Computer Systems Engineering from the University of Massachusetts at Amherst.
If you found this article to be of interest, visit EDA Designline where you will find the latest and greatest design, technology, product, and news articles with regard to all aspects of Electronic Design Automation (EDA).
Also, you can obtain a highlights update delivered directly to your inbox by signing up for the EDA Designline weekly newsletter – just Click Here to request this newsletter using the Manage Newsletters tab (if you aren't already a member you'll be asked to register, but it's free and painless so don't let that stop you [grin]).
The use of formal analysis is not yet as widely adopted as its advocates once predicted it would be. In part, this is because many potential users have unrealistic expectations or try to deploy formal analysis in ways that do not play to its strengths. However, thousands of users on hundreds of IP and SoC projects have used formal analysis successfully, so it is clearly possible to apply the technology in appropriate ways to improve design quality and accelerate verification schedules. Knowing when, where, and how to apply formal analysis is the key.
This is the first in a series of three articles presenting the “top 10” tips for the successful use of formal analysis. These tips are based on more than a dozen years of experience with this technology, including most of the leading commercial formal products. The tips presume very little knowledge of formal tools or the assertions that drive them, and are discussed at a level of detail appropriate for both new users and current users looking for more advantage from their tools. Verification leads and project managers can also benefit from many of these tips.
Before starting the list, a quick review of formal analysis is in order. Fundamentally, a formal-analysis tool performs an exhaustive mathematical analysis of some statement about a design. For example, a designer might intend that a bus arbiter grants exactly one agent access to the bus at a time. If the designer specifies this design intent in the form of a “one-hot” assertion property, or more simply an assertion, a formal tool will attempt to prove that there is no way, under any possible legal sequence of inputs to the design, that this assertion can be violated.
If the result is a proof, the designer knows for sure that the arbiter has one-hot grants. Formal analysis may instead yield a counter-example, a test case showing a scenario under which zero or multiple grants can be asserted. This represents a bug in the design, an incorrect assertion, or inadequate assumption properties (also assumptions or constraints) on the inputs of the design. For an arbiter, one assumption might be that a request must stay asserted until it is granted. Generally, the designer does not care if a bug can be produced by an illegal input sequence, and the assumptions define the bounds of legal behavior.
Many formal tools can also analyze coverage properties (or covers), which are specified by the designer to pinpoint behavior that must be exercised for effective verification. In the case of an arbiter, the designer might want to ensure that every request is asserted at least once and that every grant is asserted at least once. When formal analysis encounters a cover, it attempts to produce a witness trace, a test case showing how the cover can be reached. Alternatively, formal analysis may prove that the cover is unreachable under all possible legal input sequences.
Thus, formal analysis attempts to violate assertions or prove them inviolable and to reach covers or prove them unreachable, all under the control of assumptions/constraints on the inputs. There are two main languages for specifying these three types of properties: SystemVerilog Assertions (SVA) [1] and Property Specification Language (PSL) [2]. Both are IEEE standards; numerous academic languages exist as well. There are also complementary assertion libraries available, most notably Accellera’s Open Verification Library (OVL) [3].
Formal analysis may have capacity limitations because of its exhaustive nature, so it is most often applied on blocks or chip sub-units rather than complete chips (with a specific exception discussed in Part 2 of this series). Formal analysis is also most often applied on designs dominated by control logic rather than datapaths or arithmetic elements. Assuming that formal analysis is being applied on a design of appropriate complexity and style, there are 10 tips that designers and verification engineers should keep in mind.
Tip 1: Involve designers in property specification and, whenever possible, in formal analysis
The preceding description of formal analysis is written from the standpoint of the designer, and indeed the designer is often the ideal person to specify properties. After all, the designer knows what the design is intended to do or not do (assertions), what interesting behaviors should be exercised (covers), and what rules adjoining blocks are expected to follow when driving the design’s inputs (assumptions). The designer must “simply” transfer this knowledge from his or her head into written properties, as in the FIFO example of Figure 1.
Unlike throwaway block-level testbenches, properties add value throughout the entire project. Assertions in higher-level simulation watch for bugs missed at the block level, assumptions check for disagreements on interfaces between adjoining blocks, and cover properties can be collected as part of overall coverage at any level. However, asking or requiring design engineers to do a task purely “for the good of the project” may not be an easy sale. In fact, that argument is not necessary; specifying properties actually saves designers time in their own schedules when properly applied.
Tip 2: Apply formal analysis early in the project so that engineers specifying properties see an immediate payoff
Most project teams require designers to perform at least a minimal level of verification, usually via block-level simulation with hand-generated test vectors or a very simple testbench. For appropriate blocks, formal analysis is a very attractive alternative, completely eliminating the need to develop a testbench or tests of any kind. If the designer runs formal analysis early and often during block development, he or she can detect bugs before any testbench is available, refine the assumptions to check the design’s inputs, and determine the reasons for unreachable covers.
It is a general rule in verification that effort and impact increase 10x for every stage at which a bug is discovered, from block-level verification to chip-level verification to ICE to prototype to field. It is always better to find a bug earlier. Specifically for the designer, bugs found during higher-level verification often require a lot of effort to understand. Many bugs are even directed to the wrong designers, resulting in time wasted on analysis before proper redirection. For these reasons, it is best for designers to run block-level formal analysis and find the bugs themselves.
Realistically, not all designers are interested in learning enough about formal analysis to be successful on their own. In such cases, a formal expert may work with the designer to ensure positive results, much as a verification engineer may work with the designer to develop a more sophisticated block-level testbench. In a recently published interview, formal expert Vigyan Singhal of Oski Technology discusses his experience working with a team at Cisco to formally verify a complex statistics block in only 3 months versus the 18 months projected for simulation [4].
Tip 3: Leverage all forms of automatic assertions, from basic design checkers through assertion synthesis
The discussion thus far has centered on designer-specified properties, which arguably provide the highest value since they represent design knowledge. Verification engineers will often write properties as well, especially for standard interfaces or design-library elements. Both design and verification engineers often question whether a tool “can specify my assertions for me” as an alternative to learning SVA or PSL. While not a complete alternative to user-specific assertions, there are certain types of assertions that can be automatically inferred from the design.
The most common automatic assertions are those derived from the design itself, including overflow and underflow checks for arithmetic expressions, bounds checks for arrays, checks for bus contention and floating buses, and checks for proper synchronization of asynchronous clocks. Some formal tools can also identify finite-state machines (FSMs) and generate assertions for dead-end or unreachable states. All these types of automatic assertions tend to be very accurate, requiring little review by the designer before being used.
Other automatic assertions are derived from the design and supplemental files that express some aspect of design intent. For example, Cadence® tools can generate assertions related to low-power operation from the combination of the design and a Common Power Format (CPF) power-intent file. Most recently, NextOp Software has developed an “assertion synthesis” approach that generates proposed assertions and covers (subject to designer review) from the combination of the design and simulation traces. Broadcom recently presented an interesting case study [5].
While no automatic assertion approach can completely replicate the information in the designer’s head, the combination of generated and hand-written properties is very valuable. The next installment in this series discusses the use of assertion libraries to help with property specification and delves deeper into the methodologies around effective use of formal -analysis tools. In the meantime, any comments, suggestions, or personal anecdotes on the use of properties and formal analysis are most welcome.
Editor’s Note: We expect to post subsequent parts of this article once a month, so look out for part 2 towards the middle of January 2012.
References
[1] “1800-2009 - IEEE Standard for SystemVerilog--Unified Hardware Design, Specification, and Verification Language” http://standards.ieee.org/findstds/standard/1800-2009.html
[2] “1850-2010 - IEEE Standard for Property Specification Language (PSL)” http://standards.ieee.org/findstds/standard/1850-2010.html
[3] “Accellera Standard OVL V2 Library Reference Manual” http://www.accellera.org/activities/ovl/
[4] “Vigyan Singhal interview by Richard Goering at DAC” http://www.youtube.com/watch?v=H-QNR8agW4A
[5] “NextOp BugScope Case Study” http://www.dvclub.org/images/Presentation/DVClub2011_broadcom.pdf
Thomas L. Anderson is Product Management Group Director, Advanced Verification Systems at Cadence. His previous positions include Director of Technical Marketing in the Verification Group at Synopsys, Vice President of Applications Engineering at 0-In Design Automation, and Vice President of Engineering at Virtual Chips. Mr. Anderson has presented more than 100 conference talks and published more than 150 papers and technical articles on such topics as advanced verification, formal analysis, SystemVerilog, and design reuse. He holds an MS in Electrical Engineering and Computer Science from MIT and a BS in Computer Systems Engineering from the University of Massachusetts at Amherst.If you found this article to be of interest, visit EDA Designline where you will find the latest and greatest design, technology, product, and news articles with regard to all aspects of Electronic Design Automation (EDA).
Also, you can obtain a highlights update delivered directly to your inbox by signing up for the EDA Designline weekly newsletter – just Click Here to request this newsletter using the Manage Newsletters tab (if you aren't already a member you'll be asked to register, but it's free and painless so don't let that stop you [grin]).
|
|
|
|
|
Navigate to related information
BrianBailey
12/12/2011 10:45 AM EST
Tom, you say that adding assertions increases the time required by about 15-20%. What is the ROI in terms of the estimated time saved by having bugs found earlier, or additional bugs found?
Sign in to Reply
Rale
12/22/2011 9:01 AM EST
Actually, books about assertions claims about 1-2% of increased code size and small increase of RTL coding phase but substantially shorter verification/debug phase. For sure, assertions can help, but they are not silver bullet.
Sign in to Reply
Thomas.Anderson_#4
1/23/2012 4:02 AM EST
Brian,
I do believe that designers have a net savings across the project by adopting assertions because it's so much easier to diagnose bugs found at the block level. However, I have not seen a solid ROI analysis to support this belief.
Tom A.
Sign in to Reply