Muutke küpsiste eelistusi

E-raamat: SystemVerilog Assertions and Functional Coverage: Guide to Language, Methodology and Applications

  • Formaat: PDF+DRM
  • Ilmumisaeg: 11-May-2016
  • Kirjastus: Springer International Publishing AG
  • Keel: eng
  • ISBN-13: 9783319305394
  • Formaat - PDF+DRM
  • Hind: 159,93 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
  • Formaat: PDF+DRM
  • Ilmumisaeg: 11-May-2016
  • Kirjastus: Springer International Publishing AG
  • Keel: eng
  • ISBN-13: 9783319305394

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

This book provides a hands-on, application-oriented guide to the language and methodology of both SystemVerilog Assertions and SystemVerilog Functional Coverage. Readers will benefit from the step-by-step approach to functional hardware verification using SystemVerilog Assertions and Functional Coverage, which will enable them to uncover hidden and hard to find bugs, point directly to the source of the bug, provide for a clean and easy way to model complex timing checks and objectively answer the question have we functionally verified everything. Written by a professional end-user of ASIC/SoC/CPU and FPGA design and Verification, this book explains each concept with easy to understand examples, simulation logs and applications derived from real projects. Readers will be empowered to tackle the modeling of complex checkers for functional verification, thereby drastically reducing their time to design and debug. 





This updated second edition addresses the latest functional set released in IEEE-1800 (2012) LRM, including numerous additional operators and features. Additionally, many of the Concurrent Assertions/Operators explanations are enhanced, with the addition of more examples and figures.



·         Covers in its entirety the latest IEEE-1800 2012 LRM syntax and semantics;

·         Covers both SystemVerilog Assertions and SystemVerilog Functional Coverage language and methodologies;

·         Provides practical examples of the what, how and why of Assertion Based Verification and Functional Coverage methodologies;

·         Explains each concept in a step-by-step fashion and applies it to a practical real life example;

·         Includes 6 practical LABs that enable readers to put in practice the concepts explained in the book.
1 Introduction
1(8)
1.1 How Will This Book Help You?
4(1)
1.2 System Verilog Assertions and Functional Coverage Under IEEE 1800 System Verilog Umbrella
5(2)
1.3 System Verilog Assertions Evolution
7(2)
2 System Verilog Assertions
9(22)
2.1 What Is an Assertion?
9(1)
2.2 Why Assertions? What Are the Advantages?
9(7)
2.2.1 Assertions Shorten Time to Develop
10(1)
2.2.2 Assertions Improve Observability
11(1)
2.2.3 Assertions Provide Temporal Domain Functional Coverage
11(3)
2.2.4 Assertion Based Methodology Allows for Full Random Verification
14(1)
2.2.5 Assertions Help Detect Bugs not Easily Observed at Primary Outputs
15(1)
2.2.6 Other Major Benefits
15(1)
2.3 How Do Assertions Work with an Emulator?
16(1)
2.4 Assertions in Static Formal
17(2)
2.5 One-Time Effort, Many Benefits
19(1)
2.6 Assertions Whining
20(2)
2.6.1 Who Will Add Assertions? War Within!
21(1)
2.7 A Simple PCI Read Example---Creating an Assertions Test Plan
22(2)
2.8 What Type of Assertions Should I Add?
24(1)
2.9 Protocol for Adding Assertions
25(1)
2.10 How Do I Know I Have Enough Assertions?
26(1)
2.11 Use Assertions for Specification and Review
26(1)
2.12 Assertion Types
27(1)
2.13 Conventions Used in the Book
28(3)
3 Immediate Assertions
31(4)
4 Concurrent Assertions---Basics (Sequence, Property, Assert)
35(32)
4.1 Implication Operator, Antecedent and Consequent
40(2)
4.2 Clocking Basics
42(2)
4.3 Sampling Edge (Clock Edge) Value: How Are Assertions Evaluated in a Simulation Time Tick?
44(9)
4.3.1 Default Clocking Block
48(4)
4.3.2 Gated Clk
52(1)
4.4 Concurrent Assertions Are Multi-threaded
53(2)
4.5 Formal Arguments
55(3)
4.6 Disable (Property) Operator---'Disable Iff'
58(2)
4.7 Severity Levels (for Both Concurrent and Immediate Assertions)
60(1)
4.8 Binding Properties
61(4)
4.8.1 Binding Properties (Scope Visibility)
62(2)
4.8.2 Assertion Adoption in Existing Design
64(1)
4.9 Difference Between `Sequence' and `Property'
65(2)
5 Sampled Value Functions $rose, $fell, $stable, $past
67(14)
5.1 $rose---Edge Detection in Property/Sequence
68(4)
5.1.1 Edge Detection Is Useful Because
68(3)
5.1.2 $fell---Edge Detection in Property/Sequence
71(1)
5.1.3 $rose, $fell---in Procedural
71(1)
5.2 $stable
72(1)
5.2.1 $stable in Procedural Block
73(1)
5.3 $past
73(8)
5.3.1 Application: $past ()
78(1)
5.3.2 $past Rescues $fell!
78(3)
6 Operators
81(66)
6.1 ##m---Clock Delay
81(3)
6.1.1 Clock Delay Operator: ##m Where m=0
82(2)
6.2 ##[ m:nL-Clock Delay Range
84(10)
6.2.1 Clock Delay Range Operator: ##[ m:n]: Multiple Threads
85(9)
6.2.2 Clock Delay Range Operator:: ##[ m:n] (m=0; n=$)
94(1)
6.3 [ *m]---Consecutive Repetition Operator
94(4)
6.4 [ *m:n]---Consecutive Repetition Range
98(9)
6.4.1 Application: Consecutive Repetition Range Operator
101(6)
6.5 [ =m]---Repetition Non-consecutive
107(4)
6.6 [ =m:n]---Repetition Non-consecutive Range
111(3)
6.6.1 Application: Repetition Non-consecutive Operator
112(2)
6.7 [ ->m] Non-consecutive GoTo Repetition Operator
114(1)
6.8 Difference Between [ =m:n] and [ ->m:n]
115(2)
6.8.1 Application: GoTo Repetition---Non-consecutive Operator
116(1)
6.9 Sig1 throughout Seq1
117(4)
6.9.1 Application: Sig1 throughout Seq1
118(3)
6.10 Seq1 within Seq2
121(3)
6.10.1 Application: Seq1 within Seq2
122(1)
6.10.2 `within' Operator PASS CASES
123(1)
6.10.3 `within' Operator: FAIL CASES
124(1)
6.11 Seq1 and Seq2
124(3)
6.11.1 Application: `and' Operator
127(1)
6.12 Seq1 `or' Seq2
127(4)
6.12.1 Application: or Operator
128(3)
6.13 Seq1 `intersect' Seq2
131(1)
6.14 Application: `intersect' Operator
132(5)
6.14.1 Application: intersect Operator (Interesting Application)
133(4)
6.14.2 `intersect' and `and' :: What's the Difference?
137(1)
6.15 first_match
137(4)
6.15.1 Application: first_match
138(3)
6.16 not <property expr>
141(2)
6.16.1 Application: not Operator
141(2)
6.17 if (expression) property_expr1 else property_expr2
143(2)
6.17.1 Application: if then else
145(1)
6.18 `iff and `implies'
145(2)
7 System Functions and Tasks
147(8)
7.1 $onehot, $onehot0
147(2)
7.2 $isunknown
149(1)
7.3 $countones
150(1)
7.3.1 $countones (as Boolean)
151(1)
7.4 $assertoff, $asserton, $assertkill
151(4)
8 Multiple Clocks
155(12)
8.1 Multiply-Clocked Sequences and Properties
155(12)
8.1.1 Multiply Clocked Sequences
156(1)
8.1.2 Multiply Clocked Sequences--Legal and Illegal Sequences
157(1)
8.1.3 Multiply Clocked Properties---`and' Operator
158(1)
8.1.4 Multiply Clocked Properties---`or' Operator
159(2)
8.1.5 Multiply Clocked Properties---`not'---Operator
161(1)
8.1.6 Multiply Clocked Properties---Clock Resolution
161(3)
8.1.7 Multiply Clocked Properties---Legal and Illegal Conditions
164(3)
9 Local Variables
167(14)
9.1 Application: Local Variables
179(2)
10 Recursive Property
181(6)
10.1 Application: Recursive Property
182(1)
10.2 Application: Recursive Property
183(4)
11 Detecting and Using Endpoint of a Sequence
187(14)
11.1 .triggered (Replaced for .ended)
187(8)
11.2 .matched
195(6)
11.2.1 Application: matched
198(3)
12 `expect'
201(4)
13 `assume' and Formal (Static Functional) Verification
205(2)
14 Very Important Topics and Applications
207(40)
14.1 Asynchronous FIFO Assertions
207(10)
14.1.1 Asynchronous FIFO Design
208(2)
14.1.2 Asynchronous FIFO Testbench and Assertions
210(4)
14.1.3 Test the Testbench
214(3)
14.2 Embedding Concurrent Assertions in Procedural Code
217(5)
14.3 Calling Subroutines
222(3)
14.4 Sequence as a Formal Argument
225(1)
14.5 Sequence as an Antecedent
226(1)
14.6 Sequence in Sensitivity List
227(1)
14.7 Building a Counter
228(1)
14.8 Clock Delay: What if You Want Variable Clock Delay?
229(2)
14.9 What if the `Action Block' Is Blocking?
231(3)
14.10 Interesting Observation with Multiple (Nested) Implications in a Property. Be Careful
234(1)
14.11 Subsequence in a Sequence
235(1)
14.12 Cyclic Dependency
236(1)
14.13 Refinement on a Theme
237(1)
14.14 Simulation Performance Efficiency
237(2)
14.15 It's a Vacuous World! Huh?
239(4)
14.15.1 Concurrent Assertion---Without---An Implication
239(1)
14.15.2 Concurrent Assertion---With---An Implication
240(1)
14.15.3 Vacuous Pass. What?
241(1)
14.15.4 Concurrent Assertion---with `Cover'
241(2)
14.16 Empty Sequence
243(4)
15 Asynchronous Assertions!!!
247(4)
16 IEEE-1800-2009/2012 Features
251(54)
16.1 Strong and Weak Sequences
251(1)
16.2 Deferred Immediate Assertions
252(4)
16.3 $changed
256(1)
16.4 $sampled
257(1)
16.5 $past_gclk, $rose_gclk, $fell_gclk, $stable_gclk, $changed_ gclk, $future_gclk. $rising_gclk, $falling_gclk, $steady_gclk, $changing_gclk
258(3)
16.6 `followed by' Properties #-# and #=#
261(1)
16.7 `always' and `s_always' Property
262(2)
16.8 `eventually', `s_eventually'
264(1)
16.9 `until', `s_until' `until_with' and `s_until_with'
265(2)
16.10 `nexttime' and `s_nexttime'
267(3)
16.11 `case' Statement
270(1)
16.12 $inferred_clock and $inferred_disable
271(2)
16.13 `let' Declarations
273(7)
16.13.1 let: Local Scope
274(1)
16.13.2 let: With Parameters
275(2)
16.13.3 let: In Immediate and Concurrent Assertions
277(3)
16.14 `restrict' for Formal Verification
280(1)
16.15 Abort Properties: reject_on, accept_on, sync_reject_on, sync_accept_on
280(4)
16.16 $assertpassoff, $assertpasson, $assertfailoff, $assertfailon, $assertnonvacuouson, $assertvacuousoff
284(1)
16.17 $assertcontrol
285(5)
16.18 Checkers
290(15)
16.18.1 Nested Checkers
295(1)
16.18.2 Checkers: Illegal Conditions
296(2)
16.18.3 Checkers: Important Points
298(3)
16.18.4 Checker: Instantiation Rules
301(4)
17 System Verilog Assertions LABs
305(38)
17.1 LAB1: Assertions with/Without Implication and `bind'
305(5)
17.1.1 LAB1: `bind' DUT Model and Testbench
306(2)
17.1.2 LAB1: Questions
308(2)
17.2 LAB2: Overlap and Non-overlap Operators
310(3)
17.2.1 LAB2 DUT Model and Testbench
310(1)
17.2.2 LAB2: Questions
311(2)
17.3 LAB3: Synchronous FIFO Assertions
313(8)
17.3.1 LAB3: DUT Model and Testbench
313(4)
17.3.2 LAB3: Questions
317(4)
17.4 LAB4: Counter
321(6)
17.4.1 LAB4: Questions
324(3)
17.5 LAB5: Data Transfer Protocol
327(9)
17.5.1 LAB5: Questions
335(1)
17.6 LAB6: PCI Read Protocol
336(7)
17.6.1 LAB6: Questions
340(3)
18 System Verilog Assertions---LAB Answers
343(18)
18.1 LAB1: Answers: `bind' and Implication Operators
344(5)
18.2 LAB2: Answers: Overlap and Non-overlap Operators
349(4)
18.3 LAB3: Answers: Synchronous FIFO
353(2)
18.4 LAB4: Answers: Counter
355(1)
18.5 LAB5: Answers: Data Transfer Protocol
356(3)
18.6 LAB6: Answers: PCI Read Protocol
359(2)
19 Functional Coverage
361(6)
19.1 Difference Between Code Coverage and Functional Coverage
361(1)
19.2 Assertion Based Verification (ABV) and Functional Coverage (FC) Based Methodology
362(5)
19.2.1 Follow the Bugs!!
366(1)
20 Functional Coverage---Language Features
367(24)
20.1 Covergroup/Coverpoint
367(1)
20.2 System Verilog `Covergroup'---Basics
368(1)
20.3 System Verilog Coverpoint Basics
368(4)
20.3.1 Covergroup/Coverpoint Example
371(1)
20.4 System Verilog `Bins'---Basics
372(6)
20.4.1 Covergroup/Coverpoint with Bins---Example
374(1)
20.4.2 System Verilog `covergroup'----Formal and Actual Arguments
375(1)
20.4.3 `covergroup' in a `class'
376(2)
20.5 `cross' Coverage
378(4)
20.6 More `Bins'
382(9)
20.6.1 `Bins' for Transition Coverage
382(4)
20.6.2 `wildcard bins'
386(1)
20.6.3 `ignore_bins'
386(1)
20.6.4 `illegal_bins'
387(1)
20.6.5 `binsof and `intersect'
388(3)
21 Performance Implications of Coverage Methodology
391(4)
21.1 Know What You Should Cover
391(1)
21.2 Know When You Should Cover
392(1)
21.3 When to `Cover' (Performance Implication)
392(1)
21.4 Application: Have You Transmitted All Different Lengths of a Frame?
393(2)
22 Coverage Options
395(8)
22.1 Coverage Options---Instance Specific---Example
397(1)
22.2 Coverage Options---Instance Specific Per-Syntactic Level
397(3)
22.3 Coverage Options for `Covergroup' Type---Example
400(3)
Index 403
Ashok Mehta has been working in the ASIC/SoC design and verification field for over 20 years. He started his career at Digital Equipment Corporation (DEC) working first as a CPU design engineer, moving on to hardware design verification of the VAX11-785 CPU design. He then worked at Data General, Intel (first Pentium design team) and after a route of a couple of startups, worked at Applied Micro and TSMC. He was a very early adopter of Verilog and participated in Verilog, VHDL, iHDL (Intel HDL) and SDF (standard delay format) technical subcommittees. He has also been a proponent of ESL (Electronic System Level) designs and at TSMC he released two industry standard Reference Flows that take designs from ESL to RTL while preserving the verification environment for reuse from ESL to RTL. Lately, he has been involved with 3DIC design verification challenges at TSMC which is where SystemVerilog Assertions played an instrumental role in stacked die SoC design verification.

Ashok earned an MSEE from University of Missouri. He holds 13 U.S. Patents in the field of SoC and 3DIC design verification.