Hardware verification

Hardwareverifikation

Seminar im Sommersemester 1998
Vorbesprechung: Donnerstag, 12. Februar 1998, 9:15, Haus II, Preußerstr. 1-9
Termin: Freitags, 10:00 ct, im Raum
Stundenzahl: 2

Inhalt

Die vergangenen 50 Jahre brachten dramatische Leistungssteigerungen von Computern. Sie wurden durch die Fortschritte im Entwurf und der Realisierung digitaler Hardware ermöglicht. Die Komplexität moderner Schaltungen stellt eine Herausforderung für die formalen Methoden der Informatik dar. Die Verifikation derartiger Systeme ist umso wichtiger, als daß digitale Schaltungen in immer weitere Bereiche des täglichen Lebens eindringen und auch sicherheitskritische Aufgaben übernehmen.

Das Seminar soll in die fundamentalen Techniken des Entwurfs komplexer Hardwaresysteme einführen, mit Schwerpunkt auf die formale Behandlung und Verifikation von Hardwarekomponenten:

Logikdesign
Abstraktionsebenen der Hardwarebeschreibung und Verfeinerung
Formale Spezifikation von Hardware-Systemen
Verifikation von Hardware-Komponenten

Das Seminar wird sich in der Hauptsache auf ausgewählte Kapitel des Buches `` Reasoning about Parallel Architectures'', William. W. Collier, 1992, Prentice-Hall stützen.

Die Methoden dieses Buches wurden in einem Werkzeug (Archtest) zum Testen von shared-memory Multiprozessorarchitekturen umgesetzt. Eigenschaften, die sich damit untersuchen lassen, sind sequentielle Korrektheit, Cachekohärenz, ``out-of-order''-Ausführungen und Ähnliches.

Dies ist die vorläufige Verteilung der Vorträge:

Einführung	Martin Steffen	8. Mai
Einführung II	Martin Steffen	15. Mai
Programmordnung und Atomarizität (6-7)	Jan Paul	22. Mai
Synchronisation u. Intrastatement-Ordnung (8-10)	Kord Ehmcke	5. Juni
Ununterscheidbare Architekturen (10-12)	Mario Thies	19. Juni
Symbolic Trajectory Evaluation	Andreas Wortmann	26. Juni
``Out-of-order''-Execution, Damm/Pnueli	Marcel Kyas	3. Juli

Literatur & Hintergrundinformation

Computer Architectures: A quantitative Approach, J. L. Hennessy and D. A. Patterson; Morgan Kaufmann Publishers, 1990, San Mateo, CA, USA Ein Standardlehrbuch zum Thema Computerarchitektur. Das Buch ist am Lehrstuhl vorhanden.
Contemporary Logic Design, Randy H. Katz, University of California, Benjamin Cummings/Addison Wesley Publishing Company, 1993
A Formal Approach to Hardware Design, Jørgen Staunstrup", Kluwer Academic Publishers, 1994 Formaler Ansatz zur Beschreibung, Synthese, Analyse und Verifikation von Harwdare mittels ``Synchronized Transitions'', einer Beschreibungssprache für HW-Berechnungen.
Thomas Kropf (Ed.), Formal Hardware Verification, Methods and Systems in Comparisons, LNCS1287
Symbolic Trajectory Evaluation
Verification with Abstract State Machines using MDG's
Design Verification using Synchronized Transitions
Hardware Verification using PVS
Verifying VHDL-Designs with COSPAN
The C@S-System aktueller Sammelband mit unterschiedlichen Beiträgen und Tools zum Thema Hardwareverifikation
V. Stavridou, T. F. Melham and R. T. Boute (eds.), Theorem Provers in Circuit Design: Proceedings of the IFIP TC10/WG 10.2 International Conference, Nijmegen, June 1992, IFIP Transactions A-10 (North-Holland, 1992).
Sammelband mit einigen Papieren zur Hardwarverifikation mittels Theorembeweisern , insbesondere HOL-Theorembeweiser (Higher-Order Logic). (Sieheauch hier.
Shared Memory Consistency Models: A Tutorial, S. Adve and K. Gharachorloo
Ein Einführungsartikel über Speicherkonsistenz paralleler Architekturen.

Ein paar weitere Links

Hardware verification an der Technical University of Denmark
Hardware verification group an der Universität Cambridge
Hardware Verification Group in Karlsruhe
Ein paar Hardwareverifikationspapiere von der Universität Stanford
CMU-Seite über Modelchecking
A bunch of hardware/software codesign papers at UC Berkeley
Here is a computer system verification course provided by
Brigham Young University, they also prepared a long reading list
for graduate students
Die sehr umfangreiche Seite über Formale Methoden im allgemeinen der Universität Oxford
Formale Methoden der Uni Freiburg
Ein Sammelband über Verifikation (automatisch oder mittels Theorembeweisern) teilweise auch über Hardwareverifikation
Werner Damm und Amir Pnueli , Verifying Out-of-Order Executions , Technical Report, Weizmann-Institute, 1997 Der Artikel behandelt die gleiche Fragestellung - Korrektheit von durchmischten Ausführungen auf parallelen Architekturen - wie das Buch von Collier
``The Notion of Proof in Hardware Verification'', Avra Cohn.
Journal of Automated Reasoning, 5:127-139, 1989.
Guter Übersichtsartikel, leider bereits knapp 10 Jahre alt.
``Incremental Design and Formal Verification of Microcoded Microprocessors"'', John Herbert, University of Cambridge Report,
Thomas Melham . Abstraction Mechanisms for Hardware Verification
VLSI Specification, Verification and Synthesis, G. Birtwhistle and P. A. Subrahmanyam, editors, Kluwer Academic Publishers, 1988.
STeP -Modelchecker
Modeling a Hardware Synthesis Methodology in Isabelle. David Basin und Stefan Friedrich. To appear in The Journal of Formal Methods in Systems Design. (Informationen über den Theorembeweiser Isabelle finden sich hier.
M. Mendler, ``A Timing Refinement of Intuitionistic Proofs and its Application to the Timing Analysis of Combinational Circuits'', proceedings Tableaux '96.
Das Verilog-Projekt
Formale Verifikation einer ATM-Switches
Matt Fairtlough, Formal Design of Synchronous Concurrent Algorithms (Verifikation in Lego)
Sieben Mythen und weitere sieben Mythen über formale Methoden, eine davon über Hardwareverifikation
Eine Seite über Hardwareverifikation wäre ohne Hinweis auf den Viper-Chip nicht vollständig: `the first commercially available microprocessor with a proven correct design''..... ( The Independent, 28 May 1991 )
Die Anstrengungen, einen formal verifizierten Chip für sicherheitskritische Anwendungen (bzw. das Militär) zu entwickeln, waren sehr einflußreich und regten unterschiedliche Forschungen auf dem Gebiet formaler Methoden an (beispielsweise HOL). Hier ein kleiner Zeitungsartikel darüber, was aus dem Viper-Chip wurde. Siehe auch die weiteren Beiträge aus dem Risk-Forum: 7(98) (1988), 7(36)(1988) und 10(15) (1990). (Weitere Links zum Thema Viper-Microprozessor: Compilerverifikation für den Viper)
Eine erstaunliche Anzahl von Arbeiten zum Thema Hardware-Verifikation finden sich auf dem Server der Computational Logic, Inc., Austin, Texas
Hardware Verification using Monadic Second-Order Logic. David Basin und Nils Klarlund, CAV'95
Extracting Circuits from Constructive Proofs.
IFIP-IEEE International Workshop on: Formal Methods in VLSI Design, Miami USA, January 1991.
Formally Verified Synthesis of CMOS.
With Geoffrey Brown and Miriam Leeser. Proceedings of the IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Leuven Belgium, November 1989, North-Holland, 1990.

Anmeldung und Teilnahme

rechtzeitig

Sonstiges

Hinweise von einem Profi zur Vortragsgestaltung

Bei Fragen, email an ms@informatik.uni-kiel.de

Maintained by: Martin Steffen

Last modified: Februar 1998