Bridging the Frontier 
Bob Smith, Executive Director
Bob Smith is Executive Director of the ESD Alliance responsible for its management and operations. Previously, Bob was senior vice president of Marketing and Business Development at Uniquify, responsible for brand development, positioning, strategy and business development activities. Bob began his … More » A Look at the Practical Benefits of Formal Verification with AxiomiseFebruary 21st, 2023 by Bob Smith, Executive Director
To better understand formal and attempt to demystify it, I got in touch with ESD Alliance member Axiomise and its founder Dr. Ashish Darbari, CEO and Founder of Axiomise. Ashish is a well-known figure in verification circles for his formal expertise –– he received a Doctorate Formal Verification from the University of Oxford. Our conversation helped me appreciate and better understand the practical reasons why formal verification is becoming an important element in the verification toolbox. I’m giving a talk at DVCon during Accellera’s lunch Monday on the CHIPS Act and its impact of the design and verification markets. Watch for a blog post from me about it.
Smith: Formal verification has been a long-time verification strategy. Why has it been slow to be adopted? Darbari: The biggest barrier to adopting formal verification has been a lack of good training in the methodology. EDA vendors did a great job showcasing how formal tools could be used for solving problems such as connectivity checking, linting, X-propagation, and CDC. There was virtually no discussion or training on how to deploy formal property verification (FPV) for mainstream functional verification. While the market for formal verification has continued to grow and is about 40% of the simulation market, formal is not yet mainstream. It is certainly not the first choice of verification technology for every silicon design house yet. Smith: What’s changing to make it more central to a design and verification flow? Darbari: We have seen that in many cases, a solid understanding of the scope of formal verification and how to deploy it widely in a scalable manner makes the biggest difference. I have seen first-hand that our hands-on, vendor-neutral, methodology-focused consulting and services accompanied by training has shown a significant enhancement in formal verification usage and, more importantly, respect for formal methods. Smith: To what degree can formal methods solve or mitigate hardware vulnerabilities in new chip designs? Darbari: Formal is ideal for security verification. The reason why security is a hard problem for any verification is because design verification engineers have to conceive an unbounded (potentially infinite) number of unknown threats. Formal tools by default, inject stimulus for free and could potentially unearth problems in the chip design very easily. Formal verification uses constraints (or assumptions) to prevent illegal stimulus. By relaxing the constraints strategically, one can check the robustness of the design under what would be considered as illegal stimulus from a functional verification point of view but would be perfectly legal from a hacker’s point of view. A recent article published on EDN shows how formal was used for identifying vulnerabilities in RISC-V processors. Smith: What are the benefits of a formal verification strategy for the entire supply chain? Darbari: Formal verification can prove the absence of bugs while at the same time discovering corner case bugs within seconds. While bug hunting has the usual advantage of establishing defect-free chips, another important advantage of using formal is in integration testing where different IP blocks from potentially different suppliers are integrated on a single chip. Here, formal properties are used to establish the correctness of design interfaces (contracts) between different IP components. Smith: Can you cite an example where formal verification made a difference? Darbari: RISC-V processor cores verification challenges is a good example and I’ll use an Axiomise project as an example where we found hundreds of bugs in previously verified RISC-V cores including deadlocks, safety violations, and security issues. In other domains, for example, design engineers who never used formal at all are able to tape out their first chip extensively verified with formal finding 150 bugs with formal alone weeks and months before dynamic simulation.
Darbari: We expect to see more growth in this segment in 2023. As recession hits the industry, we see that many top silicon design houses are laying off their own workforce but continue to spend money in hiring for formal verification. This includes continued outsourcing of formal verification for projects, and we certainly see a surge in demand for our experts. About Dr. Ashish Darbari Ashish Darbari, CEO and Founder of Axiomise, has been actively using formal methods for more than two decades and is one of the foremost authorities in practical applied formal verification having trained nearly 200 designers and verification engineers globally. A keen innovator in formal verification, he is the founder and CEO of Axiomise and leads it by successfully deploying training, consulting, services and verification IP to a range of customers. Dr. Darbari has expertise in all aspects of formal methods including theorem proving, property checking and equivalence checking. He holds a Doctorate formal verification from the University of Oxford and has 60 patents in formal verification. About the ESD Alliance The ESD Alliance is a SEMI Technology Community representing members in the electronic system and semiconductor design ecosystem that addresses technical, marketing, economic and legislative issues affecting the entire industry. We act as the central voice to communicate and promote the value of the semiconductor design ecosystem as a vital component of the global electronics industry. Contact me at bsmith@semi.org if you would like to learn more. Follow SEMI ESD Alliance ESD Alliance Bridging the Frontier blog Twitter: @ESDAlliance |
|
|
|||||
|
|
|||||
|
|||||
