Research Catalog

Title

Higher order logic and hardware verification / T. Melham.

Author

Melham, T. F. (Tom F.)

Publication

Cambridge ; New York : Cambridge University Press, 1993.

Items in the Library & Off-site

Details

Description

xiii, 165 pages : illustrations; 26 cm.

Series Statement

Cambridge tracts in theoretical computer science ; 31

Uniform Title

Cambridge tracts in theoretical computer science ; 31.

Subject

• Integrated circuits > Very large scale integration > Data processing
• Logic, Symbolic and mathematical
• Integrated circuits > Very large scale integration > Data processing
• Logic, Symbolic and mathematical
• Hardwareverifikation
• Logik
• Verificatie
• Hardware
• Logica
• Integrated circuits > Very large scale integration > Design and construction
• Logic design
• Théorèmes > Démonstration automatique
• Circuits intégrés à très grande échelle > Informatique
• Logique symbolique et mathématique

Bibliography (note)

• Includes bibliographical references (p. [147]-157) and index.

Contents

• 1. Hardware Verification. 1.1. The hardware verification method. 1.2. Limitations of hardware verification. 1.3. Abstraction. 1.4. Hardware verification using higher order logic -- 2. Higher Order Logic and the HOL System. 2.1. Types. 2.2. Terms. 2.3. Sequents, theorems and inference rules. 2.4. Constant definitions. 2.5. The primitive constant [epsilon]. 2.6. Recursive definitions. 2.7. Type definitions. 2.8. The HOL system -- 3. Hardware Verification using Higher Order Logic. 3.1. Specifying hardware behaviour. 3.2. Deriving behaviour from structure. 3.3. Formulating correctness. 3.4. An example correctness proof. 3.5. Other approaches -- 4. Abstraction. 4.1. Abstraction within a model. 4.2. Two problems. 4.3. Abstraction in practice. 4.4. Validity conditions. 4.5. A notation for correctness. 4.6. Abstraction and hierarchical verification. 4.7. Abstraction between models. 4.8. Other approaches -- 5. Data Abstraction. 5.1. Defining concrete types in logic. 5.2. An example: a transistor model.
• 5.3. An example of data abstraction. 5.4. Reasoning about hardware using bit-vectors. 5.5. Reasoning about tree-shaped circuits. 5.6. Other approaches -- 6. Temporal Abstraction. 6.1. Temporal abstraction by sampling. 6.2. An example: abstracting to unit delay. 6.3. A synchronizing temporal abstraction. 6.4. A case study: the T-ring. 6.5. Other approaches -- 7. Abstraction between Models. 7.1. Representing the structure of CMOS circuits. 7.2. Defining the semantics of CMOS circuits. 7.3. Defining satisfaction. 7.4. Correctness in the two models. 7.5. Relating the models. 7.6. Improving the results. 7.7. Other approaches.

ISBN

• 052141718X
• 9780521417181

LCCN

94132457

OCLC

• ocm29596034
• 29596034
• SCSB-9334028

Owning Institutions

Princeton University Library