Formale Verifikation von SoC Protokollimplementierungen

Abstract:
Bei der formalen Verifikation von Kommunikationsstrukturen von System on Chip (SoC) Entwürfen werden Erreichbarkeitsbedingungen benötigt, um false negatives zu eliminieren, die beim bounded interval model checking (BIMC) auftreten können. In der industriellen Praxis müssen diese unter hohem Aufwand manuel ermittelt werden. Zur zielgerichteten automatischen Generierung dieser Bedingungen schlagen wir eine optimierte Implementierung der approximativen Transition-by-Transition FSM Traversierung vor. Durch den Einsatz von BDDs wird hier sowohl die Laufzeit als auch die Genauigkeit der berechneten Erreichbarkeitsbedingungen verbessert.