Formale Verifikation von Schaltkreisen unter Verwendung von Informationen der Hochsprachenebene

点击翻译按钮获取中文摘要

Im computergestützten Schaltkreisentwurf kommt der Verifikation des Entwurfes eine immer größere Bedeutung zu. Heutige Schaltungen bestehen aus bis zu 100 Millionen Transistoren. Durch Simulation kann die korrekte Funktionalität nicht mehr ausreichend gewährleistetwerden. Der Verifikationsanteil bei heutigen ASIC Projekten liegt im Mittel bei 60-70% - Tendenz steigend. Dies führte in den vergangenen Jahren zur Entwicklung von Verifikationsansätzen basierend auf formalen Methoden. Diese Verfahren lassen sich im Wesentlichen in zwei Bereiche einordnen: Äquivalenzvergleich (equivalence checking) Modellprüfung (model checking bzw. property checking). Während der Äquivalenzvergleich auf Schaltungen mit mehreren Millionen Gattern anwendbar ist, so zielt die Modellprüfung auf Beschreibungen der Modulebene mit bis zu 100.000 Gattern ab. Für beide Methoden sind kommerzielle Werkzeuge entwickelt worden, und diese werden auch im industriellen Umfeld verwendet. Diese Werkzeuge der ersten Generation haben jedoch Nachteile, die den Einsatz und die Handhabung erschweren. Die entstehenden Probleme sollen im Rahmen des Projektes untersucht werden: Verifikation unter Verwendung der Wortebene: Auch wenn die Schaltungen in einer Hardware-Beschreibungssprache, wie z.B. VHDL, gegeben sind, wird die Verifikation auf der Bit-Ebene, d.h. ohne Verwendung der Hochspracheninformation, durchgeführt. Bestimmung der erzielten Überdeckung: In der Modellprüfung werden die Verifikationsziele durch Eigenschaften beschrieben. Es gibt jedoch keine ausreichenden Ansätze, um die Qualität der Eigenschaftsmenge zu bestimmen. Im Bereich des bounded model checking sind die Fragestellungen stark mit der Berechnung der Erreichbarkeit von Zuständen bzw. Zustandsmengen in endlichen Automaten verbunden.Design for Verifiability: Ausgehend von den gewonnenen Erkenntnissen der obigen Ziele sollen Kriterien erarbeitet werden, wie leicht verifizierbare Schaltungen beschrieben werden können. In einem weiteren Schritt ergibt sich hieraus auch die Möglichkeit einen Synthesefluss zu beschreiben, der sich an der Verifikation bzw. der Verifizierbarkeit orientiert.