This book constitutes the refereed proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, FMCAD '98, held in Palo Alto, California, USA, in November 1998.
The 27 revised full papers presented were carefully reviewed and selected from a total of 55 submissions. Also included are four tools papers and four invited contributions. The papers present the state of the art in formal verification methods for digital circuits and systems, including processors, custom VLSI circuits, microcode, and reactive software. From the methodological point of view, binary decision diagrams, model checking, symbolic reasoning, symbolic simulation, and abstraction methods are covered.
Author(s): Kenneth L. McMillan (auth.), Ganesh Gopalakrishnan, Phillip Windley (eds.)
Series: Lecture Notes in Computer Science 1522
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1998
Language: English
Pages: 538
Tags: Computer Hardware; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Systems and Information Theory in Engineering
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification....Pages 1-1
Reducing Manual Abstraction in Formal Verification of Out- of- Order Execution....Pages 2-17
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking....Pages 18-35
Solving Bit-Vector Equations....Pages 36-48
The Formal Design of 1M-Gate ASICs....Pages 49-63
Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations....Pages 64-81
A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic....Pages 82-99
Almana: A BDD Minimization Tool Integrating Heuristic and RewritingMethods....Pages 100-114
Bisimulation Minimization in an Automata-Theoretic Verification Framework....Pages 115-132
Automatic Verification of Mixed-Level Logic Circuits....Pages 133-148
A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk....Pages 149-166
Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints....Pages 167-184
Using MTBDDs for Composition and Model Checking of Real-Time Systems....Pages 185-202
Formal Methods in CAD from an Industrial Perspective....Pages 203-203
A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool....Pages 204-221
Combined Formal Post- and Presynthesis Verification in High Level Synthesis....Pages 222-236
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem....Pages 237-254
A Performance Study of BDD-Based Model Checking....Pages 255-289
Symbolic Model Checking Visualization....Pages 290-302
Input Elimination and Abstraction in Model Checking....Pages 304-320
Symbolic Simulation of the JEM1 Microprocessor....Pages 321-333
Symbolic Simulation: An ACL2 Approach....Pages 334-350
Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study....Pages 351-368
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification....Pages 369-386
Formally Verifying Data and Control with Weak Reachability Invariants....Pages 387-402
Generalized Reversible Rules....Pages 403-419
An Assume-Guarantee Rule for Checking Simulation....Pages 421-431
Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared....Pages 433-450
An Instruction Set Process Calculus....Pages 451-468
Techniques for Implicit State Enumeration of EFSMs....Pages 469-481
Model Checking on Product Structures....Pages 483-500
BDDNOW: A Parallel BDD Package....Pages 501-507
Model Checking VHDL with CV....Pages 508-514
Alexandria: A Tool for Hierarchical Verification....Pages 515-522
PV: An Explicit Enumeration Model-Checker....Pages 523-528
