The Formal Verification Program Leader: An Emerging Role in Verification

Formal verification of hardware designs has been around for more than 25 years. Commercial tools, for example from AT&T Bell Labs and IBM, started appearing in the 1990s. It’s only recently that formal verification has been adopted into design and verification flows, due to a number of reasons. It’s harder to learn than simulation or emulation because of its complexity, and it takes time for a verification engineer to become proficient in using it. Formal verification experts typically learn 100s of different techniques over the course of their careers.

Now that we are in the era of formal verification, an important new role is emerging –– the Formal Verification Program Leader (FV Program Leader). This individual has the mandate to drive the formal effort in the organization, and is tasked with managing the entire formal process.  He or she is usually organized, meticulous, an excellent communicator and an even better process manager, able to take a systematic approach to problem solving. This work is separate from the work done by an expert user of formal verification.

Today, this leadership role is emerging in almost every large semiconductor organization deploying formal verification on any significant scale, whether by circumstance or intent. It exists because formal verification is more complex than simulation; and senior ASIC management, while well versed in simulation and emulation, has little understanding of formal verification from the standpoint of process or return-of-benefit. Many ASIC managers wouldn’t know where formal verification works or doesn’t work and why, what designs it is good for, or what level of expertise is needed. How to include formal as part of a complete verification strategy, where and when to start formal, and how to synergistically combine it with simulation are strategic decisions few managers would be able to make effectively, either.

Engineers who are experts in formal verification methods often have a hard time communicating the level of difficulty of what they are trying to accomplish, or determining and expressing a schedule for formal verification. They may not know how to properly express the planning needed to implement formal verification to senior management, who doesn’t know formal (and may never know it). Formal tools don’t address these issues.

Companies in this situation have a difficult time building formal verification capability and deploying it. More important, perhaps, demonstrating a return on investment (ROI) for formal verification is different than for simulation; it is difficult to measure progress and, consequently, justify the investment.  Therefore, the role of the Formal Verification Program Leader is important.

Our industry lays claim to about 100-200 formal users who would be considered experts. FV Program Leaders have an even rarer skillset. Only a handful of people –– 20 at most –– could be considered FV Program Leaders.

The FV Program Leader drives the formal effort. A FV Program Leader may not come from a formal background, because expertise as a formal user is independent of formal program leadership. While FV Program Leaders need not be formal experts, they must be good at evangelizing formal, and pairing formal with other technologies. They are skilled at managing the formal process, effectively communicating with both upper management and engineers, assessing ROI and presenting the results to justify investment in formal verification, and influencing the formal roadmap. Success as an FV Program Leader does not require mastery of formal techniques, but implementing a successful formal verification program does require mastery of the processes.

The FV Program Leader’s role involves breaking down the abstract, translating it into familiar planning terminology, and providing insight as to the team’s progress relative to the plan. He or she must be able to interact and collaborate with the owners of the various ASIC projects, and should have the ability to leverage the formal process by understanding designs, schedules, and potential trade-offs to achieve project goals.

To be integrated into the verification flow, formal verification should not be treated like a separate island. Changing the perception that formal verification is somehow insular and distinct from the rest of the verification effort may be the biggest challenge for, but also the most important task of any FV Program Leader. The role of Formal Verification Program Leader, while not for everyone, is a critical one for companies making an investment in formal. It’s highly visible and ready-made for a capable individual who’s a good communicator, is able to manage tradeoffs and is a strong process leader.

There are six areas an FV Program Leader needs to think about: Organization, Training and Upskilling, Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis. A structured approach like this is not new to engineering, but it is new to formal verification. When addressing these six areas, formal can be incorporated seamlessly into the design flow, along with other traditional tools and methods. In this blog, I will discuss the first two of these six areas, and will cover the others in future posts.

Organization: Since the FV Program leader is chartered with building the program for an entire organization, involving multiple ASIC designs across many groups, and perhaps multiple geographies, the first question that needs to be addressed is how a formal team will be organized, within the existing organizational hierarchy. Will there be a centralized group of formal engineers (full-time or part-time?) reporting to a single manager, who may be the FV Program Manager, servicing multiple ASIC projects that are spread across the organization? Or is it better to have the formal engineers distributed among the project groups? The former is better if the organization is flexible enough to allow collaboration across organizational boundaries. Formal verification is a unique skill set in that its value is enhanced when ideas and strategies are shared by a team of skilled formal engineers supporting many different customers across the globe, and working under one roof. The question of a full-time vs. part-time focus for the engineers working with formal is also related to what scope will be verified; some applications of formal verification such as automated checking, or formal apps, are amenable to part-time work. However, if end-to-end formal verification is applied to replace unit-level simulation, it must almost always be executed by full-time formal verification engineers. We have seen some large organizations budget 15% of their entire verification manpower to full-time formal verification, with successful results. Another aspect of organization is mobility and career path. Will non-formal engineers be given an opportunity to move to a centralized formal verification team? Will formal engineers have an opportunity to learn other skills? As formal engineers succeed, how do we manage their career path? Will the building of a formal team be done by hiring experienced formal engineers? This is a difficult path, as there are few experienced formal engineers in the industry, perhaps fewer than 200. Or, is it better to hire and extensively train new college graduates?

Training and Upskilling: The learning curve for formal verification can be long. Having practiced formal verification for 23 years, I am still learning new techniques. Humility and the quest for learning is key to continuously building this expertise. If the formal team is comprised of engineers who are new to this area, a rigorous training program must be put in place. Our internal 10-course training program is a requirement for our new hires who have limited experience with formal.  More important than that is what follows – an apprenticeship-style training where a new formal verification engineer is coupled with more senior, experienced formal verification engineers. The road to success in formal verification is a challenging one, and it is important to receive guidance as one encounters failures, which could come in many forms – dealing with proofs that do not converge, numerous false failures and constraint iteration, missed bugs because of incomplete checkers, vacuously false proofs, etc. Some companies have gone through a more formalized training program by partnering with Oski, and having an Oski expert mentor one of their new formal engineers and/or provide classroom-style training. We have built a skillset chart of more than 40 different skills required by formal verification engineers. It is also important to understand both the background and aptitude of the formal verification engineers. Are they more analytical (mathematical) or practical (like engineers)? Formal verification is a very white-box style of verification. It is hard to enjoy this work if you do not like debugging or getting deep into others’ code. A formal verification engineer has to love debug, because most of the time he or she will debug false failures, as it is rare to find a designer with enough patience to iterate through formal verification false failures.

Test Planning, Progress Metrics, Sign-off Process, and Post Mortem Analysis are the other four areas the FV Program Manager should be concerned with. These will be covered in later posts.

Tags: formal sign-off, formal verification, formal verification methodology, Formal Verification Program Leader, organization, Oski Technology, post-mortem analysis, progress metrics, sign-off process, test planning, training, upskilling, Vigyan Singhal

Category: Blog

This entry was posted on Monday, February 22nd, 2016 at 5:09 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.