1.

Record Nr.

UNISA996465485203316

Titolo

Formal Hardware Verification [[electronic resource] ] : Methods and Systems in Comparison / / edited by Thomas Kropf

Pubbl/distr/stampa

Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997

ISBN

3-540-69577-X

Edizione

[1st ed. 1997.]

Descrizione fisica

1 online resource (XII, 376 p.)

Collana

Lecture Notes in Computer Science, , 0302-9743 ; ; 1287

Disciplina

621.39/5

Soggetti

Computer engineering

Computer hardware

Computer logic

Mathematical logic

Computer Engineering

Computer Hardware

Logics and Meanings of Programs

Mathematical Logic and Formal Languages

Lingua di pubblicazione

Inglese

Formato

Materiale a stampa

Livello bibliografico

Monografia

Note generali

Bibliographic Level Mode of Issuance: Monograph

Nota di contenuto

Symbolic trajectory evaluation -- Automated verification with abstract state machines using multiway decision graphs -- Design verification using Synchronized Transitions -- Hardware verification using PVS -- Verifying VHDL designs with COSPAN -- The C@S system: Combining proof strategies for system verification -- Appendix: The common book examples.

Sommario/riassunto

This state-of-the-art monograph presents a coherent survey of a variety of methods and systems for formal hardware verification. It emphasizes the presentation of approaches that have matured into tools and systems usable for the actual verification of nontrivial circuits. All in all, the book is a representative and well-structured survey on the success and future potential of formal methods in proving the correctness of circuits. The various chapters describe the respective approaches supplying theoretical foundations as well as taking into account the application viewpoint. By applying all methods



and systems presented to the same set of IFIP WG10.5 hardware verification examples, a valuable and fair analysis of the strenghts and weaknesses of the various approaches is given.