第1页 / 共361页
第2页 / 共361页
第3页 / 共361页
第4页 / 共361页
第5页 / 共361页
第6页 / 共361页
第7页 / 共361页
第8页 / 共361页
SystemVerilog Assertion Handbook.pdf
Frontpage
Contents
Preface
1. Role of SystemVerilog Assertion in a Verification Methodology
2. Overview of Property and Assertions
3. Understanding Properties
4. Understanding Sequences
5. Advanced Topics for Properties and Sequences
6. SystemVerilog Assertions in the Design Process
7. Formal Verification Using Assertions
8. SystemVerilog Assertions Guidelines
9. SystemVerilog Assertions Dictionary
Appendix A: Answers to Excercises
Appendix B: Definitions
Appendix C: Quick Reference Guide
Appendix D: SystemVerilog Assertions Syntax
Appendix E: Reserved Keywords
Index
ii
SystemVerilog Assertions Handbook
SystemVerilog Assertions
Handbook
… for Formal and Dynamic Verification
Published by:
VhdlCohen Publishing
P.O. 2362
Palos Verdes Peninsula CA 90274-2362
vhdlcohen@aol.com
http://www.vhdlcohen.com
Library of Congress Cataloging-in-Publication Data
A C.I.P. Catalog record for this book is available from the Library of Congress
SystemVerilog Assertions Handbook
… for Formal and Dynamic Verification
ISBN 0-9705394-7-9
Copyright © 2005 by VhdlCohen Publishing
All rights reserved. No part of this publication may be reproduced or transmitted in any
form or by any means, electronic or mechanical, including photocopying, recording, or
by any information storage and retrieval system, without the prior written permission
from the author, except for the inclusion of brief quotations in a review.
Printed on acid-free paper
Printed in the United States of America
Preface
Contents
iii
xxv
xxxiii
xxix
Foreword ………………………………………………………………………………….. xi
Surrendra A. Dudani …………………………………………………………………… xi
xiii
Stuart Sutherland ……………………………………………………………………….
Harry D. Foster ………………………………………………………………………..
xv
xvii
Tarak Parikh ………………………………………………………………………….
xix
Keith Rieken ……………………………………………………………………………
xxi
Yu-Chin Hsu ……………………………………………………………………………
xxiii
Alain Raynaud ………………………………………………………………………….
Preface ……………………………………………………………………………………..
Acknowledgements ……………………………………………………………………
About the authors ………………………………………………………………………
Disclaimer …………………………………………………………………………………. xxxv
1 ROLE OF SYSTEMVERILOG ASSERTIONS
IN A VERIFICATION METHODOLOGY ........................................... 1
1.1 History of Design Verification methodologies .............................................................…… 2
1.2 SystemVerilog Assertions in verification Strategy ...................................................……...
5
5
1.2.1 Are Assertions Independent from SystemVerilog Structures? ………………………
6
1.2.2 Are Assertions Useful for the Definition and Verification of Designs? ..................…..
7
1.2.2.1 Captures Designer Intent ................................................................................................
1.2.2.2 Allows Protocols to be Defined and Verified ...................................................................
8
8
1.2.2.3 Reduces the Time to Market .......................................................................................….
8
1.2.2.4 Greatly Simplifies the Verification of Reusable IP ......................................................
9
1.2.2.5 Facilitates Functional Coverage Metrics ......................................................................
1.2.2.6 Generates Counterexamples to Demonstrate Violation of Properties ..................…
10
1.2.3 Can/should entire functional verification task be performed
using SystemVerilog Assertions? ...........................................................................….
1.2.4 Is SystemVerilog Assertions Solely Restricted to Applications that
Use SystemVerilog? ......................................................................................................…. 10
1.2.4.1 VHDL Model and Testbench with SystemVerilog Assertions Module ....................... 10
1.2.4.2 VHDL Model Embedded in SystemVerilog testbench with SVA Module ................... 11
1.3 Accellera's SystemVerilog Assertions Goals ...............................................................……. 11
1.4 SystemVerilog Assertions Language ............................................................................…… 12
10
SystemVerilog Assertions Handbook
iv
2 OVERVIEW OF PROPERTIES AND ASSERTIONS ...............………. 15
2.1 DEFINITIONS ......................................................................................................…………… 15
2.1.1 Properties ...................................................................................................................……. 15
2.1.2 Sequences ..................................................................................................................……. 16
2.1.3 Antecedent / Consequent / Thread ............................................................................…. 16
2.1.4 Specification and Verification ....................................................................................…… 18
Assertion-Based Verification .......................................................................................... 18
2.1.5 Assertion / Assumption / Verification Directive .................................................……….. 19
2.1.6 Constraint ..................................................................................................................……
19
2.2 property ..................................................................................................................………..
20
2.2.1 Named Properties .....................................................................................................…... 20
2.3 Assertion ..................................................................................................................………..
21
2.3.1 Immediate assertions ....................................................................................................... 22
2.3.2 Concurrent Assertion .....................................................................................................
24
Verification Directives ................................................................................................ 24
2.4 Boolean Expression .....................................................................................................……… 26
27
3 UNDERSTANDING PROPERTIES ...............................................................
28
3.1 Sequences Overview .....................................................................................................…….
29
3.1.1 Sequence Declaration .....................................................................................................
31
3.2 SystemVerilog Properties ........................................................................................………
3.2.1 Property Header .....................................................................................................……… 32
3.2.2 Property Identifier .....................................................................................................……. 33
3.2.3 Formal Arguments and Usage ........................................................................................ 33
3.2.4 Local Variables in Properties .......................................................................................... 34
3.2.5 Body of the Property ....................................................................................................... 39
39
3.2.5.1 Clocking Event .....................................................................................................………
40
3.2.5.2 Disabling condition .....................................................................................................…..
3.2.5.3 Property Expression .....................................................................................................…
42
3.2.5.3.1 Property Operators ..................................................................................................... 42
4 UNDERSTANDING SEQUENCES .............................................................…..
47
4.1 Sequence Operators and Built-in Functions ..............................................................……
48
4.2 Capturing Temporal Behavior in SystemVerilog Assertions ....................................……
49
4.3 Implication Operators ...................................................................................................….
53
4.3.1 Overlapped implication Operator |-> .............................................................................
54
4.3.2 Non Overlapped Implication Operator |=> ..............................................................…..
55
4.3.3 Understanding the Overlapped Implication Operator "|->" ...................................….. 56
4.3.4 Understanding the Non-overlapped Implication Operator " |=>" ......................…… 58
4.3.5 Using "not" with Implication Operator .............................................................……… 59
4.4 first_match Operator ....................................................................................................…..
60
64
4.5 Repetition Operators ....................................................................................................…..
66
4.5.1 Consecutive Repetition ..................................................................................................
4.5.1.1 [*n] Repetition ................................................................................................................
66
4.5.1.2 [*n:m] Repetition ....................................................................................................……
66
4.5.1.3 [*0 : m] Repetitions ....................................................................................................…. 69
4.5.1.4 [*n : $], ##[0:$] .............................................................................................................… 71
4.5.2 Sequence Non-consecutive Repetition ([=n]) .............................................................….
74
v
74
75
76
76
77
77
78
79
80
80
83
84
85
86
Preface
4.5.3 Sequence goto Repetition ([->n ]) ..........................................................................…….
4.6 Sequence Composition Operators ..........................................................................………..
4.6.1 Sequence Fusion (##0) ....................................................................................................
4.6.2 Sequence Disjunction (or) .......................................................................................……
4.6.3 Sequence Non-Length-Matching (and) .............................................................……….
4.6.4 Sequence Length-Matching (intersect) ...................................................................…
4.6.5 Sequence Containment (within) .........................................................................………
4.6.6 Conditions over Sequences (throughout operator) ...............................................…….
4.7 Methods Supporting Sequences .........................................................................…………
4.7.1 Endpoint of a Single Clock Sequence "ended" ..........................................................
4.7.2 Endpoint of a Multi-Clock Sequence "matched" ...............................................……
4.7.3 Triggered Method ...................................................................................................……
4.7.4 Sequence events ...................................................................................................………..
Exercises ....................................................................................................................................
5 Advanced Topics For Properties and Sequences ..............................……. 91
5.1 Data types in Properties and Sequences ...........................................................…………..
91
93
5.2 Misuse of Assertion Overlapping ........................................................................………….
98
5.3 Multiple Threads Termination ........................................................................………….
5.4 Assertion Refinement Process ...................................................................................…..
99
5.4.1 Relaxed, stringent assertion ...................................................................................….. 100
5.5 Unbounded Range $ in Properties ......................................................................………… 100
5.6 Recursion ............................................................................................................…………. 101
5.7 Emulating PSL-Like Constructs in SVA .......................................................………….
104
5.7.1 whilenot .............................................................................................................……… 104
5.7.2 The eventually! Operator in Sequence ..................................................................…. 106
5.7.3 Emulating UNTIL with Sequences ......................................................................……. 106
5.7.4 F before G .............................................................................................................……..
107
5.7.5 One-Shot Assertion Using Initial blocks .........................................................……….
108
5.7.5.1 Flag Bit Defining Start of Antecedent ........................................................................ 108
109
5.7.5.2 Procedural Assertion in Initial Block ........................................................................
5.8 Assertion-Based System Functions ......................................................................……..
109
109
5.8.1 Sampled Valued Functions ...................................................................................…..
109
5.8.1.1 Value access functions ...............................................................................................
110
5.8.1.1.1 $sampled(expression [, clocking_event]) ............................................……………
5.8.1.1.2 $past .............................................................................................................………
111
5.8.1.2 Value change functions ...................................................................................……….
113
5.8.1.2.1 $rose and $fell ................................................................................................……… 113
5.8.1.2.2 $stable .............................................................................................................……… 115
5.8.2 Vector-Analysis System Functions .....................................................................……
116
5.8.3 Severity-level System Functions .....................................................................………… 116
117
5.8.4 Assertion-Control System Tasks .....................................................................……….
118
5.9 Clocked Sequence and Multi-Clocking ........................................................…………….
5.9.1 Clock Specification for Properties and Sequences ..........................................…….
118
5.9.2 Clock Resolution ...............................................................................................……..
120
5.9.2.1 Clock Resolution in Assertion and Property Directives ..............................………. 121
5.9.2.2 Clock Resolution in Sequences ................................................................................. 121
5.9.3 Multiple clocked sequences ..................................................................................…….
123
SystemVerilog Assertions Handbook
vi
5.9.3.1 Rules in Using Multiple-Clocked Sequence .......................................................…... 125
5.9.4 Multiple-clocked properties ..................................................................................…….
127
5.9.5 Clock flow ............................................................................................................……… 128
5.9.6 Clocking Rules in Assertions .................................................................................….. 129
5.9.6.1 Single clocked assertions: ..................................................................................……… 130
5.9.6.2 Sequence and Properties in Clocking Blocks ........................................................….
130
5.9.6.3 Multiple-clocked Assertions ..................................................................................…… 131
131
5.10 SystemVerilog Scheduling semantics for Assertions ...........................................…..
5.11 Properties in Interfaces ..................................................................................……….
134
5.12 Verification Directives ............................................................................................…. 135
5.12.1 assert Directive ..............................................................................................……….. 135
5.12.1.1 Concurrent Assertion Statements Outside of Procedural Code .................……. 135
5.12.1.2 Concurrent Assertion Statements Embedded in Procedural Block .................. 136
5.12.1.3 Immediate assertion: .............................................................................................. 137
137
5.12.1.4 Action-block ...........................................................................................................
138
5.12.2 assume Directive ...............................................................................................…….
140
5.12.3 cover Directive ...........................................................................................................
5.12.4 Expect Construct ...............................................................................................……
142
143
5.13 Binding Properties to Scopes or Instances ........................................................……
148
5.14 Verifying VHDL Models with SystemVerilog Assertions ..............................………
148
5.14.1 The Concept ............................................................................................................…..
5.14.2 VHDL Module in VHDL Testbench with SystemVerilog Assertions Module ......
148
5.14.2.1 VHDL Model ........................................................................................................
149
5.14.2.2 SystemVerilog Assertions Module ....................................................................... 149
5.14.2.3 Connecting SystemVerilog Assertions module to VHDL design .................…… 150
5.14.2.3.1 Direct Instantiation of SVA module into VHDL Testbench .............................. 150
5.14.2.3.2 Binding of SVA Verification Module to VHDL Model ..............................…… 151
5.14.3 VHDL Model in a SystemVerilog Testbench with SVA Module .................……….. 152
6 SystemVerilog Assertions In the Design Process ....................................… 153
6.1 Traditional Design Process ...................................................................................……….. 154
154
6.2 Design Process with ABV using SVA as vehicle ............................................…………
6.2.1 System-level Assertions ..................................................................................………...
155
161
6.2.2 Interface Assertions ................................................................................................….
161
6.2.3 Architectural Plan ................................................................................................…….
6.2.4 Verification Plan ................................................................................................……..
162
6.2.5 RTL Design ............................................................................................................……. 163
6.2.6 Write Testbench and Simulate ................................................................................ 164
164
6.2.7 Analyze the Simulation Results and Coverage .........................................................
169
6.2.8 Formal Verification (FV) ...................................................................................……
6.3 Case Study - Synchronous FIFO ......................................................................………..
170
170
6.3.1 Synchronous FIFO Requirements ......................................................................……
182
6.3.2 Verification Plan ................................................................................................……..
191
6.3.3 RTL Design ............................................................................................................…...
6.3.4 Simulation .............................................................................................................…….
193
193
6.3.5 Formal Verification ...............................................................................................…….
Exercises ..................................................................................................................................
195
vii
Preface
199
7 FORMAL VERIFICATION USING ASSERTIONS .........................
200
7.1 FV METHODOLOGY ...................................................................................…………..
203
7.1.1 Model Checking Expectations and Rules .......................................................... …..
204
7.2 Role of SystemVerilog Assertions in FV .........................................................…………
7.2.1 SystemVerilog Assertions in Formal Specifications ............................................….
204
7.2.2 SystemVerilog Assertions Usage in FV vs. Dynamic ABV ...............................…… 205
7.2.2.1 Same Inputs in Antecedent and Consequent ......................................................…..
205
7.3 CASE STUDY - FV OF A TRAFFIC LIGHT CONTROLLER ..................…………. 206
7.3.1 Model ..........................................................................................................................… 206
7.3.2 Basic requirements .................................................................................................…… 209
209
7.3.3 SystemVerilog Assertions for Traffic Light Controller ................................………
7.3.4 Verification ..............................................................................................................….
213
7.3.5 Good Traffic Light Controller ................................................................................... 215
7.4 FV COVERAGE METRICS ....................................................................................……..
216
216
7.4.1 Proof Radius ................................................................................................................
217
7.4.2 Explored State-Based Coverage .......................................................................……..
217
7.4.3 Flip-flop to Property Distance ...................................................................................
7.4.4 Functional Coverage Points ....................................................................................….
217
7.5 EMERGING APPLICATIONS OF SYSTEMVERILOG ASSERTIONS
WITH FORMAL METHODS ............................................................................... 217
217
7.5.1 SystemVerilog Assertions Based Performance Evaluation of Digital Systems .....
7.5.2 Hybrid (dynamic and formal) Verification ..........................................................….
218
219
7.5.3 Directed Random Test Generation from SystemVerilog Assertions ...................…
219
7.5.4 Achieving hard-to-hit functional coverage goals using Formal Methods .....…….
7.6 Temporal Debugging .................................................................................................…….
222
224
7.7 SIMULATION OR FORMAL VERIFICATION? ............................................……….
224
7.7.1 Arguments for Simulation with ABV .........................................................................
225
7.7.2 Arguments for Formal Verification .......................................................................….
7.7.3 Balance ..............................................................................................................………..
225
226
7.7.4 Recommendations .................................................................................................…….
7.7.5 Validity of Formal Verification results ..........................................................………..
226
8 SystemVerilog Assertions Guidelines ..........................................................…. 229
230
8.1 Typographic Guidelines ....................................................................................………….
230
8.1.1 Naming Convention ………………………………………………………………….
230
8.1.1.1 File naming …………………………………………………………………………….
8.1.1.2 Object Naming ……………………………………………………………………….
230
231
8.1.1.3 Naming of Assertion Constructs …………………………………………………….
8.1.2 Ending Statements ……………………………………………………………………
231
8.1.3 Constants for Modules and Interfaces ……………………………………………. 232
8.2 Use Model Guidelines …………………………………………………………………
232
8.2.1 Where to Write Properties and Assertions ………………………………………… 232
234
8.2.2 Assertions for Accuracy ……………………………………………………….………
234
8.2.2.1 Abide by Good Verilog Coding Style Rules ……………………………………….
8.2.2.2 Avoid Nested System Functions …………………………………………………….
234
235
8.2.2.3 Beware of unsized additions in +1 versus +1'b1 …………………………………
237
8.2.2.4 Beware of Property Negation Operator …………………………………………..
8.2.2.5 Ensure "Write before Read" while using Local Assertion Variables …………..
238
SystemVerilog Assertions Handbook
viii
238
8.2.2.6 Be Aware of Overlapping Assertions ……………………………………………….
239
8.2.2.7 Beware of Metalogical Values …………………………………………………….
239
8.2.2.8 Avoid Vacuous Properties ………………………………………………………….
239
8.2.2.9 Avoid Contradictory Properties ……………………………………………….……
8.2.3 Use $sampled Function in Action Block to Display Values of Current Variables
240
8.2.4 Accessing Local Variables in Assertions ……………………………………………… 240
8.2.5 Style ………………………………………………………………………………….… 240
8.2.5.1 Avoid Unbounded Ranges …………………………………………………………… 240
8.2.5.2 Use of Default Clock ………………………………………………………………… 241
8.2.5.3 Evaluate Assertion Relative to a Clock ……………………………………………… 241
8.2.5.4 Handling Resets in Properties ……………………………………………………… 241
8.2.5.5 Defining Time Unit and Time Format Specifications for Design ………………… 242
8.2.5.6 Direct or Implicit Declaration of Properties ………………………………………. 245
8.2.5.7 Use Formal Arguments only when Reuse is Intended …………………………… 246
8.2.5.8 Use module ports or Registered Signals in Properties …………………………… 246
8.2.5.9 Standardize Action Block Error Display …………………………………………… 247
8.2.5.10 Use generate Construct for Assertions Conditional on Parameters …………
247
8.2.5.11 Use Pattern Format in Documenting Assertions ……………………………… 248
248
8.2.5.12 Review Properties and Assertions Against Requirements …………………….
248
8.2.5.13 Simulate Design …………………………………………………………………
249
8.2.5.14 Guidelines for Debugging Assertions ………………………………………….
8.2.6 Using SystemVerilog assertions with Verilog RTL ………………………………….
249
8.2.7 Using Dynamic Data Types inside Properties ………………………………………
250
8.3 Methodology Guidelines …………………………………………………………………. 251
8.3.1 Identifying Properties from Design Specifications ……………………………….… 251
8.3.2 Classification of properties ………………………………………………………….. 251
8.3.2.1 Design Centric . ……………………………………………………………………… 251
8.3.2.1.1 Style in FSM properties …………………………………………………………… 251
253
8.3.2.2 Assumption Centric …………………………………………………………………..
8.3.2.3 Requirement / Verification Centric …………………………………………………
253
254
8.3.2.4 Environmental Properties ………………………………………………………….
8.3.2.5 Coverage Properties …………………………………………………………………
255
8.3.3 Process of Writing Properties and Assertions ……………………………………... 256
9 SystemVerilog Assertions Dictionary ……………………………………… 261
9.1 If COND1, then COND2 ………………………………………………………………. 262
9.2 If COND1, then at next COND2, COND3 ……………………………………………… 262
9.3 If COND1, then after nth COND2, COND3 ……………………………………………. 263
9.4 If COND1 and first COND2, then COND3 until COND4 …………………………….. 264
9.5 If COND1 and first COND2, then sequence ……………………………………………… 264
9.6 Between COND1 and COND2, Signal 1 asserted ……………………………………….. 265
9.7 If COND1 and then 1 occurrence of COND2 then sequence ………………………….. 266
9.8 If COND1 then N Occurrences of COND2 before COND3. N is value of signal …… 266
9.9 If COND1 and within n cycles y occurrences of COND2, then COND3 ……………….. 268
9.10 If COND1, then COND2 until COND3 ……………………………………………… 269
9.11 If Cond1 then Cond2 before Cond3 …………………………………………………. 269
9.12 If COND1 is followed by COND2, and COND3 is not received within 64 cycles while
COND2 then Error (COND5). If COND3 is received within 64 cycles then COND4 ……. 269
ix
Preface
9.13 For every write (COND1), data transfers must alternate between
odd and even entries …………………………………………………………………… 271
9.14 If COND1 then COND2 in N cycles unless COND3 ………………………………… 271
9.15 Data Integrity in Memory. Data read from Memory should be same as
what was last written …………………………………………………………………. 273
9.16 Data Integrity in QUEUES. Interface Data Written must be properly
transferred to the Receiving Hardware ……………………………………………….. 274
9.17 Never 2 consecutive Writes with same Address ……………………………………. 276
9.18 Cache controller requirement: A cached address (COND1) will eventually
be retired (COND2) and after that, within 2 to 7 clocks the cache
copy shall be invalidated (COND3) ………………………………………………….. 277
9.19 during cond1 Never COND3 after COND2. Cond2 may occur within
n cycles after Cond1 …………………………………………………………………. 278
9.20 If COND1, then next N cycles COND2. If new COND1 before end of COND2,
then COND2 extended for N cycles until no COND1 ………………………………. 278
9.21 Never two CONDs within 2 cycles Apart ……………………………………………. 280
9.22 Assume Reset low for initial N cycles ………………………………………………… 281
9.23 If COND1 and N cycle later COND2, then COND3 until COND4, unless COND5 .. 282
9.24 If Sequence COND1 followed by N non-necessarily consecutive COND2,
then N consecutive COND3 until COND4 …………………………………………… 283
9.25 If COND1, COND2 doesn't change for N clocks, unless COND1 goes high again
283
9.26 If a Sequence Starts but does not Complete, then State Register must be in
ERROR state …………………………………………………………………………. 284
9.27 COND1 and COND2 are Mutually Exclusive ……………………………………….. 286
9.28 If Address Error, then eventually good address …………………………………… 287
9.29 Enabling a property after a trigger ………………………………………………….. 288
6 Appendix A Answers to Exercises ……………………………………………. 289
A.1 Answers to Chapter 4 Exercises …………………………………………………………. 289
A.2 Answers to Chapter 6 Exercise …………………………………………………………. 298
Appendix B: Definitions ……………………………………………………………… 305
APPENDIX C: QUICK REFERENCE GUIDE ……………………………… 313
APPENDIX D: CLOCK RESOLUTION ……………………………………….. 317
APPENDIX E: SYSTEMVERILOG ASSERTIONS SYNTAX ………. 321
Index ………………………………………………………………………………………… 325
相关推荐
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
