Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line MonitoringAssertion-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. |
Lietotāju komentāri - Rakstīt atsauksmi
Saturs
1 | |
6 | |
7 | |
9 | |
13 | |
16 | |
23 Assertion Checkers and Checker Generators | 20 |
24 Assertion Support in Simulators and Emulators | 24 |
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 |
Citi izdevumi - Skatīt visu
Generating Hardware Assertion Checkers: For Hardware Verification, Emulation ... Marc Boulé,Zeljko Zilic Priekšskatījums nav pieejams - 2010 |
Generating Hardware Assertion Checkers: For Hardware Verification, Emulation ... Marc Boulé,Zeljko Zilic Priekšskatījums nav pieejams - 2008 |