System-on-chip protocol compliance verification using interval property checking [Elektronische Ressource] = Verifikation von System-on-Chip-Protokollimplementierungen durch intervallbasierte Eigenschaftsprüfung / von Duc-Minh Nguyen

Informations

• Publié par: technische_universitat_kaiserslautern
• Publié le: 01 janvier 2009
• Nombre de lectures: 16
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

System-on-Chip Protocol Compliance Verification
Using Interval Property Checking
Verifikation von System-on-Chip-Protokollimplementierungen
durch intervallbasierte Eigenschaftspruf¨ ung
Vom Fachbereich Elektrotechnik und Informationstechnik
der Technischen Universita¨t Kaiserslautern
zur Erlangung des akademischen Grades
Doktor der Ingenieurwissenschaften (Dr.-Ing.)
genehmigte Dissertation
von
M.Sc. Duc-Minh Nguyen
geb. in Hanoi, Vietnam
D 386
Dekan: Univ.-Prof. Dr. Steven Liu
Gutachter: Prof. Dr.-Ing. Wolfgang Kunz,
Technische Universita¨t Kaiserslautern
Prof. Dr.-Ing. Hans Eveking,
Technische Unversita¨t Darmstadt
Datum der Disputation: 16 Januar 2009iiAcknowledgments
This thesis is the result of5 year work done at the Electronic Design Automation Group at
the University of Kaiserslautern. Additionally, the problem of false negatives in interval
property checking was discovered during a short but intensive stay at the Formal Verifica-
tion Section in Infineon Technologies AG, that is now OneSpin Solutions GmbH. There
are a numerous people who have contributed to this research in various ways and whom I
would like to thank.
First of all, I am deeply indebted to my advisor, Prof. Wolfgang Kunz. He has pro-
vided me not only the opportunity to work in very interesting research field but also con-
siderable guide and constant support during my long stay with his group. The ideas
described in this thesis were greatly enriched during the long, intensive discussions with
Wolfgang in which he has been very patient and encouraging.
I would like to thank Prof. Hans Eveking for reviewing this thesis and contributing
helpful feedback.
The industrial designs and the verification tool were provided by OneSpin Solutions
GmbH, Infineon, and Siemens, for which I appreciate. I owe special thanks to Dr. Klaus
Winkelmann for his first introduction of practical verification problems when I was at the
Formal Verification Section in Infineon.
I am very grateful to Dominik Stoffel, Markus Wedler for the time they spent proof-
reading and correcting my papers and also for their fruitful collaborations. Many thanks
to Max Thalmaier for helping to conduct experiments with the BDD-based algorithms. I
would like to thank Sacha Loitz for his proof reading of this thesis. Furthermore, I would
like to thank the other colleagues in the Design Automation Group in Kaiserslautern,
especially Ingmar Neumann, Evgeny Karibaev, Evgeny Pavlenko, Bernard Schmidt and
Carmen Vicente for the interesting fun talks and support.
I am indebted my mother and my Late father for their great personal sacrifices when
I was in Germany away from their difficulties. Last, but not least, I would like to thank
Chi, my wife, for her understanding and caring.
Nguyen Duc Minh Kaiserslautern, February 4th, 2009.
iiiTo my parentsContents
Acknowledgments iii
1 Introduction 1
1.1 Hardware Verification of System-on-Chip Designs . . . . . . . . . . . . 1
1.1.1 Equivalence Checking . . . . . . . . . . . . . . . . . . . . . . . 1
1.1.2 Property Checking . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.1.3 Block-based Verification of SoC Designs . . . . . . . . . . . . . 5
1.2 Motivation and Thesis Overview . . . . . . . . . . . . . . . . . . . . . . 6
2 Fundamentals 9
2.1 Graphs and Graph Algorithms . . . . . . . . . . . . . . . . . . . . . . . 9
2.1.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.1.2 Graph Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2 Representations of Boolean Functions . . . . . . . . . . . . . . . . . . . 13
2.2.1 Boolean Functions . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.2 Combinational Circuits . . . . . . . . . . . . . . . . . . . . . . . 15
2.2.3 Reduced Ordered Binary Decision Diagrams . . . . . . . . . . . 18
2.2.4 Conjunctive Normal Forms . . . . . . . . . . . . . . . . . . . . . 19
3 Model Checking 21
3.1 Models and Properties of Sequential Systems . . . . . . . . . . . . . . . 21
3.1.1 Models of Sequential Systems . . . . . . . . . . . . . . . . . . . 21
3.1.2 Property Languages . . . . . . . . . . . . . . . . . . . . . . . . 24
3.2 Symbolic Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.2.1 Introduction of Model Checking . . . . . . . . . . . . . . . . . . 27
3.2.2 Symbolic Model Checking . . . . . . . . . . . . . . . . . . . . . 28
3.2.3 State Space Explosion Problem . . . . . . . . . . . . . . . . . . 29
3.3 Improvements of Symbolic Model Checking . . . . . . . . . . . . . . . . 30
3.3.1 Improvement of Image Computation . . . . . . . . . . . . . . . . 30
3.3.2 Approximate FSM Traversal . . . . . . . . . . . . . . . . . . . . 31
3.3.3 Abstraction Refinement . . . . . . . . . . . . . . . . . . . . . . 35
3.4 Bounded Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . 39
vContents
4 Interval Property Checking 45
4.1 Properties in Interval Property Checking . . . . . . . . . . . . . . . . . . 45
4.1.1 Operational Interval Properties . . . . . . . . . . . . . . . . . . . 45
4.1.2 Interval Properties Based on the Main-FSM . . . . . . . . . . . . 48
4.2 Interval Property Checking . . . . . . . . . . . . . . . . . . . . . . . . . 50
5 Transition by Transition FSM Traversal 59
5.1 Decomposition of State Space and Transition Relation . . . . . . . . . . 59
5.1.1 Definition of the Main-FSM . . . . . . . . . . . . . . . . . . . . 59
5.1.2 Decomposition Using the Main-FSM . . . . . . . . . . . . . . . 60
5.2 Decomposing Using Sub-FSMs . . . . . . . . . . . . . . . . . . . . . . 65
5.2.1 Partitioning the Design into Sub-FSMs . . . . . . . . . . . . . . 65
5.2.2 Traversing Sub-FSMs . . . . . . . . . . . . . . . . . . . . . . . 68
5.3 SAT-based Implementation of TBT . . . . . . . . . . . . . . . . . . . . . 70
5.3.1 SAT-based Constrained Image Calculation . . . . . . . . . . . . . 70
5.3.2 SAT-based Constrained Support Set Calculation . . . . . . . . . . 72
5.4 TBT Traversal in IPC-based Verification Flow . . . . . . . . . . . . . . . 74
5.5 Comparison with Previous Work . . . . . . . . . . . . . . . . . . . . . . 76
5.5.1 Comparison with Improvements in Image Computation . . . . . . 76
5.5.2 Comparison with Approximative Reachability Analysis Methods . 76
5.5.3 Comparison with Abstraction Refinement Methods . . . . . . . . 76
5.5.4 Comparison with BMC-based Methods . . . . . . . . . . . . . . 77
5.6 Experimental Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.6.1 Design Characteristics . . . . . . . . . . . . . . . . . . . . . . . 77
5.6.2 Performance Measurements for TBT Traversal . . . . . . . . . . 78
5.6.3 Effect of Generated Reachability Constraints on IPC . . . . . . . 79
5.6.4 Comparison with Other Model Checking Techniques Using Ap-
proximation or Abstraction . . . . . . . . . . . . . . . . . . . . . 83
5.6.5 Comparison with Other Approximative Reachability Analysis Al-
gorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
6 Reuse Methodology for Protocol Compliance Verification 87
6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
6.1.1 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.1.2 Contribution of this Chapter . . . . . . . . . . . . . . . . . . . . 89
6.2 Recorder-FST and ITL Properties . . . . . . . . . . . . . . . . . . . . . 90
6.2.1 Recorder-FST . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
6.2.2 ITL Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
6.3 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
6.4 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
6.4.1 Recorders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
6.4.2 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
viContents
6.4.3 Verifying Compliance Based on a Recorder using IPC and Reach-
ability Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7 Summary and Future Work 107
7.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
7.1.1 Approximate TBT FSM Traversal for IPC Verification Flow . . . 108
7.1.2 Re-usable Properties and Generic Recorder . . . . . . . . . . . . 108
7.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
7.2.1 Identifying Reachability Invariants . . . . . . . . . . . . . . . . . 109
7.2.2 Applying Approximate FSM Traversal in Abstraction Refinement 111
8 Zusammenfassung (in Deutsch) 113
8.1 Approximative TBT FSM-Traversierung fu¨r IPC . . . . . . . . . . . . . 114
8.2 Wiederverwendbare Eigenschaften und generischer Recorder . . . . . . . 115
viiContents
viiiChapter 1
Introduction
1.1 Hardware Verification of System-on-Chip Designs
In present-day hardware design flow, one of the most challenging tasks is to guarantee that
designs are free of bugs. While design tools and technologies for system-on-chip (SoC)
and reusable Intellectual Property Components (IP cores) allow more complex hardware
systems to be designed effectively the verification methodologies are less effective. This
le