Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Report on the International Workshop on Formal Methods in VLSI Design, Miami, January 9-11, 1991

Report on the International Workshop on Formal Methods in VLSI Design, Miami, January 9-11, 1991 UNION D E P A R T M E N T OF ELECTRICAL ENGINEERING A N D C O M P U T E R SCIENCE ......... C O L L E G E FOUNDED 179~ S T E I N M E T Z HALL S C H E N E C T A D Y , N E W YORK 12308-2311 (518) 370-6270 Report on the International Workshop on Formal Methods in VLSI Design Miami, January 9-11, 1991 David Hemmendinger hemmendd@tardis.union.edu This workshop, sponsored by the ACM SIGDA, together with the IFIP WG-10.2 and the IEEE TC on VLSI, included 27 papers, 4 surveys and panel discussions, and about 10 poster presentations in two and a half days. The sessions covered the now-ubiquitous binary decision diagrams and verification by means of model-checking, finite-state automata, the relationship among design, theorem proving and CAD, higher order logic in hardware design, timing issues in design, and algebraic techniques. The sessions on BDD's and model checking showed that the combination of well-designed data-structures, good algorithms, and faster processors permit the automatic verification of finitestate systems far beyond what one might have expected a few years ago C 1020 states and beyond", to quote one paper title). As one who is interested in possible methods for combining formal verification with VHDL, I found the paper "VHDL verification in the State Delta Verification System" particularly interesting. The discussions of VHDL that occurred several times during the workshop produced criticisms of the language for its complexity, but several other papers made at least passing reference to combining VHDL and formal methods. Sessions on the uses of theorem-provers (Boyer-Moore, Nuprl) and proof-checkers (HOL) focused on the real achievements of these tools and the work still required to make them useful for design. The latter includes the development of much better user interfaces and closer focus on the kinds of problems that designers actually encounter. A major subject of the discussions was the need to bring users of CAD and of formal verification tools together to learn more about the needs and capabilities of each side. I found these discussions one of the merits of the workshop. Several opened with (scheduled) provocative statements by workers in theorem proving (Warren Hunt) and CAD (Kurt Keutzer). If anything, we could have used more discussion time; the program was very full and some of the time allocated for general discussion was consumed by the comments following each paper. Another valuable feature was the poster session; I hope that workshops will increase the role of such sessions, which are a very good, though less prestigious, way to present information and obtain responses. My thanks to SIGDA for the travel grant that enabled me to attend the workshop. SIGDA Newsletter, vol 21, number I http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png ACM SIGDA Newsletter Association for Computing Machinery

Report on the International Workshop on Formal Methods in VLSI Design, Miami, January 9-11, 1991

Hemmendinger, David
ACM SIGDA Newsletter , Volume 21 (1) – Jun 1, 1991
Download PDF
1 page

Loading next page...
 
/lp/association-for-computing-machinery/report-on-the-international-workshop-on-formal-methods-in-vlsi-design-Oq60FZ7Dly
Publisher
Association for Computing Machinery
Copyright
Copyright © 1991 by ACM Inc.
ISSN
0163-5743
DOI
10.1145/126990.127001
Publisher site
See Article on Publisher Site

Abstract

UNION D E P A R T M E N T OF ELECTRICAL ENGINEERING A N D C O M P U T E R SCIENCE ......... C O L L E G E FOUNDED 179~ S T E I N M E T Z HALL S C H E N E C T A D Y , N E W YORK 12308-2311 (518) 370-6270 Report on the International Workshop on Formal Methods in VLSI Design Miami, January 9-11, 1991 David Hemmendinger hemmendd@tardis.union.edu This workshop, sponsored by the ACM SIGDA, together with the IFIP WG-10.2 and the IEEE TC on VLSI, included 27 papers, 4 surveys and panel discussions, and about 10 poster presentations in two and a half days. The sessions covered the now-ubiquitous binary decision diagrams and verification by means of model-checking, finite-state automata, the relationship among design, theorem proving and CAD, higher order logic in hardware design, timing issues in design, and algebraic techniques. The sessions on BDD's and model checking showed that the combination of well-designed data-structures, good algorithms, and faster processors permit the automatic verification of finitestate systems far beyond what one might have expected a few years ago C 1020 states and beyond", to quote one paper title). As one who is interested in possible methods for combining formal verification with VHDL, I found the paper "VHDL verification in the State Delta Verification System" particularly interesting. The discussions of VHDL that occurred several times during the workshop produced criticisms of the language for its complexity, but several other papers made at least passing reference to combining VHDL and formal methods. Sessions on the uses of theorem-provers (Boyer-Moore, Nuprl) and proof-checkers (HOL) focused on the real achievements of these tools and the work still required to make them useful for design. The latter includes the development of much better user interfaces and closer focus on the kinds of problems that designers actually encounter. A major subject of the discussions was the need to bring users of CAD and of formal verification tools together to learn more about the needs and capabilities of each side. I found these discussions one of the merits of the workshop. Several opened with (scheduled) provocative statements by workers in theorem proving (Warren Hunt) and CAD (Kurt Keutzer). If anything, we could have used more discussion time; the program was very full and some of the time allocated for general discussion was consumed by the comments following each paper. Another valuable feature was the poster session; I hope that workshops will increase the role of such sessions, which are a very good, though less prestigious, way to present information and obtain responses. My thanks to SIGDA for the travel grant that enabled me to attend the workshop. SIGDA Newsletter, vol 21, number I

Journal

ACM SIGDA Newsletter – Association for Computing Machinery

Published: Jun 1, 1991

There are no references for this article.