Webinar Report: How Formal “Apps” Ease IC Verification
By Richard Goering on August 16, 2012Comments(0)Filed under: Industry Insights, IP-XACT, verification, Incisive, IEV, Formal Analysis, IFV, VIP, webinar, assertions, ABV,assertion-based verification, formal verification, properties, code coverage, formal scoreboard, Mueller, Rubik's cube, Lego robot, reachability, Hupcey, formal apps, register map, protocol compliance, SoC connectivity, Sudoku, linting, formal applications, functional verificatioin, ABVIPFormal verification applications, or "apps," can significantly lighten the IC verification workload without requiring a knowledge of assertion-based verification (ABV) - or even, in most cases, the need to write assertions. A recently archived Cadence webinar, held Aug. 8, 2012, describes some helpful formal apps and encourages users to build their own.
The webinar, titled "Formal Apps to Automate Mainstream Verification Challenges," was presented by Joseph Hupcey III, product marketing director at Cadence, and Joerg Mueller, staff solutions engineer at Cadence. It is part of an ongoing series of free functional verification webinars that will run through mid-December.
Hupcey began the webinar by talking about the challenges that have limited the adoption of formal and ABV technologies. He noted that many engineers do not want to learn about assertion languages, that most engineers do not want to learn about formal techniques, and that verification leads have trouble showing the value of formal in the context of a full project. While there's an assumption that it takes a PhD to run formal verification, "that's not true today, and we'll show you a way to automate that away completely," Hupcey said.
What's a Formal App?
In a general sense, Mueller said, an app runs on a platform - in this case, on Cadence Incisive Formal Verifieror Incisive Enterprise Verifier. He offered this three-part definition of a formal app:
Formal apps across the project life cycle
Automatic Formal Analysis and Super Linting
The top two apps identified on the chart work together to provide an advanced linting solution in which properties are generated directly from the implied behavior of the RTL. This is needed because designers generally do not provide adequate verification for the code they write. An HDL analysis linting capability links checks and messages back to the source code. Automatic formal analysis automatically provides checks for such concerns as dead code, finite state machine, pragmas, X states, busses, range overflow, and toggling. HDL analysis linting combined with automatic formal analysis results in "Super Linting."
Protocol Compliance
Protocols are well-defined in written specifications, but what we need to verify against is an executable specification. The solution is to use pre-packaged properties along with assertion-based verification IP (ABVIP) for a given protocol. Cadence now provides ABVIP for major AMBA protocols and for OCP, and it can be used in both simulation and formal verification. Protocol-aware debug, now available in the Cadence SimVision user interface, offers protocol-specific transaction-level debugging. The webinar includes a demo.
Formal Scoreboard
Formal verification has historically been targeted only to control-oriented functionality, but data transport checking is actually a "sweet spot" for formal technology, according to Mueller. The solution is to provide a set of pre-packaged properties that are tuned for data transport checking using sequences of symbols. The basic idea is to force (or constrain) a sequence of input values, and check (assert) that the same sequence appears on the output. Cadence Incisive Formal Verifier and Incisive Enterprise Verifier provide a Formal Scoreboard Template that can help with this task.
Code Coverage Unreachability
This is "probably the fastest growing formal app that we see in the marketplace at the moment," according to Mueller. The problem is that holes in code coverage can take weeks to analyze manually. If you can sort out unreachable (impossible to hit) coverage holes, the task will be easier. This formal app analyzes whether uncovered code is reachable (in which case the test suite is insufficient) or unreachable (solved by fixing RTL or discarding the hole). A demo shows that this process is fully automatic and that users don't even see the formal tool running.
(Note: A user case study of a code coverage unreachability formal app is provided in an archived CDNLive! India 2011 paper by Freescale. )
Register Map Validation
All too often, simulation insufficiently checks for correct register map access and absence of corruption. A formal app can generate properties automatically from an IP-XACT specification, and greatly simplify the register map validation flow. The assertions can check value after reset, register access policies, and the use of write-read sequences with front door and back door access.
SoC Connectivity
This is the oldest and most mature formal app, in production since 2005, Mueller said. It automatically generates properties from the connectivity specification in order to quickly and efficiently verify IP integration. The spec defines internal connections as well as external connections to and from I/O pads. The app provides forms and wizards to ease specification entry and import into a spreadsheet, lets users import results from analysis, and offers built-in connectivity "linting." A demo shows how to edit a spreadsheet, run connectivity checks, debug a failure, and back-annotate results to the spreadsheet.
Dream Your Own!
"What we want to encourage you to do now," Mueller concluded, "is to dream up your own formal apps. Look for verification problems that are boring, repetitive, or inefficient with simulation because it is difficult or tedious to create the desired stimulus. Look for a requirement that can be easily described in assertions."
Note: For examples of "fun" formal apps dreamt up by Cadence R&D people, see the following:
Richard Goering
Related Blog Posts
Video: How Formal Analysis "Apps" Provide New Verification Solutions
DVCon 2012 Video: Product Engineer Chris Komar Reviews the Tutorial on Formal Apps
Archived Webinar: Using Scoreboards With Formal Verification
The webinar, titled "Formal Apps to Automate Mainstream Verification Challenges," was presented by Joseph Hupcey III, product marketing director at Cadence, and Joerg Mueller, staff solutions engineer at Cadence. It is part of an ongoing series of free functional verification webinars that will run through mid-December.
Hupcey began the webinar by talking about the challenges that have limited the adoption of formal and ABV technologies. He noted that many engineers do not want to learn about assertion languages, that most engineers do not want to learn about formal techniques, and that verification leads have trouble showing the value of formal in the context of a full project. While there's an assumption that it takes a PhD to run formal verification, "that's not true today, and we'll show you a way to automate that away completely," Hupcey said.
What's a Formal App?
In a general sense, Mueller said, an app runs on a platform - in this case, on Cadence Incisive Formal Verifieror Incisive Enterprise Verifier. He offered this three-part definition of a formal app:
- A well-documented tool capability or methodology focused on a specific, high-value problem
- The problem is more efficiently solved using formal methods than using simulation-based methods
- The need to create properties or have ABV knowledge is significantly reduced, because properties can be generated automatically or provided in a pre-packaged form
Formal apps across the project life cycle
The top two apps identified on the chart work together to provide an advanced linting solution in which properties are generated directly from the implied behavior of the RTL. This is needed because designers generally do not provide adequate verification for the code they write. An HDL analysis linting capability links checks and messages back to the source code. Automatic formal analysis automatically provides checks for such concerns as dead code, finite state machine, pragmas, X states, busses, range overflow, and toggling. HDL analysis linting combined with automatic formal analysis results in "Super Linting."
Protocol Compliance
Protocols are well-defined in written specifications, but what we need to verify against is an executable specification. The solution is to use pre-packaged properties along with assertion-based verification IP (ABVIP) for a given protocol. Cadence now provides ABVIP for major AMBA protocols and for OCP, and it can be used in both simulation and formal verification. Protocol-aware debug, now available in the Cadence SimVision user interface, offers protocol-specific transaction-level debugging. The webinar includes a demo.
Formal Scoreboard
Formal verification has historically been targeted only to control-oriented functionality, but data transport checking is actually a "sweet spot" for formal technology, according to Mueller. The solution is to provide a set of pre-packaged properties that are tuned for data transport checking using sequences of symbols. The basic idea is to force (or constrain) a sequence of input values, and check (assert) that the same sequence appears on the output. Cadence Incisive Formal Verifier and Incisive Enterprise Verifier provide a Formal Scoreboard Template that can help with this task.
Code Coverage Unreachability
This is "probably the fastest growing formal app that we see in the marketplace at the moment," according to Mueller. The problem is that holes in code coverage can take weeks to analyze manually. If you can sort out unreachable (impossible to hit) coverage holes, the task will be easier. This formal app analyzes whether uncovered code is reachable (in which case the test suite is insufficient) or unreachable (solved by fixing RTL or discarding the hole). A demo shows that this process is fully automatic and that users don't even see the formal tool running.
(Note: A user case study of a code coverage unreachability formal app is provided in an archived CDNLive! India 2011 paper by Freescale. )
Register Map Validation
All too often, simulation insufficiently checks for correct register map access and absence of corruption. A formal app can generate properties automatically from an IP-XACT specification, and greatly simplify the register map validation flow. The assertions can check value after reset, register access policies, and the use of write-read sequences with front door and back door access.
SoC Connectivity
This is the oldest and most mature formal app, in production since 2005, Mueller said. It automatically generates properties from the connectivity specification in order to quickly and efficiently verify IP integration. The spec defines internal connections as well as external connections to and from I/O pads. The app provides forms and wizards to ease specification entry and import into a spreadsheet, lets users import results from analysis, and offers built-in connectivity "linting." A demo shows how to edit a spreadsheet, run connectivity checks, debug a failure, and back-annotate results to the spreadsheet.
Dream Your Own!
"What we want to encourage you to do now," Mueller concluded, "is to dream up your own formal apps. Look for verification problems that are boring, repetitive, or inefficient with simulation because it is difficult or tedious to create the desired stimulus. Look for a requirement that can be easily described in assertions."
Note: For examples of "fun" formal apps dreamt up by Cadence R&D people, see the following:
- Incisive Enterprise Verifier solving Sudoku puzzle in 0.1 seconds
- Incisive Enterprise Verifier driving a Rubik's Cube solving Lego robot
Richard Goering
Related Blog Posts
Video: How Formal Analysis "Apps" Provide New Verification Solutions
DVCon 2012 Video: Product Engineer Chris Komar Reviews the Tutorial on Formal Apps
Archived Webinar: Using Scoreboards With Formal Verification
Using formal “apps” to automate IC verification | LinkedIn
'via Blog this'
No comments:
Post a Comment