Ramdan Hours:
Sun - Thu
9.30 AM - 2.30 PM
Iftar in --:--:--
🌙 Maghrib: --:--

Introduction to formal hardware verification / (Record no. 2412)

MARC details
000 -LEADER
fixed length control field 02701nam a22003734i 4500
001 - CONTROL NUMBER
control field 11768717
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20210222114549.0
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 990812s1999 gw a f b 001 0 eng d
010 ## - LIBRARY OF CONGRESS CONTROL NUMBER
LC control number 99012500
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 3540654453 (acidfree paper)
035 ## - SYSTEM CONTROL NUMBER
System control number (DLC) 99012500
040 ## - CATALOGING SOURCE
Original cataloging agency DLC
Transcribing agency DLC
Modifying agency DLC
Description conventions rda
042 ## - AUTHENTICATION CODE
Authentication code pcc
082 00 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 621.395
Edition number 21
Item number K.T.I.
100 1# - MAIN ENTRY--PERSONAL NAME
Personal name Kropf, Thomas,
Dates associated with a name 1961-,
9 (RLIN) 9944
Relator term author.
245 10 - TITLE STATEMENT
Title Introduction to formal hardware verification /
Statement of responsibility, etc Thomas Kropf.
264 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc Berlin ;
-- New York :
Name of publisher, distributor, etc Springer,
Date of publication, distribution, etc [1999]
264 #4 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Date of publication, distribution, etc ©1999
300 ## - PHYSICAL DESCRIPTION
Extent ix, 299 pages :
Other physical details illustrations ;
Dimensions 25 cm
336 ## - CONTENT TYPE
Source rdacontent
Content type term text
337 ## - MEDIA TYPE
Source rdamedia
Media type term unmediated
338 ## - CARRIER TYPE
Source rdacarrier
Carrier type term volume
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc Includes bibliographical references (pages [277]-289) and index.
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Introduction -- Setting the Context -- Circuit Design -- Fighting Design Errors -- Verification versus Validation -- Hardware Verification -- The Success of Formal Hardware Verification -- Limitations of Formal Hardware Verification -- The Pragmatic Approach: Recipes for Verifying Circuits -- Summary -- Structure of the Book -- Literature.- Boolean Functions. Motivation -- Representations for Boolean Functions -- Modeling Hardware Behavior -- Specification, Proof Goals and Proof -- Further Developments and Tools -- Technical Details -- Summary.- Finite State Machine Based Approaches. Motivation -- Formal Basics -- Modeling Hardware Behavior -- Specification, Proof Goal and Proof -- Further Developments -- Summary.- Propositional Temporal Logics. Motivation -- Formal Basics -- Modeling Hardware Behavior -- Specification, Proof Goal and Proof -- Further Developments -- Technical Details -- Summary.- Higher Order Logic. Motivation -- Formal Basics -- Modeling Hardware Behavior -- Specification and Proof -- Performing Proofs -- Technical Details -- Conclusion.- Appendix A: Mathematical Basics -- Appendix B: Axioms and Rules for CTL* -- Appendix C: Axioms and Rules for Higher Order Logic.- References.- Index
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Integrated circuits
General subdivision Very large scale integration
-- Computer-aided design.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Integrated circuits
General subdivision Verification.
856 42 - ELECTRONIC LOCATION AND ACCESS
Materials specified Publisher description
Uniform Resource Identifier <a href="http://www.loc.gov/catdir/enhancements/fy0816/99012500-d.html">http://www.loc.gov/catdir/enhancements/fy0816/99012500-d.html</a>
856 41 - ELECTRONIC LOCATION AND ACCESS
Materials specified Table of contents only
Uniform Resource Identifier <a href="http://www.loc.gov/catdir/enhancements/fy0816/99012500-t.html">http://www.loc.gov/catdir/enhancements/fy0816/99012500-t.html</a>
906 ## - LOCAL DATA ELEMENT F, LDF (RLIN)
a 7
b cbc
c orignew
d 1
e ocip
f 19
g y-gencatlg
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Source of classification or shelving scheme Dewey Decimal Classification
Koha item type Books
Holdings
Lost status Source of classification or shelving scheme Damaged status Not for loan Collection code Home library Current library Shelving location Date acquired Source of acquisition Inventory number Total Checkouts Full call number Barcode Date last seen Price effective from Koha item type
  Dewey Decimal Classification     Faculty of Engineering & Technology (Electrical) Main library Main library B3 10/08/2008 Academic bookshop DO   621.395 K.T.I. 00003791 19/02/2025 21/09/2010 Books