Formal Methods in Computer-Aided Design
Subtitle: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1-3, 2000 Proceedings (Lecture Notes in Computer Science)
Contributors: Warren A. Jr. Hunt (Editor); Steven D. Johnson (Editor)
Edition: 1 edition
Publisher: Springer
Published: November 27, 2000
Language: eng
Format: Paperback
Number of pages: 539
ISBN-13: 9783540412199
Subjects: Computer aided design (CAD); Programming - Software Development; Computers; Software Engineering; Formal Language Theory; Computers - General Information; Integrated circuits; Computer Books: General; Artificial Intelligence - General; Robotics; Computers / Personal Computers & Microcomputers / General; Verification; Computer Science; Computer Engineering; Computer-aided design; Congresses
First sentence: The formal hardware verification effort at AMD has emphasized theorem proving using ACL2 [3], and has focused on the elementary floating-point operations.
Description: Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1–3, 2000 Proceedings<br />Author: Warren A. Hunt Jr., Steven D. Johnson<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-41219-9<br /> DOI: 10.1007/3-540-40922-X<br /><br />Table of Contents:<p></p><ul><li>Applications of Hierarchical Verification in Model Checking
</li><li>Trends in Computing
</li><li>A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon 
</li><li>An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps
</li><li>Automated Refinement Checking for Asynchronous Processes
</li><li>Border-Block Triangular Form and Conjunction Schedule in Image Computation
</li><li>B2M: A Semantic Based Tool for BLIF Hardware Descriptions
</li><li>Checking Safety Properties Using Induction and a SAT-Solver
</li><li>Combining Stream-Based and State-Based Verification Techniques
</li><li>A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
</li><li>Correctness of Pipelined Machines
</li><li>Do You Trust Your Model Checker?
</li><li>Executable Protocol Specification in ESL
</li><li>Formal Verification of Floating Point Trigonometric Functions
</li><li>Hardware Modeling Using Function Encapsulation
</li><li>A Methodology for the Formal Analysis of Asynchronous Micropipelines
</li><li>A Methodology for Large-Scale Hardware Verification
</li><li>Model Checking Synchronous Timing Diagrams
</li><li>Model Reductions and a Case Study
</li><li>Modeling and Parameters Synthesis for an Air TrafficManagement System</li></ul>