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
Verfasser*innenangaben: | Duc-Minh Nguyen |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-23074 |
Betreuer*in: | Wolfgang Kunz |
Dokumentart: | Dissertation |
Sprache der Veröffentlichung: | Englisch |
Jahr der Fertigstellung: | 2008 |
Jahr der Erstverö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: | Verifikation; Bounded Model Checking; Model checking; System-on-Chip; Protocol Compliance; Reachability |
Fachbereiche / Organisatorische Einheiten: | Kaiserslautern - 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 |