Correct hardware design and verification methods

Auteurs

• Daniel Geist

Paramètres

• Pages: 426 pages
• Temps de lecture: 15 heures

• Informatique, programmation
• Lecture notes in computer science

En savoir plus sur le livre

The content covers a range of topics in microprocessor and system design, including invited talks and tutorials on various specification languages and software verification techniques. Key discussions include the challenges of finding regularity in circuit analysis, predicate abstraction, and efficient symbolic model checking using partial disjunctive partitioning. Processor verification is explored through the functional verification of systems like VAMP and the analysis of memory ordering rules in Intel Itanium. Automata-based methods are examined, particularly in relation to nondeterministic Büchi automata and coverage metrics for formal verification. Short papers delve into optimized bounded model checking engines, constrained symbolic simulation, and semi-formal verification of memory systems. Specification methods are discussed, focusing on GSTE assertion graphs and enhancing efficiency in event sequence languages. Protocol verification is highlighted through the combination of symmetry reduction and symbolic representation, as well as the correctness of intrusion-tolerant group communication protocols. Additional short papers address the design of abstract interpreters for VHDL, operand forwarding analysis, and the integration of RAM and disk-based verification. Theorem proving techniques, including inductive assertions and operational semantics, are also presented. Bounded model checking and its efficiency in distrib

Achat du livre

• Année de publication: 2003
• Reliure: (souple)