In recent years, technology and methodology improvements have increased formal technology's ease-of-use, productivity and quality of results, enabling its application throughout the design flow. At the top end, it is used to explore, verify and debug architecture level models; in the middle, to help develop and verify RTL blocks; and at the bottom end, for post-silicon debug. Clearly, the industry has the formal technology and methodologies to tackle complex verification and debug issues.
Here's a scenario that we commonly encounter. A design team is having difficulty verifying and analyzing some functionality using only dynamic verification methods. Using simulation on tasks such as ensuring the absence of deadlock, detecting and debugging unexpected X's, and verifying cache coherency, outcomes can be uncertain and are often effort-intensive. With this in mind, the team decides that formal methods can deliver greater certainty—even absolute certainty.
This is often the first step in a design team's adoption of formal—one pain point triggers the decision. Initially, the team wants to use formal to solve only this problem. Understandably, it wants only those tools, methodologies and external expertise necessary to do so. However, many formal tool suites are structured to address a wide range of verification challenges, and require more expertise than the "formal newcomer" design team needs to address this single pain point. Even seasoned formal users occasionally have gaps that they want to fill without having to expend more time and effort than is necessary.
The industry has effective technology and methodology, but clearly "something" is missing. That "something" is a true, targeted solutions approach to formal verification. The Targeted Solutions Approach
The industry needs a solution that addresses individual formal verification tasks without the user having to become expert in all aspects of formal verification. We need an "apps" approach that enables the design team to jump-start and complete an immediate verification task with only the technology, methodology and expertise appropriate to that task—one that doesn't require the team to learn and use all of the features, functionality and "how to" of the formal verification tool. Of course, a team can research and identify the appropriate tool functionality and formal methodology by itself, but an app eliminates this effort and the need for the expertise to do it.
Moreover, an apps approach is tailor-made to suit a design team's incremental adoption and deployment of formal methods. Starting with the initial pain point, an apps approach enables the team to extend its use of formal step-by-step, and with minimum risk. When the team is ready to expand deployment of formal beyond the initial pain point, it simply invokes the appropriate additional apps. In this manner, the team broadens and deepens its expertise and knowledge in synch with its project requirements—a gradual, non-disruptive approach essential to low-risk adoption and deployment.
As the team's deployment of formal expands, it will need a great deal of flexibility in the use of these various apps. For example, to support optimum work sharing, an apps approach must support the execution of several instances of a particular app in parallel. It must also support the execution of several different apps simultaneously on the same block, enabling verification and analysis of the block up and down the design flow.
The apps approach needs a single, common database that captures the results of all apps/tasks, together with a common graphical user interface (GUI) that accesses only the data of interest to a given user. This tool architecture is not only essential to efficient apps usage; it also allows the technology innovator to enhance the technology seamlessly with further apps.
And how should the technology provider create additional apps? To ensure that there is a market need for an app, it should be a customer-driven development. A new app starts with a customer-specific problem. The technology, methodology, and expertise developed and used to solve it are then packaged as a standard "app" product, already tried-and-tested on a real customer problem.
The bottom line? Formal verification apps offer users greater ease and speed of adoption; the simplicity, reliability and lower risk of incremental deployment; the flexibility to mix-and-match apps to suit the task requirements; and higher productivity.
In short, we need a simpler and faster approach to formal verification. We need apps. Rajeev Ranjan is CTO of Jasper Design Automation. He can be reached at Rajeev@jasper-da.com.
We have many examples of how customers are using Jasper formal technology. Go to www.jasper-da.com/customers/success-stories or go to www.jasper-da.com/resource-library/technical-white-papers to find articles, white papers, and technical videos.
David Patterson, known for his pioneering research that led to RAID, clusters and more, is part of a team at UC Berkeley that recently made its RISC-V processor architecture an open source hardware offering. We talk with Patterson and one of his colleagues behind the effort about the opportunities they see, what new kinds of designs they hope to enable and what it means for today’s commercial processor giants such as Intel, ARM and Imagination Technologies.