Debugging in der formalen Modulverifikation

Im Rahmen des vom BMBF geförderten Projektes VALSE-XT werden gemeinsam mit den Firmen Infineon Technologies AG und Concept Engineering GmbH neue Methoden zum Debugging in der formalen Modulverifikation entwickelt.

Kontakt: Prof. Dr. Rolf Drechsler

Hochautomatisierte, zertifizierende und skalierende Validierung von "System-on-Chip"-Entwürfen

SoCs ermöglichen fast unbegrenzte Produktinnovationen. Aber beim Entwurf solcher Chips wird die Verifikation zum begrenzenden Faktor. 60-80% der Entwurfsaufwände entfallen auf die Verifikation. Die Projektpartner von

VALSE-XT

gehen davon aus, dass die Unvollständigkeit der Simulation maßgeblich für das Verifikationsproblem verantwortlich ist. Die Simulation für wichtige Verifikationsaufgaben kann durch weit leistungsfähigere, spezialisierte Verfahren ersetzt werden, die massive Produktivitäts- und Qualitätsgewinne bringen. Aus dieser Arbeitshypothese wurden das Valse-Programm und insbesondere das Arbeitsprogramm für VALSE-XT abgeleitet. Es sieht vor:

• Die Technik der formalen Eigenschaftsprüfung zu einer erschöpfenden, hochautomatisierten Verifikation auszubauen,

• Die Korrektheit automatischer und händischer Entwurfsverfeinerungen für digitale Schaltungen und Analogzellen durch mathematische Äquivalenzvergleiche zu garantieren und

• Durch eine vollständige Betriebsfehleranalyse kostengünstig die Robustheit sicherheitskritischer Systeme gegen Betriebsfehler sicherzustellen.

Projektleitung:
Infineon Technologies AG
Prof. Dr. Wolfram Büttner

Projektpartner in Deutschland:
Concept Engineering GmbH
Infineon Technologies AG
Lucent Technologies Network Systems GmbH
Melexis GmbH
Robert Bosch GmbH

Forschungspartner:
Universität Bremen
Universität Darmstadt
Universität Freiburg
Universität Hannover
Universität Kaiserslautern
Universität Tübingen
FhG IIS/EAS Dresden
Konrad-Zuse-Zentrum Berlin