«Abstract. In the last quarter century computer-aided veriﬁcation – es- pecially in the form of model checking – has evolved from a research ...»
Veriﬁcation Technology Transfer
R. P. Kurshan
Cadence Design Systems, Inc., New Providence, NJ 07974
Abstract. In the last quarter century computer-aided veriﬁcation – es-
pecially in the form of model checking – has evolved from a research con-
cept to a commercial product. While the pace of this technology transfer
was anything but rapid, the new technology had almost insuperable hur-
dles to jump on its way to the market place. Hurdle number one was a
required signiﬁcant change in methodology. On account of its limited ca- pacity, model checking must be applied only to design components (RTL blocks in the case of hardware) instead of the whole design as with sim- ulation test. Thus, the functional behavior of these design components must be speciﬁed. Since component level functionality is often revealed at best obscurely in the design’s functional speciﬁcation, either designers must convey component functionality to those doing the testing or else testers must somehow fathom it on their own. The former was consid- ered an unacceptable diversion of vaunted designer resources while the latter was often undoable. A second hurdle was uncertainty surround- ing the quality of the new tools. Initially the tools were incomparable and required the user to create considerable tool-speciﬁc infrastructure to specify properties before a tool could be evaluated. Recreating the re- quired infrastructure for several tools was infeasible. This meant choosing a tool without a head-to-head evaluation against other tools. With the high cost and uncertain outcome aﬀorded by these hurdles, no circuit manufacturer was willing even to consider seriously this new technology.
Not, that is, until the cost of testing-as-usual became higher than the cost of jumping these formidable hurdles. This essay is the saga of the transfer of computer-aided veriﬁcation technology from research to the market place.
1 Introduction Computer-aided veriﬁcation could be said to derive from Russell-Whitehead’s Principia Mathematica (1910-1913) [WR13], which laid a foundation for ax- iomatic reasoning. More germane was Alan Turing’s model of computation [Tur36].
The Turing Machine led to automata theory developed by Rabin and Scott[RS59] for languages of strings and then by B¨ chi [B¨ c62] for languages of sequences.
u u The latter provided the basis for automata-theoretic veriﬁcation [Kur94,VW86] on which model checking can be founded. Model checking per se was developed in 1980 by Clarke and Emerson [CE82] and Queille and Sifakis [QS82] indepen- dently. Earlier, around 1960, computer-aided veriﬁcation was introduced in the form of automated theorem proving. Theorem proving derived especially from the resolution method of Robinson [Rob65], which evolved into other more practical non-resolution methods by Bledsoe and others, leading to the UT Austin school of automated theorem proving that featured Gypsy (by Ron Goode and J. C. Browne) and then the famous Boyer-Moore theorem prover – see [BL84].
Until 1990, most of the investment in computer-aided veriﬁcation went to automated theorem proving. This was especially true for U. S. government support, which was lavished on automated theorem proving during this period.
For all its expressiveness and proving potential, automated theorem proving has not quite yet made it into main-stream commercial use for computer-aided veriﬁcation. One important reason is scalability of use: using an automated theorem prover requires specialized expertise that precludes its broad use in industry. Moreover, even in the hands of experts, using an automated theorem prover tends to take more time than would allow it to be applied broadly and still track the development of a large design project. Therefore, to the extent that automated theorem proving is used on commercial projects, it tends to be used for niche applications like veriﬁcation of numerical algorithms (hardware multipliers and dividers, for example). Although one company in particular, AMD, has made extensive practical use of theorem proving for such applications, utilization is presently too narrow and specialized to attract much attention in the Electronic Design Automation (EDA) marketplace, where vendors such as Cadence, Synopsys, Mentor Graphics and others sell software tools for industrial development of integrated circuits. A brief exception was the failed attempt by
Hardware Ltd. of Scotland to market the LAMBDA theorem prover based on HOL [GMW79]. Based on Milner’s ML, HOL had been developed originally for hardware veriﬁcation. Its commercialization was led by M. Fourman and R. Harris.
Perhaps it was the inherent diﬃculties in applying automated theorem proving that led Amir Pnueli to envision a more restricted but potentially simpler approach to verifying concurrent programs for properties expressed in Temporal Logic [Pnu77]. Although he too was focused on deductive reasoning, he noted (in passing) that Temporal Logic formulas could be checked algorithmically. In this incidental observation, commercial computer-aided veriﬁcation could be said to have been conceived. Its birth would come three years later as model checking.
Analyzing a ﬁnite state coordinating system through an exploration of its composite state space was actually proposed by Rudin and West [RW82,Wes78] around 1980 too. However, it was model checking that formalized the process in terms of checking a model for a property deﬁned in a temporal logic. This diﬀerence was very germane to practicality, as it led to decision procedures. Moreover, only with model checking could properties cast as assertions to be checked be reused as constraints to deﬁne the environment of an adjoining block. These two: formalization of assertions and algorithmic veriﬁcation paved the path to the broad success of model checking. In fact, the gating issues for technology transfer were procedural, not technical. Model checking technology has continuously far out-stripped its pace of adoption.
1.1 First Projects Although the theory spoke of veriﬁcation, anyone who applied the theory soon realized that its real value lay in falsiﬁcation. Go to a designer with the the claim “I veriﬁed that your design is correct” and you get a muﬄed yawn – of course her design is correct, she thinks, why wouldn’t it be? (And who knows what “veriﬁed” means anyway.) But, show her a bug in a form she can readily
comprehend (a simulation error trace) and she immediately recognizes the value:
you found a bug that she did not know was there. From the ﬁrst applications of model checking, it was clear that the real value of model checking was that it was an uncommonly good debugger – reductio ad bug. It is more eﬀective to ﬁnd a bug by trying to prove that there is none, than to go looking for it directly – the bug is always where you didn’t think to look. As a debugger, the model checker is forgiven for any black magic that went into its application (like abstractions, restrictions, unsoundness) since it’s only the bug that matters; no need to understand the means. “I don’t need to understand what model checking is, because I know a bug when I see it (and ‘veriﬁed’ only means ‘failed to ﬁnd a bug’).” In 1983 I applied an early version of the COSPAN [HHK96] model checker to a model that I created by hand. The model was a very high level abstraction of an implementation developed in AT&T of the link-level protocol of the X.25 standard. Through this process I found 2 bugs that were manifest in their implementation (among about a dozen artifactual failures manifest by my abstraction, but not reﬂecting design errors). Although before this event my “veriﬁcation” work was viewed with jaundiced suspicion at Bell Labs Research, my “practical contribution” lent me some (begrudged) breathing room. (Begrudged, because my work was hard to categorize among recognized ﬁelds of research that were supported at Bell Labs.) With this breathing room I found another similar application that was credited with saving AT&T a half-million dollars. This earned me the resources to re-write and develop COSPAN, which I then started with Zvi Har’el in 1985. During this process, I began to understand what I was doing (having been embarrassingly ignorant of the entire relevant literature).
COSPAN was based on ω-automata, which I then learned were classical objects in computer science. In 1986 I proposed a development methodology based on automata-theoretic veriﬁcation, in which design testing (via veriﬁcation) could be started earlier in the development ﬂow than previously possible and this I claimed would accelerate the design development process [KH90].
As I found others working in this area, especially Ed Clarke whom I met in 1985, I learned that my application experiences were common and shared by most who tried to apply algorithmic veriﬁcation. In fact Ed and his students had made interesting and relevant advances that I could use, as had others. Ed was impressed that COSPAN (circa 1986) could explore as many as a million states (!), and did much to encourage me to continue my work.
In 1987-89 COSPAN was applied to an ambitious hardware development project: a packet layer controller chip (PLC). With an anticipated layout of 200,000 transistors, it was medium-sized at the time. The project was spec’d but rejected by Marketing based on its projected development cost – 30 staﬀ years. The disgruntled project manager had read an early draft (internal TM) of [KH90] and invited me to try my method on his design, which we would run as a “black bag” job – oﬀ the record. I agreed to contribute 100% of my time and he would contribute his architect for the project. Together (in the end, he contributed 2 more people), we completed the project in 6 staﬀ years, 2 calendar years. We had succeeded to verify over 200 properties (well, more or less), drawn from a list of what the test group would test for. The design was developed through a 4-level abstraction hierarchy, wherein each subsequent reﬁnement was correct by construction. The bottom level was synthesized automatically, from C code generated by COSPAN. Although the performance of the design was only half as fast as expected – on account of some architectural decisions we had made to simplify veriﬁcation – the design passed system integration test with ﬂying colors. It was said to have the level of reliability of a second generic release. The low development cost (20% of what had been projected) and speed to market was said to out-weigh its somewhat poor performance.
The PLC project created a stir in AT&T MicroElectronics, as the TM that documented the project was circulated. By this time both myself and the project manager were vindicated and rewarded. It was 1989, and I was conﬁdent that the last six years of wandering had ﬁnally reached a conclusion and all that remained was to help shepherd this new and obviously valuable technology into general use. Little could I imagine that I had another 15 years of shepherding ahead of me.
1.2 The Catch 22 of Technology Transfer
Post-PLC, I was certain that my new technology would be in great demand. I worked out a triage plan to deal with the anticipated requests for my time, to avoid dilution of eﬀort and remain eﬀective. I would demand assistants, carefully select which projects I would handle.
But after a few days, my phone had registered nary a ring. Was my name misspelled in the TM? Where are all my anticipated fans? What’s going on?
Swallowing my pride, I went back to the same development group that had the success with the PLC and asked about their next project. Were they planning to use the PLC methodology? (A rhetorical politeness for “why haven’t you called me for the next project?”) To my astonishment, the answer was “no” – no future anticipated application of the PLC methodology! Amazing! What’s going on? “Well,” they said, “the PLC was a great project, but we could never implement your methodology ourselves, you may be the only one in the world who can do this for all we know, and anyway we could never rely on ‘Research software’ for a ‘real’ (i.e., non-black-bag) project – who would maintain the software? Next month you may be working on something else, and then who do we go to when your software breaks?”. “No, go to our CAD group”, they counseled, “convince them to support your software and then we will eagerly use it”.
Ah, so reasonable! How could I have been so naive? Oﬀ to the CAD group.
“Had they heard about the PLC project?” “Well, here’s who to speak to.” “What do you mean, ‘no point’ ? This is a proven productivity enhancer! You must support it! Ask them.” The answer remained “No”. They said “We cannot support a complex piece of software embedded in a revolutionary new methodology just because one development team asks us to – we would never make back our investment. Come back to us when you have 20 development teams asking us to support this. Then we will consider it.” “Hmm.. At 2 years per project, I could reach 20 successes in 40 years. Would the ﬁrst project still be around to remember?” To be broadly used it must be supported; to be supported, it must already be broadly used. The inescapable vicious circle!
Utterly depressed, I accepted an invitation to give a course on this technology, ﬁrst at UC Berkeley, then at the Technion in Israel. (My book [Kur94] came directly from my Berkeley course notes.) Attending my Technion course were four designers from Intel. They invited me down to Intel to give a mini-course there. It was 1990. From the mini-course came a challenge: verify this P5 cache protocol.
It had been simulated for 13 months with billions of vectors, and had no known problems, but they were still worried about it. They drew some diagrams on the board, I translated them into a model, tried to verify the model, found a “bug” and they explained to me, based on the bug, what was wrong with my model.
This process repeated for ten days, generating about two revisions per day. In fact, I wasn’t allowed to use the Intel computers (nor was I authorized to download COSPAN there), so all my runs were at the Technion where a university licensed COSPAN was installed. The explanations for revisions came by email.