Die Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Verwaltung des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Mathematik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Universität Bremen


INHALT & PFAD:
Startseite Detail


Vermeidung von False-Negatives bei formaler Hardware Verifikation



Datum: 15.08.2011
Uhrzeit: 16 Uhr c.t.

Ort: Cartesium Rotunde


Vortragende(r): Prof. Peer Johannsen (Hochschule Pforzheim)

Abstract:

Im Entwurfsprozess digitaler Schaltkreise entfallen heutzutage 60% - 70% des Aufwandes auf die funktionale Verifikation. Neben herkömmlicher Simulation setzt die Industrie hierbei immer stärker auch auf formale Techniken, um mit der beständig wachsenden Komplexität moderner Mikro-Chips umgehen zu können. Jüngste Fortschritte in den Kerntechnologien formaler Beweise, die Standardisierung von Assertion-Sprachen wie z.B. SVA, und der Reifegrad und die Benutzerfreundlichkeit heutiger kommerzieller Tools haben formale Methoden mittlerweile zum unverzichtbaren Bestandteil der Verifikation von VHDL oder Verilog Entwürfen gemacht.

Beim SAT oder BDD basierten formalen Property Checking können unerreichbare Gegenbeispiele jedoch das erfolgreiche Beweisen einer Schaltkreiseigenschaft verhindern. In Verifikationsprojekten besteht ein Großteil der Arbeit aus Erreichbarkeitsanalyse und aus manueller iterativer Anwendung von Methodik zum Ausschluß von False-Negatives, wie z.B. Inductive Proof Reasoning, Assumption Strengthening und Invariant Generation. Dieses ist zeitauwändig und setzt das Expertenwissen eines Verifikationsingenieurs voraus und erschwert so einen frühen Einsatz formaler Verifikation im Entwurfsprozess durch den Chip-Designer selbst.



Der Vortrag stellt einen Ansatz vor, Erreichbarkeits-Methodik beim Property Checking so zu automatisieren und in den Beweisprozess des Verifikationstools zu verlagern, dass dem Benutzer eine weitgehende Push-Button Lösung zur Verfügung gestellt wird. Gleichzeitig erlaubt es dieser Ansatz, Erreichbarkeitsinformation nicht nur auf der Ebene der Properties, sondern auch inkrementell auf der Ebene des SAT Checkers auszunutzen.



Bio:

Peer Johannsen ist Professor für Informatik und Software-Engineering im Bereich Informationstechnik an der Hochschule Pforzheim. Er hat an der Christian-Albrechts-Universität zu Kiel über Formale Hardware-Verifikation promoviert. Die Dissertation ist in Zusammenarbeit mit Siemens in München und Infineon, USA, entstanden. Anschließend hat er von 2004 bis 2010 bei OneSpin Solutions an der Entwicklung des formalen Verifikationstools 360 MV gearbeitet, bevor er 2010 an die Hochschule Pforzheim wechselte. Zu seinen Forschungs- und Lehrgebieten gehören neben der Hardware Verifikation die Theoretische Informatik, sowie Algorithmen und Datenstrukturen.









zurück  

Seitenanfang  -  Impressum Zuletzt geändert durch: birgit [b]   09.08.2011 Admin-Login