Schaltungs- und Systemverifikation auf der Wort-Ebene

Im Rahmen des Projektes sollen Datenstrukturen sowohl theoretisch untersucht als auch praktisch erprobt werden, die es erlauben Strukturen auf der Wort-Ebene direkt im Verifikationsprozess zu verwenden.

Kontakt: Prof. Dr. Rolf Drechsler

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ährleistet werden. 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. Im Wesentlichen werden die Schaltungen nur auf der Bit-Ebene verifiziert, wobei die Beschreibungen der Schaltungen selbst auf der Wort-Ebene, d.h. unter Verwendung von Wort-Ebenen-Konstrukten, stattfindet. Im Rahmen des Projektes sollen Datenstrukturen sowohl theoretisch untersucht als auch praktisch erprobt werden, die es erlauben Strukturen auf der Wort-Ebene direkt zu verwenden.