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

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.

Priekšskatīt šo grāmatu »

No grāmatas satura

Lietotāju komentāri - Rakstīt atsauksmi

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

Atlasītās lappuses

Titullapa

Saturs

Introduction	1

12 Book Objectives	6

13 Overview of the Book	7

14 External Contributions and Collaborations	9

Assertions and the Veriﬁcation Landscape	13

22 Uses of Assertions in Hardware	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 Veriﬁcation 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 Veriﬁcation	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 Veriﬁcation Directives and Other Declarations	68

42 SystemVerilog Assertions	70

421 SVA Boolean Expressions	73

422 SVA Sequences	75

423 SVA Properties	79

424 SVA Veriﬁcation 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 Sufﬁx 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

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

Bieži izmantoti vārdi un frāzes

activity actually added algorithm allow alphabet antecedent appearing applied approach argument assertion checkers automata automaton behavior Boolean Boolean expressions Chapter checking circuit clock cycle complete condition consequent construction corresponds create debugging deﬁned Deﬁnition described determinization developed directive directly dynamic veriﬁcation edge effect equivalent errors evaluated eventually example execution expression fails failure false Figure ﬁnal ﬁrst ﬂip-ﬂops FoCs formal function given hardware hold implementation implication indicates initial input interrupt intersection language logic matching MBAC monitoring never observed occur operator output performed presented produced proof Proposition range regular expressions repetition reported represents reset rewrite rules semantics separate sequence SERE shown shows side signal similar simulation single speciﬁcation statements strong subset symbol Table techniques temporal threading tion tool trace transition true veriﬁcation

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.

Iekļauts 624 grāmatās, sākot no 1935. līdz 2008.

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.

Iekļauts 14 grāmatās, sākot no 1959. līdz 2008.

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,...

Iekļauts 6 grāmatās, sākot no 2005. līdz 2008.

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,

Iekļauts 9 grāmatās, sākot no 1991. līdz 2008.

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.

Iekļauts 5 grāmatās, sākot no 1983. līdz 2008.

265. lappuse - B. Beizer: Software testing techniques. Van Nostrand Reinhold, New- York, Second edition. 1990.

Iekļauts 6 grāmatās, sākot no 1993. līdz 2008.

272. lappuse - F. Brewer: Clairvoyant: A Synthesis System for ProductionBased Specification, IEEE Transactions on VLSI Systems, pp.

Iekļauts 5 grāmatās, sākot no 1998. līdz 2008.

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.