This book constitutes the refereed proceedings of the First International Conference on Formal Methods in Computer-Aided Design, FMCAD '96, held in Palo Alto, California, USA, in November 1996.
The 25 revised full papers presented were selected from a total of 65 submissions; also included are three invited survey papers and four tutorial contributions. The volume covers all relevant formal aspects of work in computer-aided systems design, including verification, synthesis, and testing.
Author(s): Kurt Keutzer (auth.), Mandayam Srivas, Albert Camilleri (eds.)
Series: Lecture Notes in Computer Science 1166
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1996
Language: English
Pages: 478
Tags: Computer Hardware; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Computer-Aided Engineering (CAD, CAE) and Design; Software Engineering
The need for formal methods for integrated circuit design....Pages 1-18
Verification of all circuits in a floating-point unit using word-level model checking....Pages 19-33
* BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions....Pages 34-48
Modular verification of multipliers....Pages 49-63
Verification of IEEE compliant subtractive division algorithms....Pages 64-78
Hierarchical verification of two-dimensional high-speed multiplication in PVS: A case study....Pages 79-93
Experiments in automating hardware verification using inductive proof planning....Pages 94-108
Verifying nondeterministic implementations of deterministic systems....Pages 109-125
A methodology for processor implementation verification....Pages 126-142
Coverage-directed test generation using symbolic techniques....Pages 143-158
Self-consistency checking....Pages 159-171
Inverting the abstraction mapping: A methodology for hardware verification....Pages 172-186
Validity checking for combinations of theories with equality....Pages 187-201
A unified approach for combining different formalisms for hardware verification....Pages 202-217
Verification using uninterpreted functions and finite instantiations....Pages 218-232
Formal verification of the Island Tunnel Controller using Multiway Decision Graphs....Pages 233-247
VIS....Pages 248-256
PVS: Combining specification, proof checking, and model checking....Pages 257-264
HOL Light: A tutorial introduction....Pages 265-269
A tutorial on digital design derivation using DRS....Pages 270-274
ACL2 theorems about commercial microprocessors....Pages 275-293
Formal synthesis in circuit design — A classification and survey....Pages 294-309
Formal specification and verification of VHDL....Pages 310-326
Specification of control flow properties for verification of synthesized VHDL designs....Pages 327-345
An algebraic model of correctness for superscalar microprocessors....Pages 346-361
Mechanically checking a lemma used in an automatic verification tool....Pages 362-376
Automatic generation of invariants in processor verification....Pages 377-388
A brief study of BDD package performance....Pages 389-403
Local encoding transformations for optimizing OBDD-representations of finite state machines....Pages 404-418
Decomposition techniques for efficient ROBDD construction....Pages 419-434
BDDs vs. Zero-Suppressed BDDs: for CTL symbolic model checking of Petri nets....Pages 435-449
HDL-based integration of formal methods and CAD tools in the PREVAIL environment....Pages 450-467
