Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring

Pirmais vāks
Springer Science & Business Media, 2008. gada 1. jūn. - 280 lappuses

Assertion-based design is a powerful new paradigm that is facilitating quality improvement in electronic design. Assertions are statements used to describe properties of the design (I.e., design intent), that can be included to actively check correctness throughout the design cycle and even the lifecycle of the product. With the appearance of two new languages, PSL and SVA, assertions have already started to improve verification quality and productivity.

This is the first book that presents an “under-the-hood” view of generating assertion checkers, and as such provides a unique and consistent perspective on employing assertions in major areas, such as: specification, verification, debugging, on-line monitoring and design quality improvement.

No grāmatas satura

Lietotāju komentāri - Rakstīt atsauksmi

Ierastajās vietās neesam atraduši nevienu atsauksmi.

Atlasītās lappuses

Saturs

643 Rewrite Rules Based on Sequences as Properties
136
644 Rewrite Rules Based on Property Variations
138
645 ComputerAssisted Correctness Proofs for Rewrite Rules
140
65 Automata Construction for Verification Directives
152
Enhanced Features and Uses of PSL Checkers
155
72 Recursive Compilation Strategies
156
73 A Special Case for eventually
160
74 Debug Enhancements for Checkers
162

25 Checkers in Silicon Debugging
27
26 Assertions in Static and Dynamic Verification
28
27 Supported Simulation and Emulation Semantics
33
Basic Techniques Behind Assertion Checkers
37
311 Regular Expressions and Classical Automata
38
312 Automata in Model Checking
44
32 Modular Approach to Checker Generation
47
33 AutomataBased Approach to Checker Generation
49
34 Other Related Research
52
PSL and SVA Assertion Languages
55
411 PSL Boolean Expressions
58
412 PSL Sequences and SEREs
59
413 PSL Properties
62
414 PSL Verification Directives and Other Declarations
68
42 SystemVerilog Assertions
70
421 SVA Boolean Expressions
73
422 SVA Sequences
75
423 SVA Properties
79
424 SVA Verification Statements
81
Automata for Assertion Checkers
83
52 Automaton Framework
84
522 Determinization of Automata
91
523 Minimization of Automata
94
524 Complementation of Automata
98
53 Generating CircuitLevel Checkers from Assertion Automata
100
Construction of PSL Assertion Checkers
105
62 Automata Construction for Booleans
106
63 Automata Construction for Sequences
111
631 Conventional Regular Expression Operators
112
632 Sequence Fusion
115
633 LengthMatching Intersection
116
634 Repetition with a Range
118
635 Rewrite Rules
120
64 Automata Construction for Properties
124
641 Base Cases for Properties
126
642 Rewrite Rules Based on Suffix Implication
134
741 Reporting Signal Dependencies
163
743 Signaling Assertion Completion
165
744 Assertion and Cover Counters
167
745 Hardware Assertion Threading
168
75 Checkers in Silicon Debug and OnLine Monitoring
172
751 Checkers in Silicon Debugging
173
753 Assertion Grouping
175
Evaluating and Verifying PSL Assertion Checkers
179
82 Nonsynthetic Assertions
182
83 Evaluating Assertion Grouping
188
84 Presynthesis Results
191
842 Complex Sequences
193
85 Benchmarking Debug Enhancements
195
86 Benchmarking Sequences and Properties
198
862 OccurrenceMatching Sequences
199
863 FailureMatching Sequences
200
864 Properties
203
Checkers for System Verilog Assertions
207
921 Automata Construction for Booleans
208
922 Automata Construction for Sequences
212
923 Automata Construction for Properties
218
924 Automata Construction for Verification Statements
225
93 Experimental Results for SVA Checkers
229
932 Benchmarking Sequences and Properties
235
933 Using SVA Checkers with Formal Verification Tools
240
Conclusions and Future Work
251
102 Future Work
253
1022 Checkers and Debugging
254
1023 Assertion Language Compilation
255
1024 Testing the Checkers
256
1025 Beyond RTL Assertion Languages
257
Example for UpDown Counter
259
References
265
Index
275
Autortiesības

Citi izdevumi - Skatīt visu

Bieži izmantoti vārdi un frāzes

Populāri fragmenti

2. lappuse - Quality — the totality of features and characteristics of a product or service that bear on its ability to satisfy stated or implied needs.
13. lappuse - How can one check a large routine in the sense of making sure that it's right? In order that the man who checks may not have too difficult a task, the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole program easily follows.
273. lappuse - ... 1994. [146] T. Shiple, G. Berry, and H. Touati, Constructive analysis of cyclic circuits, Proceedings of European Design and Test Conference, Paris, France, 1996, pp. 328-333. [147] M. Riedel and J. Bruck, The synthesis of cyclic combinational circuits, Proceedings of ACM/IEEE [148] The VIS group, VIS: a system for verification and synthesis, in Proceedings of the 8th International Conference on Computer Aided Verification, number 1102, R. Alur and T. Henzinger, Eds., New Brunswick, NJ, 1996,...
269. lappuse - First ACM & IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE '03), Mont St-Michel, France, June 2003, pp. 237-245. [3] WB Gardner, "CSP++: An Object-Oriented Application Framework for Software Synthesis from CSP Specifications,
272. lappuse - ... Springer, 1981. Lecture Notes in Computer Science Number 137. [18] Pascal Raymond. Recognizing regular expressions by means of dataflow networks. In 23rd International Colloquium on Automata, Languages, and Programming, pages 336-347. Springer, 1996. Lecture Notes in Computer Science Number 1099. [19] Andrew Seawright and Forrest Brewer. High-level symbolic construction techniques for high performance sequential synthesis.
265. lappuse - B. Beizer: Software testing techniques. Van Nostrand Reinhold, New- York, Second edition. 1990.
272. lappuse - F. Brewer: Clairvoyant: A Synthesis System for ProductionBased Specification, IEEE Transactions on VLSI Systems, pp.
266. lappuse - ... computation and parametric representation is ideally suited to equivalence checking. 8. REFERENCES [1] M. Aagaard, RB Jones, and C.-SH Seger. Formal verification using parametric representations of boolean constraints. In Proceedings of the Design Automation Conference, pages 402-407, June 1999. [2] D. Brand. Verification of large synthesized designs. In Proceedings of the International Conference on Computer- Aided D esign, pages 534-537, Santa Clara, CA, Nov.

Bibliogrāfiskā informācija