Formale Verifikation von SoC Protokollimplementierungen

Conference: Zuverlässigkeit und Entwurf - 1. GMM/GI/ITG-Fachtagung
03/26/2007 - 03/28/2007 at München

Proceedings: Zuverlässigkeit und Entwurf

Pages: 8Language: germanTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Authors:
Thalmaier, Max; Nguyen, Minh D.; Wedler, Markus; Stoffel, Dominik; Kunz, Wolfgang (Fachbereich Elektrotechnik und Informationstechnik, Technische Universität Kaiserslautern)

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.