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
|
