Formal Model Checking
Formal verification proponents can talk about how capacity has improved to upwards of 500K gates, how multiple formal engines working together have helped to fill in some of the gaps and how designers can verify their designs without any test vectors. We can wipe the tears of joy from our eyes and announce that all will be better with the next release; but we have to admit that apart from equivalence checking, formal technology has not been widely accepted or fully deployed. Formal model checking is not delivering on its promise. While the capacity of current tools is adequate for real design blocks, the creation of a good environment and the right assertions remain a major barrier to adoption. A joint study by Texas Instruments illustrates the basic challenges related with writing assertions. The technical team wrote 100 constraints for a 60K gate design and reported that the "environment constraints required a 2 weeks development (sic)." Many were very simple assertions by the team’s own admission. The paper concludes that "one big challenge today is to help people to easily express the properties to be checked on a design." Samuel Dellacherie participated in that project and is now the Project Manager for Formal Verification Tools at TransEDA. He is not shy to talk about the challenges: "In many cases, formal tools find a test sequence that will violate the environment. These false positives have to be analyzed because the cause of the failure could be an error in the environment or in the property itself." He is not surprised to hear that designers can spend 80% of their time writing and debugging the environment and the assertions. "In the Texas Instruments study, we spent 2 weeks to constrain and debug the environment while the properties only took 10 minutes to verify" he adds. Deployability is a significant barrier to the adoption of all new methodologies and tools. Formal model checking requires familiarity with the design, expertise with assertion languages and formal methods in order to avoid false results. The Texas Instruments study found that "(We) noticed that the knowledge of the RTL code influenced a lot the way to write properties." The difficulty in constraining the design environment and writing the properties affects formal verification’s deployability. An error, omission or ambiguity can significantly influence the results. "It’s often not the answer that the system gives you, but the question that you are asking" Samuel Dellacherie reaffirms, "an inexperienced user can spend a lot of time to determine if the problem is in the design or in the assertions." From most users’ perspective, deployability determines the real cost of the tool. Design managers often calculate a verification tool’s price tag by dividing the total cost by the number of designers who can use the tool. As long as formal verification remains a technology that can only be deployed to a few experts, the cost per user will remain relatively high. The Texas Instruments study offers valuable direction on how to deliver on the model checking promise: "However, in order to convince designers to use model checking techniques for hardware verification, it is mandatory to deliver them a convivial tool with user interface facilities. Also, the tool has to be effectively and easily integrated into the traditional hardware verification flow." Formal Verification becomes most valuable when it is focused where it can bring immediate benefit to the existing verification flow with minimum human interaction. A recent study by the Institute of System Level Integration, working with the University of Edinburgh and Motorola shows the power of formal model checking when it is combined with coverage tools to determine if each expression in a design is fully coverable. Putting the problem in perspective they specify that "because of coding style, some designs at Motorola have as much as 20% of their expression cases uncoverable." The result is pessimistic coverage figures, which must be analyzed, fixed or at least explained. Using available model checking and coverage tools, the team manually applied the two technologies to real designs and reduced the time to analyze each expression case from 5 minutes to 5 seconds. This research team also gives the EDA industry some guidance. "Although our implementation has been successfully used in the analysis of complex designs, further work would obviously be required before an efficient tool could be created." Formal verification must be automated to remove the risk of manual errors in creating the environment and the assertions. Some vendors are taking notice and we have already seen some successes such as the 0-In (now Mentor Graphics) assertion libraries. Averant created an AMBA verification kit and TransEDA automated the creation of the entire formal verification environment needed to exhaustively verify standard bus based designs further reducing the need for user interaction. Atrenta and TransEDA have incorporated formal technology with RTL rule checkers to provide more deployable solutions that prevent errors later in the design cycle. Design managers are conservative because they have to authorize tape-out, and that can mean a $1M signature. Formal model checking alone does not answer the questions that many design managers ask: "How do I know that I have enough assertions, the right assertions? How do I know when I’m done with my verification?" Pass-or-fail analysis is not enough and manually linking tools together introduces yet more uncertainty. The design manager must have a familiar way to determine that enough assertions have been written, that all the steps of each assertion have been reached and that all the variables have been fully verified. The greater promise of formal technology will be in its integration with complete coverage metrics, design coverability and specification coverage. Formal verification will deliver on its promises when it is focused, automated and integrated with other tools to provide better design coverage, faster verification and comprehensive metrics that tell the design manager when the verification process is complete and when it is safe to authorize the chip for tape-out. This delivery has already begun, some integrated solutions are available today and surely more will follow in the next few months. As for Peace in the World, that will have to wait until the next release.
References: 1. "Using Model Checking Techniques for Debugging a Data-Cache Management Block"
2. "Expression Coverability Analysis: Improving code coverage with model checking"
May 19, 2005 Modesto Casas is an independent specialist in Global Business Development for the EDA Industry. He is responsible for Corporate Business Development at TransEDA.
|