KEYNOTE: Robustness of formal verification of x86 microprocessors

Presented as part of the 2021 HCSS conference. 

ABSTRACT

Industrial formal verification is challenging due to the continuous changes inherent in commercial design. Validation starts as soon as any part of a new design is available, and it needs to continue smoothly through post-silicon verification. Hence, verification must be adaptable to incomplete design and frequent changes. In addition, specification might change due to a feedback from back-end tools (layout, timing, array organization, power) and changes in the product market. Centaur Technology, an Austin, TX-based company that designs x86 compatible microprocessors, has been using formal verification since 2007. This effort was initiated by Centaur leadership through their contact with UT Professor, Warren Hunt. Hunt with his then PhD student, Sol Swords, proposed to make a case study using ACL2 system to analyze their arithmetic design. Their ability to find a very subtle bug in a mature design convinced Centaur's leadership to invest in a formal verification (FV) team that over time grew to four members. Over the thirteen years of their existence, FV group has become an indispensable part of Cenatur's design team. Unlike other hardware companies, Centaur analyzes their designs primarily using theorem proving, instead of relying on model-checking and SMT tools only. Although surprising to some, the ACL2 theorem prover provides a fine balance between proof automation and user guidance. The Centaur FV approach is fully integrated into their design flow. A suite of regression proofs can be trigerred by changes in the design, specification and/or proofs, or can be scheduled (nightly, weekly, etc.). FV team is then alerted by a failure that can be investigated and remediated. Formal microprocessor verification has been shown to be resilient to the continuous changes of the design under development. We will describe the challenges of using formal verification in an industrial setting, and how we handle them using open-source and proprietary tools.

Anna Slobodova is the Lead of the Formal Verification group at Centaur Technology, Inc. Centaur's focus is on designing high-performance low-cost x86 microprocessors https://www.centtech.com/ . Dr. Slobodova is interested in technology that can improve validation of complex industrial design (from hands-on theorem proving to automated procedures). She obtained a Masters degree and a PhD in Theoretical Computer Science (with a focus on Complexity Theory) at Comenius University, Bratislava, Slovakia. She started her career as a Research Scientist at Comenius University. She later moved to became an Assistant Professor at the University of Trier, Germany, and she was also appointed in the Fraunhoffer Institue for Telematik. In 1998, she joined Digital Equipment Corporation (later Compaq) in Massachussetts, USA, where she worked in a small group on one of the first sequential equivalence checkers in industry. When Compaq was purchased by Intel, she joined the formal verification group known as "Dragon Team". After seven years at Intel, Dr. Slobodova joined Centaur Technology, where she assumed responsibility for Centaur's formal verification team that had been started by a University of Texas professor. Additional professional staff has been added, and the FV team's work is now an indispensable part of the company's design and validation process. Dr. Slobodova has served on multiple program committees focused on formal methods including CAV, CPP, DATE and FMCAD. For FMCAD 2009, she served as the, organizational co-chair, and as the conference general co-chair in 2011. She presently serves on the FMCAD Steering Committee. She was a Test and Verification track co-chair of ICCD 2011, and FV topic co-chair for DATE 2020 and 2021.