Formal VLSI correctness verification : proceedings of the IFIP WG 10.2/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design
Author(s)
Bibliographic Information
Formal VLSI correctness verification : proceedings of the IFIP WG 10.2/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design
(VLSI Design methods, v. 2)
North-Holland , Distributed in the U.S. and Canada, Elsevier Science Pub. Co., 1990
Available at 10 libraries
  Aomori
  Iwate
  Miyagi
  Akita
  Yamagata
  Fukushima
  Ibaraki
  Tochigi
  Gunma
  Saitama
  Chiba
  Tokyo
  Kanagawa
  Niigata
  Toyama
  Ishikawa
  Fukui
  Yamanashi
  Nagano
  Gifu
  Shizuoka
  Aichi
  Mie
  Shiga
  Kyoto
  Osaka
  Hyogo
  Nara
  Wakayama
  Tottori
  Shimane
  Okayama
  Hiroshima
  Yamaguchi
  Tokushima
  Kagawa
  Ehime
  Kochi
  Fukuoka
  Saga
  Nagasaki
  Kumamoto
  Oita
  Miyazaki
  Kagoshima
  Okinawa
  Korea
  China
  Thailand
  United Kingdom
  Germany
  Switzerland
  France
  Belgium
  Netherlands
  Sweden
  Norway
  United States of America
Note
Includes bibliographical references
Description and Table of Contents
Description
Functional and behavioral verification of correctness forms the bottleneck in current VLSI design systems. For economical reasons, design of VLSI circuits must be completely validated before manufacturing. Current VLSI validation is mainly done through extensive simulation. The emerging alternative is based on formal design and verification methods that guarantee correctness. This book describes original work in all aspects of formal hardware design methods. Topics covered include high-level specification, hardware description languages, formal hardware verification methods, guided synthesis methods, correctness preserving transformations, use of theorem provers for verification, formal proof of correctness, MOS timing verification methods, design for verifiability, and practical experiences.
Table of Contents
MOS Circuit Level Verification. Efficient Tautology Checking Algorithms. Verification of Sequential Machines. Functionality Extraction, Comparison and Testing. Register Transfer Level Verification. Boyer-Moore Theorem Prover Based Verification. Hardware Verification Using HOL.
by "Nielsen BookData"