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

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Duc-Minh Nguyen
URN:urn:nbn:de:hbz:386-kluedo-23074
Advisor:Wolfgang Kunz
Document Type:Doctoral Thesis
Language of publication:English
Year of Completion:2008
Year of first Publication:2008
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2009/01/16
Date of the Publication (Server):2009/02/09
Tag:Erreichbarkeit
GND Keyword:Verifikation; Bounded Model Checking; Model checking; System-on-Chip; Protocol Compliance; Reachability
Faculties / Organisational entities:Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
DDC-Cassification:6 Technik, Medizin, angewandte Wissenschaften / 620 Ingenieurwissenschaften und Maschinenbau
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011