Prof. Dr. rer. nat. Peer Johannsen

Material zur Vorlesung Formale Hardware Verifikation

Allgemeines

  • Studiengang Master Embedded Systems, 2. Semester
  • Wahlfach, 2 SWS, 3 ECTS
  • Die Vorlesung wird bis auf Weiteres im Online-Format stattfinden.
  • Bitte schreiben Sie sich in den zugehörigen Moodle Kurs ein.
  • Dort finden Sie die weitere Informationen.

Moodle Kurs und virtueller Hörsaal

Vorlesungstermine und Hinweise für Teilnehmer der TAE:

  • 21.03.2020, 09:00 - 17:00 Uhr, abgesagt!
  • 04.04.2020, 09:00 - 12:00 Uhr
  • Ein weiterer Halbtagestermin wird folgen und schnellstmöglich bekannt gegeben.
  • 16.05.2020, 09:00 - 17:00 Uhr, vorerst noch so geplant.
  • Bitte beachten Sie die weiteren Hinweise von Seiten der TAE!

Voranmeldung

  • Falls Sie an dieser Veranstaltung teilnehmen möchten, dann schicken Sie mir bitte frühestmöglich vorab eine unverbindliche E-Mail, damit ich die Teilnehmerzahl dieser Veranstaltung besser abschätzen kann. Bitte geben Sie hierbei Ihren Studiengang (MES bzw. TAE) an.

Funktionale Verifikation digitaler Schaltkreise

Im Entwurfsprozess digitaler Schaltkreise entfallen heutzutage 60% - 70% des Aufwandes auf die funktionale Verifikation. Da digitale Hardware verstärkt in sicherheitskritischen Bereichen zu finden ist, ist ein Nachweis korrekter Funktionalität im Vorfeld unabdingbar geworden. Solch ein Nachweis sollte frühestmöglich im Entwurfsprozess erfolgen, um teure Redesigns und Respins zu vermeiden.

Neben herkömmlicher Simulation setzt die Industrie hierbei immer stärker auf formale Verifikationstechniken, um mit der beständig wachsenden Komplexität moderner Mikro-Chips umgehen zu können. Unter formalen Techniken versteht man hier Methoden, die eine 100% Aussage über die funktionale Korrektheit eines Schaltkreises vor der eigentlichen Fertigung treffen können. Ausgangspunkt ist hierbei der Entwurf einer Schaltung in einer Hardwarebeschreibungssprache wie z.B. VHDL oder Verilog. Aufgrund der exponentiellen Komplexität der Anzahl der möglichen Stimuli einer Schaltung kann hierbei mittels Simulation immer nur ein vergleichsweise sehr kleiner Anteil des möglichen Schaltungsverhaltens überprüft werden. Formale Methoden sind in der Lage, Aussagen über das gesamte Schaltungsverhalten zu treffen, und können so funktionale Korrektheit vollständig beweisen bzw. durch Gegenbeispiele widerlegen. Der Einsatz solcher Methoden ist mittlerweile zum unverzichtbaren Bestandteil der Verifikation von VHDL oder Verilog Entwürfen geworden, und eine Bandbreite kommerzieller Software-Tools zur formalen Verifikation digitaler Schaltkreise wird mittlerweile in der industriellen Praxis eingesetzt.

Die wesentlichen Methoden, die hier Einsatz finden, werden bezeichnet als Equivalence Checking (Äquivalenzvergleich zweier Schaltungsentwürfe), Property Checking (Verifikation dedizierter Eigenschaften einer Schaltung) und als Assertion Based Verification (Überprüfen von Eigenschaften des VHDL oder Verilog Codes). Die formalen Techniken und Algorithmen, die hier eingesetzt werden, haben ihren Ursprung in der theoretischen Informatik und fundieren auf Verfahren wie z.B. Satisfiability Checking (SAT), Model Checking, oder Datenstrukturen zur Schaltkreisrepräsentation wie z.B. Binary Decision Diagrams (BDDs), und bieten ein breites Forschungsgebiet mit hochgradigem Bezug zur aktuellen industriellen Praxis.


Folien

Labor

  • Im Labor T2.2.07 stehen 8 Linux PCs zur Verfügung, auf denen jeweils eine Vollversion von OneSpin 360 DV installiert ist.
  • OneSpin 360 DV - Laboranleitung mit Reference-Manual und Übungsaufgaben
  • Quelldateien zu den Übungsaufgaben (lab.zip)

VHDL Beispiele

Letzte Änderung am 05.04.2020, 07:45 Uhr

  • Hinweise aktualisiert