第1页 / 共374页
第2页 / 共374页
第3页 / 共374页
第4页 / 共374页
第5页 / 共374页
第6页 / 共374页
第7页 / 共374页
第8页 / 共374页
SystemVerilog Assertions and Functional Coverage.pdf
Foreword
Preface
Acknowledgments
Contents
Figures
Tables
1 Introduction
1.1…How Will This Book Help You?
1.2…SystemVerilog Assertions and Functional CoverageFunctional Coverage Under IEEE 1800 SystemVerilogIEEE 1800 SystemVerilog Umbrella
1.3…SystemVerilog Assertions EvolutionAssertions Evolution
2 System Verilog Assertions
2.1…What is an AssertionAssertionWhat is an Assertion?
2.2…Why Assertions? What are the AdvantagesAssertions advantages?
2.2.1 Assertions Shorten Time to DevelopAssertions shorten time to develop
2.2.2 Assertions Improve ObservabilityAssertions improve observabilityobservability
2.2.3 Assertions Provide Temporal Domain Functional Coveragefunctional coverage
2.2.3.1 Assertion Based Methodology Allows for Full Random Verificationrandom verification
2.2.3.2 Assertions Help Detect Bugsdetect bugs not Easily Observed at Primary Outputs
2.2.3.3 Other Major Benefitsmajor benefits
2.3…How do Assertions Work with an EmulatorAssertions in an emulator?
2.4…Assertions in Static FormalAssertions in Static Formal
2.5…One Time Effort, Many Benefits
2.6…Assertions Whining
2.6.1 Who Will Add Assertions? War Within!
2.7…A Simple PCI ReadPCI Read Example: Creating an Assertions Test PlanCreating an assertions test plan
2.8…What Type of Assertionstype of assertions Should I Add?
2.9…Protocol for Adding AssertionsProtocol for adding assertions
2.10…How do I Know I have Enough Assertions?enough assertions?
2.11…Use Assertions for Specification and ReviewAssertions for Specification and Review
2.12…Assertion Types
2.13…ConventionsConventions Used in the Book
3 Immediate Assertions
4 Concurrent Assertions: Basics (Sequence, Property, Assert)
4.1…Implication Operator, Antecedent and Consequent
4.2…Clocking Basics
4.3…Sampling Edge (Clock Edge) Value: How are Assertions Evaluated in a Simulation Time Tick?
4.3.1 Default Clocking Block
4.3.2 Gated Clk
4.4…Concurrent Assertions are Multi-Threaded
4.5…Formal Arguments
4.6…Disable (Property) Operator: ‘disable iff’
4.7…Severity Levels (for Both Concurrent and Immediate Assertions)
4.8…Bindingbinding Properties
4.8.1 Binding Properties (Scope Visibility)
4.8.2 Assertion Adoption in Existing DesignABV Adoption in Existing Design
4.9…Difference Between ‘sequence’ and ‘property’
5 Sampled Value FunctionsSampled Value Functions $rose$rose, $fell$fell
5.1…$rose: Edge DetectionEdge detection$rose -- edge detection in Property/Sequence
5.1.1 Edge Detection is Useful Because hellip
5.1.2 $fell$fell: Edge Detectionedge detection in Property/Sequence
5.1.3 $rose, $fell: In Procedural$rose, $fell -- in Procedural
5.2…$stable$stable
5.2.1 $stable in Procedural Block$stable in procedural block
5.3…$past$past
5.3.1 Application: $pastApplication\$past$past()
5.3.2 $past$past rescues $fell!
6 Operators
6.1…##m##m: Clock DelayClock Delay
6.1.1 Clock Delay Operator :: ##m##m Where m=0
6.1.1.1 Application: Clock Delay OperatorApplication\Clock delay operator :: ##m##m (m=0)
6.2…##[m:n]##[m\n]: Clock DelayClock Delay Range
6.2.1 Clock Delay Range Operator: ## [m:n] :: Multiple Threads
6.2.2 Clock Delay Range OperatorClock delay range operator :: ##[m:n]##[m\n] (m=0; n=$)
6.3…[*m][*m]: Consecutive Repetition OperatorConsecutive repetition operator
6.4…[*m:n][*m\n]: Consecutive Repetition RangeConsecutive Repetition Range
6.4.1 Application: Consecutive Repetition Range OperatorConsecutive Repetition Range operatorApplication\Consecutive Repetition Range operator
6.5…[=m][=m]: Repetition Non-Consecutivenon-consecutiveRepetition non-consecutive
6.6…[=m:n][= m\n]: Repetition Non-Consecutivenon-consecutive RangeRepetition non-consecutive range
6.6.1 Application: Repetition Non-Consecutive OperatorApplication\Repetition non-consecutive operator
6.7…[- greaterthan m][- greaterthan m] Non-Consecutive GoTo RepetitionGoTo repetition Operator
6.8…Difference Between [=m:n] and [- greaterthan m:n]Difference between [=m\n] and [- greaterthan m\n]
6.8.1 Application: GoTo Repetition---Non-Consecutive OperatorApplication\GoTo repetition---non-consecutive operator
6.9…sig1 ThroughoutThroughout seq1
6.9.1 Application: sig1 Throughout seq1Application \sig1 throughout seq1
6.10…seq1 withinwithin seq2
6.10.1 Application: seq1 within seq2Application\seq1 within seq2
6.10.2 ‘within’ Operator PASS CASES
6.10.3 ‘within’ Operator: FAIL CASES6.11…seq1 andand seq2seq1 and seq2
6.11…seq1 andand seq2seq1 and seq2
6.11.1 Application: ‘and’ OperatorApplication\‘and’ operator
6.12…seq1 ‘or’ seq2seq1 or seq2
6.12.1 Application: or OperatorApplication\or operator
6.13…seq1 ‘intersect’Intersect seq2
6.14…Application: ‘intersect’ OperatorApplication\‘intersect’ perator
6.14.1 Application: Intersect Operator (Interesting Application)Application\intersect operator (interesting application)
6.14.2 ‘intersect’ and ‘and’ :: What’s the Difference?‘Intersect’ and ‘and’ \\What’s the difference?
6.15…first_matchfirst_match complex_seq1
6.15.1 Application: first_matchApplication \first_match
6.16…not lessthan property expr greaterthan not lessthan property expr greaterthan
6.16.1 Application: not OperatorApplication\not operatornot operator
6.17…if (expression) property_expr1 else property_expr2if (expression) property_expr1 else property_expr2
6.17.1 Application: if then elseif then elseApplication\if then else
7 System Functions and Tasks
7.1…$onehot, $onehot0$onehot, $onehot0
7.2…$isunknown$isunknown
7.2.1 Application $isunknownApplication $isunknown
7.3…$countones$countones
7.3.1 $countones (as a boolean)$countones (as a boolean!!)
7.4…$assertoff$assertoff, $asserton$asserton, $assertkill$assertkill
8 Multiple Clocks
8.1…Multiply Clocked Sequences and Property OperatorsMultiply clocked Sequences and Property operators
8.1.1 Multiply Clocked Sequences
8.1.2 Multiply Clocked Sequences: Legal and Illegal SequencesMultiply clocked sequences: Legal and illegal sequences
8.1.3 Multiply Clocked Properties---‘and’ OperatorMultiply Clocked Properties---‘and’ Operator
8.1.4 Multiply Clocked Properties---‘or’ OperatorMultiply Clocked Properties---‘or’ operator
8.1.5 Multiply Clocked Properties---‘not’ OperatorMultiply clocked Properties---‘not’ Operator
8.1.6 Multiply Clocked Properties---Clock ResolutionMultiply Clocked Properties---Clock Resolution
8.1.7 Multiply Clocked Properties---Legal and Illegal ConditionsMultiply clocked Properties---Legal and Illegal conditions
9 Local VariablesLocal Variables
9.1…Application: Local VariablesApplication \Local Variables
10 Recursive PropertyRecursive property
10.1…Application: Recursive PropertyApplicationRecursive Property
11 Detecting and Using Endpoint of a SequenceDetecting and Using Endpoint of a Sequence
11.1….ended.ended
11.2….matched.matched
11.2.1 Application: .matchedApplication: .matched
12 ‘expect’expect and ‘assume’
13 ‘assume’assume and Formal (Static Functionalstatic functionalformal (static functional) Verification
14 Other Important TopicsApplications and important topics
14.1…Asynchronous FIFO AssertionsAsynchronous FIFO AssertionsFIFO AssertionsApplication\
14.1.1 FIFO Design
14.1.2 FIFO Test-Bench and AssertionsFIFO DESIGN, TESTBENCH AND ASSERTIONS
14.1.3 Test the Test-benchTest the Testbench
14.2…Embedding Concurrent Assertions in Procedural CodeEmbedding concurrent assertions in procedural code
14.3…Calling SubroutinesCalling subroutines
14.4…Sequence as a Formal ArgumentSequence as a formal argument
14.5…Sequence as an AntecedentSequence as an antecedent
14.6…Sequence in Sensitivity ListSequence in sensitivity list
14.7…Building a CounterBuilding a counter
14.8…Clock DelayClock Delay: What if You Want Variable Clock Delay?Variable delay?
14.9…What if the ‘action blockrsquor is Blocking?
14.10…Interesting Observation with Multiple Implications in a Property. Be Very Carefulhellip
14.11…Subsequence in a SequenceSubsequence in a sequence
14.12…Cyclic DependencyCyclic dependency
14.13…Refinement on a ThemeRefinement on a themehellip
14.14…Simulation Performanceperformance EfficiencySimulation performance efficiency
14.15…Itrsquors a Vacuous Worldvacuous world! Huh?
14.15.1 Concurrent Assertion --Without- an Implicationimplication
14.15.2 Concurrent Assertion --with- an ImplicationConcurrent assertion --with- an implicationimplication
14.15.3 Vacuous PassVacuous pass. What?
14.15.4 Concurrent Assertion--with ‘coverrsquorConcurrent Assertion---with ‘coverrsquor
14.16…Empty Sequence
15 Asynchronous Assertions !!!Asynchronous Assertions !!!
Outline placeholder
16.1…Strong and Weak SequencesWeak sequencesStrong and Weak sequences
16.2…Deferred Assertions
16.3…$changed
16.4…$sampled
16.5…$past_gclk, $rose_gclk, $fell_gclk, $stable_gclk, $changed_gclk, $future_gclk, $rising_gclk, $falling_gclk, $steady_gclk, $changing_gclk
16.6…‘triggeredtriggered’
16.7…‘followed by’ Property #-# and #=#
16.8…‘always’always and ‘s_always’s_always Property
16.9…‘eventually’eventually, ‘s_eventually’s_eventually
16.10…until, s_until, until_with and s_until_with Properties
16.11…nexttimeNexttime and s_nexttime
16.12…Case Statement
16.13…$inferred_clock$inferred_clock and $inferred_disable
16.14…Let Declarations
16.14.1 Let: Local Scope
16.14.2 Let: with Parameters
16.14.3 Let: In Immediate and Concurrent Assertions
16.15…‘restrictrestrict’ for Formal Verification
16.16…Abort Properties: reject_onreject_on, accept_onaccept_on, sync_reject_onsync_reject_on, sync_accept_onsync_accept_on
16.17…$assertpassoff, $assertpasson, $assertfailoff, $assertfailon, $assertnonvacuouson, $assertvacuousoff
16.18…CheckersCheckers
16.18.1 Nested CheckersCheckersNested
16.18.2 Checkers: Illegal ConditionsCheckers\illegal conditions
16.18.3 Checkers: Important PointsCheckers\Important Points
16.18.4 Checker: Instantiation RulesChecker\Instantiation Rules
17 SystemVerilog Assertions LABs
17.1…LAB1: Assertions with/without Implication
17.1.1 LAB1: ‘bind’ DUT Model and Test-Bench
17.1.2 LAB1: Questions
17.2…LAB 2: Overlap and Non-Overlap Operators
17.2.1 LAB2 DUT Model and Test-Bench
17.2.2 LAB2: Questions
17.3…LAB3: FIFO Assertions
17.3.1 LAB3: DUT Model and Test-Bench
17.3.2 LAB3: Questions
17.4…LAB4: Counter
17.4.1 LAB4: Questions
17.5…LAB5: Data Transfer Protocol
17.5.1 LAB5: Questions
17.6…LAB6: PCI Read Protocol
17.6.1 LAB6: Questions
18 System Verilog Assertions: LAB Answers
18.1…LAB1: Answers : ‘Bind’ and Implication Operators (Figs. 18.1, 18.2, 18.3)
18.2…LAB2: Answers : Overlap and Non-Overlap Operators (Figs. 18.4, 18.5)
18.3…LAB3: Answers : FIFO (Fig. 18.6)
18.4…LAB4: Answers : Counter (Fig. 18.7)
18.5…LAB5: Answers : Data Transfer Protocol (Fig. 18.8)
18.6…LAB6: Answers (Fig. 18.9)
19 Functional CoverageFunctional Coverage
19.1…Difference Between Code CoverageCode Coverage and Functional CoverageFunctional Coverage
19.2…Assertion Based Verification and Functional Coverage Based Methodology
19.2.1 Follow the BugsFollow the Bugs !!
20 Functional Coverage: Language Features
20.1…Covergroup/CoverpointCovergroup
20.2…SystemVerilog ‘covergroupCovergroup’: Basicshellip
20.3…SystemVerilog coverpointcoverpoint Basicshellip
20.3.1 Covergroup/Coverpoint ExampleCovergroup/Coverpoint Example hellip
20.4…SystemVerilog ‘binsbins’: Basics‘bins’ -- basicsSystemVerilog ‘bins’: basics hellip
20.4.1 Covergroup/Coverpoint with bins: ExampleCovergroup/Coverpoint with bins -- example hellip
20.4.2 SystemVerilog ‘covergroup’: Formal and Actual Arguments
20.4.3 ‘covergroupCovergroup’ in a ‘class’
20.5…‘crosscross’ Coverage‘cross’ coverage
20.6…More ‘bins’
20.6.1 ‘bins’ for Transition Coverage‘bins’ for transition coverage
20.6.2 ‘wildcard’ ‘bins’‘wildcard’ ‘bins’
20.6.3 ‘ignore_bins’‘ignore_bins’
20.6.4 ‘illegal_bins’‘illegal_bins’
20.6.5 ‘binsof’ and ‘intersect’‘binsof’ and ‘intersect’
21 Performance Implications of Coverage Methodology
21.1…Know what you Should Cover
21.2…Know when you Should Cover
21.3…When to ‘Cover’ (Performance Implication)
21.4…Application: Have you Transmitted All Different Lengths of a Frame?
22 Coverage Options (Reference Material)
22.1…Coverage Options: Instance Specific---Example (Figs. 22.1 and 22.2)
22.2…Coverage Options: Instance Specific Per-Syntactic Level (Figs. 22.3 and 22.4)
22.3…Coverage Options for ‘Covergroup’ Type: Example (Figs. 22.5 and 22.6)
Index
Ashok B. Mehta
SystemVerilog
Assertions
and Functional
Coverage
Guide to Language, Methodology and
Applications
www.it-ebooks.info
SystemVerilog Assertions
and Functional Coverage
www.it-ebooks.info
Ashok B. Mehta
SystemVerilog Assertions
and Functional Coverage
Guide to Language, Methodology
and Applications
123
www.it-ebooks.info
Ashok B. Mehta
Los Gatos, CA
USA
Additional material to this book can be downloaded from http://extras.springer.com.
ISBN 978-1-4614-7323-7
DOI 10.1007/978-1-4614-7324-4
Springer New York Heidelberg Dordrecht London
ISBN 978-1-4614-7324-4
(eBook)
Library of Congress Control Number: 2013935401
Ó Springer Science+Business Media New York 2014
This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of
the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations,
recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or
information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar
methodology now known or hereafter developed. Exempted from this legal reservation are brief
excerpts in connection with reviews or scholarly analysis or material supplied specifically for the
purpose of being entered and executed on a computer system, for exclusive use by the purchaser of the
work. Duplication of this publication or parts thereof is permitted only under the provisions of
the Copyright Law of the Publisher’s location, in its current version, and permission for use must
always be obtained from Springer. Permissions for use may be obtained through RightsLink at the
Copyright Clearance Center. Violations are liable to prosecution under the respective Copyright Law.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this
publication does not imply, even in the absence of a specific statement, that such names are exempt
from the relevant protective laws and regulations and therefore free for general use.
While the advice and information in this book are believed to be true and accurate at the date of
publication, neither the authors nor the editors nor the publisher can accept any legal responsibility for
any errors or omissions that may be made. The publisher makes no warranty, express or implied, with
respect to the material contained herein.
Printed on acid-free paper
Springer is part of Springer Science+Business Media (www.springer.com)
www.it-ebooks.info
To
My dear wife Ashraf Zahedi
and
My dear parents Rukshmani
and Biren Mehta
www.it-ebooks.info
Foreword
Louis H. Sullivan, an American architect, considered the father of the modern
skyscraper, and mentor to Frank Lloyd Wright, coined the phrase ‘‘form follows
function.’’ The actual quote is ‘‘form ever follows function’’ which is a bit more
poetic and assertive than the version that has found its way into the common
vernacular. He wrote those words in an article written for Lippincott’s Magazine
#57 published in March 1896. Here is the passage in that article that contains the
famous quote:
‘‘Whether it be the sweeping eagle in his light or the open apple-blossom, then toiling
work horse, the blithe swan, the branching oak, the winding stream at its base, the drifting
clouds—over all the coursing sun, form ever follows function, and this is the law. Where
function does not change, form does not change. The granite rocks, the ever brooding hills,
remain for ages; the lightning lives, comes into shape, and dies, in a twinkling.
It is the pervading law of all things organic and inorganic, of all things physical and
metaphysical, of all things human and all things superhuman—of all true manifestations of
the head, of the heart, of the soul—that the life is recognizable in its expression, that form
ever follows function. This is the law.’’
Earlier in the article, Sullivan foreshadows his thought with this passage:
‘‘All things in nature have a shape, that is to say, a form, an outward semblance, that tells
us what they are, that distinguishes them from ourselves and from each other.’’
The precise meaning of this pithy phrase has been debated in art and archi-
tecture circles since Sullivan’s article was first published. However, it is widely
accepted to mean that the form of something—its shape, color, size, etc.—is
related to what it does. Water flows, rocks sit, and birds fly.
In his book ‘‘The Design of Everyday Things,’’(Basic Books 1988) Don Nor-
man discusses a similar concept, the notion of affordances. Norman defines the
term as ‘‘… the perceived and actual properties of the thing, primarily those
fundamental properties that determine just how the thing could possibly be used.’’
He cites some examples: ‘‘A chair affords (‘‘is for’’) support and, therefore, affords
sitting. A chair can also be carried. Glass is for seeing through, and for breaking.
Wood is normally used for solidity, opacity, support or carving.’’
vii
www.it-ebooks.info
viii
Foreword
Norman’s idea turns Sullivan’s upside down. He is saying function follows
form. The shape, color, size, etc., of an object affects what it does. Nonetheless,
both men would likely agree that form and function, whichever drives the other,
are inextricably linked.
Software designers have the luxury of choosing the form to fit the function.
They are not as constrained by the laws of physics as say, a cabinetmaker. The
cabinetmaker must choose materials that will not only look nice, but will withstand
the weight of books or dishes or whatever is to be placed on the shelves. Software
designers have some constraints with regard to memory space and processing time,
but beyond that they have a lot of freedom to build whatever comes to mind.
Sullivan referred to ‘‘all things physical and metaphysical.’’ Without much of a
stretch we can interpret that to include software, a most abstract human creation.
The form of a piece of software is linked to its function. The complex software that
verification engineers build, called a testbench, must be designed before it can be
built. The verification engineer, like an architect, must determine the form of his
creation.
The architecture space is wide open. Computer code, while much more abstract
than say, a staircase or a door handle on a car, has a form and a function. The form
of computer code is the set of syntactic elements strung together in a program. The
function is what
the program does when executed, often referred to as its
semantics.
A verification engineer is typically presented a set of requirements, often as a
design specification, and asked to build a testbench that meets these requirements.
Because of the tremendous flexibility afforded by the software medium he must
choose the form carefully to ensure that not only meets the requirements, but is
easy to use, reusable, and robust. He must choose a form that fits the function.
Often an assertion is just the right thing to capture the essence of some part of a
design. The form of an assertion is short sequence of text that can be inserted easily
without disrupting the design. With their compact syntax and concise semantics
assertions can be used to check low-level invariants, protocols, or end-to-end
behavior.
The function of an assertion, in a simulation context, is to assert that something
is always (or never) the case. It ensures that invariants are indeed invariant.
Assertions can operate as checkers or as coverpoints. The fact that they can be
included in-line in RTL code or in separate checkers, they can be short or long for
simple or complex checking makes them invaluable in any testbench.
The wise verification engineer uses all the tools as his disposal to create an
effective and easy to use testbench. He will consider the function of the testbench
and devise a form that suits the required function. Assertions are an important part
of any testbench.
Ashok Mehta has written a book that makes assertions accessible. His approach
is very pragmatic, choosing to show you how to build and use assertions rather
than engage in a lot of theoretical discussion. Not that theoretical discussion is
www.it-ebooks.info
Foreword
ix
irrelevant—it is useful to understand the theoretical underpinnings of any tech-
nology. However, there are many other books on that topic. This book fills a gap
for practicing engineers where before no text provided the how-tos of building and
using assertions in a real-world context.
Ashok opens up the world of assertions to verification engineers who may have
thought them too opaque to consider using in a real testbench. He does an espe-
cially nice job of deconstructing assertions to show how they work and how to
write them. Through detailed examples he shows all the pieces that go into cre-
ating assertions of different kinds, and how they fit together. Ashok completes the
picture by demonstrating how assertions and coverage fit together.
Part of the book is devoted to functional coverage. He deconstructs the
sometimes awkward SystemVerilog syntax of covergroups and coverpoints. Like
he has with assertions, he takes the mystery out of building a high-quality coverage
model.
With the mysteries of assertions unmasked, you can now include them in your
personal vocabulary of testbench forms. This will enable you to create testbenches
with more sophisticated function.
February 2013
Mark Glasser
www.it-ebooks.info
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
