+612 9045 4394
 
CHECKOUT
Formal Methods in Computer-Aided Design : Second International Conference, Fmcad '98, Palo Alto, Ca, Usa, November 4-6, 1998, Proceedings - Ganesh C. Gopalakrishnan

Formal Methods in Computer-Aided Design

Second International Conference, Fmcad '98, Palo Alto, Ca, Usa, November 4-6, 1998, Proceedings

Paperback

Published: 21st October 1998
Ships: 5 to 9 business days
5 to 9 business days
$158.39
or 4 easy payments of $39.60 with Learn more
if ordered within

This volumecontains the proceedingsof the Second InternationalConferenceon Formal Methods in Computer-Aided Design (FMCAD'98), organized November 4-6, in Palo Alto, California, USA. The rst event of this series was organized byMandayamSrivasand Albert Camilleriin 1996 inPaloAlto. FMCAD, which evolved from the series Theorem Provers in Circuit Design (TPCD), strives to beapremierforumfordisseminatingresearchinFormalVeri cation(FV) me- ods for digital circuits and systems, including processors, custom VLSI circuits, microcode, andreactivesoftware.Inadditiontosigni cantcase-studiesandve- cationapproaches, FMCADalsoendeavorstorepresentadvancesinthedriving technologies for veri cation, including binary decision diagrams, model che- ing, symbolicreasoning(theorem proving), symbolicsimulation, andabstraction methods. Theconferenceincludedfourinvitedlectures.Theinvitedlecturesweregiven by Kenneth McMillan (Cadence Berkeley Labs) on Minimalist proof assistants: interactions of technology and methodology in formal system level veric ation, by Carl-Johan Seger on Formal methods in CAD from an industrial perspective, by Randal E. Bryant and Bwolen Yang on A performance study of BDD-based model checking, and by Amir Pnueli on Veric ation of data-insensitive circuits: an in-order-retirement case study. Of the 55 regular paper submissionsreceived, 27 were selected by the technical program committee for presentation at the conference. All four tools papers received were also selected. We gratefully acknowledge the services of the technical program comm- tee of FMCAD'98, which consisted of Adnan Aziz (Univ. of Texas at Austin, USA), AlanHu(Univ.ofBritishColumbia, Canada), Albert Camilleri(Hewlett- Packard, USA), CarlPixley(Motorola, USA), CarlosDelgadoKloos (Univ. C- los III de Madrid, Spain), Ching-TsunChou (Intel, USA), EduardCerny (Univ.

Minimalist Proof Assistants: Interactions of Technology an Methodology in Formal System Level Verificationp. 1
Reducing Manual Abstraction in Formal Verification of Out-of-Order Executionp. 2
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checkingp. 18
Solving Bit-Vector Equationsp. 36
The Formal Design of 1M-Gate ASICsp. 49
Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutationsp. 64
A Tutorial on Stalmarck's Proof Procedure for Propositional Logic Mary Sheeran and Gunnar Stalmarckp. 82
Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methodsp. 100
Bisimulation Minimization in an Automata-Theoretic Verification Frameworkp. 115
Automatic Verification of Mixed-Level Logic Circuitsp. 133
A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talkp. 149
Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraintsp. 167
Using MTBDDs for Composition and Model Checking of Real-Time Systemsp. 185
Formal Methods in CAD from an Industrial Perspectivep. 203
A Methodology for Automatic Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Toolp. 204
Combined Formal Post- and Presynthesis Verification in High Level Synthesisp. 222
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problemp. 237
A Performance Study of BDD-Based Model Checkingp. 255
Symbolic Model Checking Visualizationp. 290
Input Elimination and Abstraction in Model-Checkingp. 304
Symbolic Simulation of the JEM1 Microprocessorp. 321
Symbolic Simulation: An ACL2 Approachp. 334
Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Studyp. 351
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verificationp. 369
Formally Verifying Data and Control with Weak Reachability Invariantsp. 387
Generalized Reversible Rulesp. 403
An Assume-Guarantee Rule for Checking Simulationp. 421
Three Approaches to Hardware Verification: HOL, MDG, and VIS Comparedp. 433
An Instruction Set Process Calculusp. 451
Techniques for Implicit State Enumeration of EFSMsp. 469
Model Checking on Product Structuresp. 483
BDDNOW: A Parallel BDD Packagep. 501
Model-Checking VHDL with CVp. 508
Alexandria: A Tool for Hierarchical Verificationp. 515
PV: An Explicit Enumeration Model-Checkerp. 523
Author Indexp. 529
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540651918
ISBN-10: 3540651918
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 538
Published: 21st October 1998
Publisher: SPRINGER VERLAG GMBH
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 2.82
Weight (kg): 0.76