WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 | 5 |

«Abstract. In the last quarter century computer-aided verification – es- pecially in the form of model checking – has evolved from a research ...»

-- [ Page 1 ] --

Verification Technology Transfer

R. P. Kurshan

Cadence Design Systems, Inc., New Providence, NJ 07974

Abstract. In the last quarter century computer-aided verification – 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 significant 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 specified. Since component level functionality is often revealed at best obscurely in the design’s functional specification, 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-specific 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 afforded 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 verification technology from research to the market place.

1 Introduction Computer-aided verification 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 verification [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 verification 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 verification 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 verification. 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 verification 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

Abstract

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 verification. Its commercialization was led by M. Fourman and R. Harris.

Perhaps it was the inherent difficulties 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 verification could be said to have been conceived. Its birth would come three years later as model checking.

Analyzing a finite 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 defined in a temporal logic. This difference 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 define the environment of an adjoining block. These two: formalization of assertions and algorithmic verification 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 verification, anyone who applied the theory soon realized that its real value lay in falsification. Go to a designer with the the claim “I verified that your design is correct” and you get a muffled yawn – of course her design is correct, she thinks, why wouldn’t it be? (And who knows what “verified” 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 first 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 effective to find 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 ‘verified’ only means ‘failed to find 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 reflecting design errors). Although before this event my “verification” 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 fields 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 verification, in which design testing (via verification) could be started earlier in the development flow 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 verification. 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 staff 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 – off 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 staff 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 refinement 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 verification – the design passed system integration test with flying 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 confident that the last six years of wandering had finally 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 effort and remain effective. 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? Off 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 first 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, first 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.



Pages:   || 2 | 3 | 4 | 5 |


Similar works:

«The Bosnian State a Decade after Dayton SUMANTRA BOSE A decade on from the Dayton peace settlement, this essay sets out to examine two questions. First, is the consociational and confederal paradigm established by the Dayton agreement, and subsequently institutionalized, the appropriate framework for the Bosnian state? It will be suggested that in the circumstances that prevail, this framework does in fact provide the most feasible and most democratic form of government for Bosnia’s...»

«Ipek Çalislar: Latife Hanim Turkish, Biography Report by Moris Farhi Latife Hanim – “Hanim” means “Lady” in Turkish – was the wife of Mustafa Kemal (of Gallipoli fame), the founder and first president of modern Turkey later to be known as Atatürk, “Father of the Turks”. (Note: I will refer to Mustafa Kemal as Atatürk throughout this report even though the cognomen was conferred on him long after his marriage to Latife Hanim.) In the main, this biography concentrates on Latife...»

«i HP Creative Scrapbook Assistant Software for quick and easy printable layouts and unique page elements User’s Guide ii Contents Introduction.................................. 4 About this User’s Guide..................... 5 Visit the HP Scrapbooking Web site............. 6 Getting started........................... 6 1 Installing and starting the program................. 7...»

«Membership & Levy Consultation Feedback Association Chair Informal Feedback Associations chairs were asked to give their views informally, that is their personal views rather than an association view – simply because many associations do not hold meetings during the 3-month consultation period. Option 1 2 3 Other Yes 1 2 3 1 ? Yes Yes 1 1 1 1 No 1 Alternatives See notes 1 Key points made during the discussions: 1. Option 2 preferred, a continuation of the 1:3 balance that feels right; feels...»

«Rev. Claire Feingold Thoryn Theme: “Gratitude” Sermon: “Give It Away” November 22, 2015 (Reverse Offering Service) Call to Worship The prophet Mohammed was asked “What actions are most excellent?” And he replied: “To gladden the heart of a human being. To feed the hungry. To help the afflicted. To lighten the sorrow of the sorrowful. To remove the wrongs of the injured. That person is the most beloved of God who does the most good to God’s creatures.” Let us join together with...»

«A method to assess global energy requirements of suburban areas at the neighbourhood scale Anne-Françoise Marique1,* and Sigrid Reiter1 1 Local Environment: Management & Analysis (LEMA), University of Liege, Liege, Belgium * Corresponding email: afmarique@ulg.ac.be ABSTRACT This article presents the method developed to assess existing suburban neighbourhoods in order to improve their energy efficiency. It combines the use of dynamic simulation tools to evaluate energy requirements for heating...»

«DE NOVO CLASSIFICATION REQUEST FOR TEARSCIENCE, INC. LIPIFLOW® THERMAL PULSATION SYSTEM REGULATORY INFORMATION FDA identifies this generic type of device as: Eyelid Thermal Pulsation System. An eyelid thermal pulsation system is an electricallypowered device intended for use in the application of localized heat and pressure therapy to the eyelids. The device is used in adult patients with chronic cystic conditions of the eyelids, including meibomian gland dysfunction (MGD), also known as...»

«Cordarone® (amiodarone HCl) TABLETS DESCRIPTION Cordarone (amiodarone HCl) is a member of a class of antiarrhythmic drugs with predominantly Class III (Vaughan Williams’ classification) effects, available for oral administration as pink, scored tablets containing 200 mg of amiodarone hydrochloride. The inactive ingredients present are colloidal silicon dioxide, lactose, magnesium stearate, povidone, starch, and FD&C Red 40. Cordarone is a benzofuran derivative: 2-butyl-3benzofuranyl...»

«33 GEORGE AND HELEN WAITE PAPASHVILY: THE FIRST DAY The First Day * * GEORGE AND HELEN WAITE PAPASHVILY George Papashvily and his American wife collaborated on Anything Can Happen, a book recounting George's experiences as,an immigrant from Georgia, one of the republics of the former Soviet Union, to the United States shortly after World War I (1914-1918). AT FIVE IN THE MORNING THE ENGINES STOPPED, AND AFTER THIRTY-SEVEN days the boat was quiet. We were in America. I got up and stepped over...»

«PATIENT & FAMILY CARE GUIDE 2 care guide for Patients and Families Our Legacy and PrOmise tO yOu For over 35 years, Hospice of Dayton and Hospice of Butler & Warren Counties have served the needs of our local communities by providing the very best end-of-life care, support and comfort for any patient or family that needs it. Our promise is to celebrate the lives of those we have the privilege of serving by honoring memories, sharing stories and cherishing moments in time. Our commitment is to...»

«30029-XX Entocort® EC (budesonide) Capsules Rx only DESCRIPTION Budesonide, the active ingredient of ENTOCORT® EC capsules, is a synthetic corticosteroid. It is designated chemically as (RS)­ 11β, 16α, 17,21-tetrahydroxypregna-1,4-diene-3,20-dione cyclic 16,17-acetal with butyraldehyde. Budesonide is provided as a mixture of two epimers (22R and 22S). The empirical formula of budesonide is C25H34O6 and its molecular weight is 430.5. Its structural formula is: C H 2O H C O CH3 H O HO C O...»

«  1   Excerpt from Wer ist Martha? By Marjana Gaponenko Translated by Arabella Spencer I Love is cold. Love is cold. But in the grave we burn and melt to gold. Levadski waited for the tears. The tears didn’t come. In spite of this he wiped his face. Disgusting! With a fixed stare he had just put the receiver on its cradle. What else, if not impatience, had he sensed in the breathing of his family doctor? Impatience and the buzzing of thoughts that had nothing to do with him, Levadski:...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.