From owner-qed Tue Nov 22 18:51:16 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id SAA15055 for qed-out; Tue, 22 Nov 1994 18:50:51 -0600 Received: from grolsch.cs.ubc.ca (grolsch-2.cs.ubc.ca [142.103.5.5]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id SAA15049 for ; Tue, 22 Nov 1994 18:50:45 -0600 Received: from troy.cs.ubc.ca (aagaard@troy.cs.ubc.ca [142.103.11.19]) by grolsch.cs.ubc.ca (8.6.9/8.6.9) with SMTP id QAA10354 for ; Tue, 22 Nov 1994 16:50:13 -0800 Message-Id: <199411230050.QAA10354@grolsch.cs.ubc.ca> From: aagaard@troy.cs.ubc.ca (Mark Aagaard) Date: Tue, 22 Nov 1994 16:50:10 -0800 Reply-To: Mark Aagaard Organization: University of British Columbia, Computer Science X-Address: Vancouver, BC V6T 1Z4 X-Phone: 604/822-5401 X-Fax: 604/822-5485 X-Mailer: Mail User's Shell (7.2.4 2/2/92) To: qed@mcs.anl.gov Subject: hardware verification Sender: owner-qed@mcs.anl.gov Precedence: bulk In regards to the discussion on the use in hardware verification of formal methods in general, and proof development systems in particular, I'd like to emphasize some of the points that have been made and add my own opinions. I think the main lessons from the past few years are that: 1) No single method is suitable for all aspects of verification for any reasonable size circuit. 2) We are moving from "virtuoso" verification efforts, to design and verification methodologies. - - - - - - Addressing the first point: By acknowledging that we must rely on a variety of methods and tools to verify a circuit, we decide where proof development systems are most effective. I think that it is generally acknowledged that they work well when: 1) There is a large abstraction gap between the specification and implementation. (e.g. specifications about real numbers and implementations with bit-vectors). 2) Regularity in the structure of the circuit can be used to decompose the problem into smaller pieces. (e.g. n-bit adders, multipliers, networks, etc) 3) A common structure appears in a class of circuits or a reasoning approach is applicable a class of circuits. (e.g. Microprocessors) Theorem proving based methods have not been as successful at reasoning effectively about properties like set-up and hold times as conventional tools such as timing analyzers have been. That doesn't mean that theorem-proving based methods are ineffective in general, just that they are not a panacea. Conventional simulation, model-checkers and other automated tools can bang out many circuits must faster than any proof system could. But, there are examples, such as those that have been mentioned by others here, and which I believe fall into the categories I've listed above, where theorem-proving based methods are very effective. As designs get more and more sophisticated, simulation times increase to the point where engineers choose not to implement proposed designs because the verification effort would be too costly. As an example, the MIPS R8000 design team chose in-order (rather than out-of-order) instruction issue and completion for their integer pipeline [Hsu93]. These types of design complexities are prime targets for theorem-proving based methods --- no other known techniques have a chance of solving them. (As a blatant and self-serving plug for my own work, I've developed some verification techniques for pipelined circuits. This work provides systematic ways of decomposing some of the large and complex verification problems (which can not be handled by conventional or model-checking techniques) into relatively small and straightforward tasks that can be handled by such automated tools [AL94].) - - - - - - Addressing the second point: (The second point is actually due to Phil Windley.) As one piece of evidence, at Theorem Provers in Circuit Design 94, 10 out of the 18 papers described techniques for simplifying verification efforts. In 1992 less than 1/4 of the papers focused on this topic. As Phil has pointed out here, he routinely teaches students to verify microprocessors that several years ago would have required a great deal of effort by an expert. Advances such as these are possible because we have gained enough experience with virtuoso verification to recognize patterns and similarities between different examples. An earlier example along these lines is Tom Melham's type definition package for HOL. Before this package was available, defining a new recursive type in HOL required intimate knowledge of the logic. Now, it is almost as easy as defining a new type in a functional programming language. In hardware verification, Phil's abstract interpreter package for microprocessors, which students in his class rely on, is a good example. The hardware tactics that Miriam Leeser mentioned also fit into this category. -mark aagaard aagaard@cs.ubc.ca @inproceedings{[AL94], author = {Aagaard, Mark D. and Leeser, Miriam E.}, title = {Reasoning About Pipelines with Structural Hazards}, booktitle = tpcd-94, year = 1994, month = sep, publisher = springer-verlag, editor = {Kumar, Ramayya and Kropf, Kumar}, } Available by ftp as ftp://tesla.ee.cornell.edu/pub/hw-verify/pipes-tpcd94.ps.Z [Hsu93] http://www.mips.com/HTMLs/r8000_docs/Micro_Paper/R8000_Micro_Paper_cv.html