System-on-Chip Protocol Compliance Verification Using Interval Property Checking

  • In recent years, formal property checking has become adopted successfully in industry and is used increasingly to solve the industrial verification tasks. This success results from property checking formulations that are well adapted to specific methodologies. In particular, assertion checking and property checking methodologies based on Bounded Model Checking or related techniques have matured tremendously during the last decade and are well supported by industrial methodologies. This is particularly true for formal property checking of computational System-on-Chip (SoC) modules. This work is based on a SAT-based formulation of property checking called Interval Property Checking (IPC). IPC originates in the Siemens company and is in industrial use since the mid 1990s. IPC handles a special type of safety properties, which specify operations in intervals between abstract starting and ending states. This paves the way for extremely efficient proving procedures. However, there are still two problems in the IPC-based verification methodology flow that reduce the productivity of the methodology and sometimes hamper adoption of IPC. First, IPC may return false counterexamples since its computational bounded circuit model only captures local reachability information, i.e., long-term dependencies may be missed. If this happens, the properties need to be strengthened with reachability invariants in order to rule out the spurious counterexamples. Identifying strong enough invariants is a laborious manual task. Second, a set of properties needs to be formulated manually for each individual design to be verified. This set, however, isn’t re-usable for different designs. This work exploits special features of communication modules in SoCs to solve these problems and to improve the productivity of the IPC methodology flow. First, the work proposes a decomposition-based reachability analysis to solve the problem of identifying reachability information automatically. Second, this work develops a generic, reusable set of properties for protocol compliance verification.
  • Verifikation von System-on-Chip-Protokollimplementierungen durch intervallbasierte Eigenschaftsprüfung

Volltext Dateien herunterladen

Metadaten exportieren

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:Duc-Minh Nguyen
URN (Permalink):urn:nbn:de:hbz:386-kluedo-23074
Betreuer:Wolfgang Kunz
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:2008
Jahr der Veröffentlichung:2008
Veröffentlichende Institution:Technische Universität Kaiserslautern
Titel verleihende Institution:Technische Universität Kaiserslautern
Datum der Annahme der Abschlussarbeit:16.01.2009
Datum der Publikation (Server):09.02.2009
Freies Schlagwort / Tag:Erreichbarkeit
GND-Schlagwort:Bounded Model Checking; Model checking; Protocol Compliance; Reachability; System-on-Chip; Verifikation
Fachbereiche / Organisatorische Einheiten:Fachbereich Elektrotechnik und Informationstechnik
DDC-Sachgruppen:6 Technik, Medizin, angewandte Wissenschaften / 620 Ingenieurwissenschaften und Maschinenbau
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011