Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1-3, 2000 Proceedings

כריכה קדמית
Warren A. Jr. Hunt, Steven D. Johnson
Springer, 29 בנוב׳ 2007 - 552 עמודים
The biannual Formal Methods in Computer Aided Design conference (FMCAD 2000)is the third in a series of conferences under that title devoted to the use of discrete mathematical methods for the analysis of computer hardware and so- ware. The work reported in this book describes the use of modeling languages and their associated automated analysis tools to specify and verify computing systems. Functional veric ation has become one of the principal costs in a modern computer design e ort. In addition,verica tion of circuit models, timing,power, etc., requires even more eo rt. FMCAD provides a venue for academic and - dustrial researchers and practitioners to share their ideas and experiences of using discrete mathematical modeling and veric ation. It is noted with interest by the conference chairmen how this area has grown from just a few people 15 years ago to a vibrant area of research, development, and deployment. It is clear that these methods are helping reduce the cost of designing computing systems. As an example of this potential cost reduction, we have invited David Russino of Advanced Micro Devices, Inc. to describe his veric ation of ?oating-point - gorithms being used in AMD microprocessors. The program includes 30 regular presentations selected from 63 submitted papers.
 

תוכן

Trends in Computing
1
The Floating Point Adder of the AMD AthlonTM Processor
3
An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps
37
Automated Refinement Checking for Asynchronous Processes
55
BorderBlock Triangular Form and Conjunction Schedule in Image Computation
73
A Semantic Based Tool for BLIF Hardware Descriptions
91
Checking Safety Properties Using Induction and a SATSolver
108
Combining StreamBased and StateBased Verification Techniques
126
Model Reductions and a Case Study
299
Modeling and Parameters Synthesis foran Air Traffic Management System
316
MonitorBased Formal Specification of PCI
335
SATBased Image Computation with Application in Reachability Analysis
354
SATBased Verification without State Space Traversal
372
Scalable Distributed OntheFly Symbolic Model Checking
390
The Semantics of Verilog Using Transition System Combinators
405
Sequential Equivalence Checking by Symbolic Simulation
423

A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
143
Correctness of Pipelined Machines
161
Do You Trust Your Model Checker?
179
Executable Protocol Specification in ESL
197
Formal Verification of Floating Point Trigonometric Functions
217
Hardware Modeling Using Function Encapsulation
234
A Methodology for the Formal Analysis of Asynchronous Micropipelines
246
A Methodology for LargeScale Hardware Verification
263
Model Checking Synchronous Timing Diagrams
283
Speeding Up Image Computation by Using RTL Information
443
Symbolic Checking of SignalTransition Consistency for Verifying HighLevel Designs
455
Symbolic Simulation with Approximate Values
470
A Theory of Consistency for Modular Synchronous Systems
486
Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined DeductiveAlgorithmic Methods
505
Visualizing System Factorizations with Behavior Tables
520
Author Index
538
זכויות יוצרים

מהדורות אחרות - הצג הכל

מונחים וביטויים נפוצים

מידע ביבליוגרפי