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 |