SystemVerilogAssertionHandbook_assertiononoff不输出

Assertion

5星 · 超过95%的资源需积分: 50 360 浏览量更新于2023-05-21 评论 4 收藏 21.98MB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

资源详情

资源评论

资源推荐

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

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 iii

Contents

Foreword ………………………………………………………………………………….. xi

Surrendra A. Dudani …………………………………………………………………… xi

Stuart Sutherland ………………………………………………………………………. xiii

Harry D. Foster ……………………………………………………………………….. xv

Tarak Parikh …………………………………………………………………………. xvii

Keith Rieken …………………………………………………………………………… xix

Yu-Chin Hsu …………………………………………………………………………… xxi

Alain Raynaud …………………………………………………………………………. xxiii

Preface

…………………………………………………………………………………….. xxv

Acknowledgements

…………………………………………………………………… xxix

About the authors

……………………………………………………………………… xxxiii

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

1.2.1 Are Assertions Independent from SystemVerilog Structures? ……………………… 5

1.2.2 Are Assertions Useful for the Definition and Verification of Designs? ..................….. 6

1.2.2.1 Captures Designer Intent ................................................................................................ 7

1.2.2.2 Allows Protocols to be Defined and Verified ................................................................... 8

1.2.2.3 Reduces the Time to Market .......................................................................................…. 8

1.2.2.4 Greatly Simplifies the Verification of Reusable IP ...................................................... 8

1.2.2.5 Facilitates Functional Coverage Metrics ...................................................................... 9

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? ...........................................................................…. 10

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

iv SystemVerilog Assertions Handbook

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

3 UNDERSTANDING PROPERTIES ............................................................... 27

3.1 Sequences Overview .....................................................................................................……. 28

3.1.1 Sequence Declaration ..................................................................................................... 29

3.2 SystemVerilog Properties ........................................................................................……… 31

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

3.2.5.1 Clocking Event .....................................................................................................……… 39

3.2.5.2 Disabling condition .....................................................................................................….. 40

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

4.5 Repetition Operators ....................................................................................................….. 64

4.5.1 Consecutive Repetition .................................................................................................. 66

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

Preface v

4.5.3 Sequence goto Repetition ([->n ]) ..........................................................................……. 74

4.6 Sequence Composition Operators ..........................................................................……….. 75

4.6.1 Sequence Fusion (##0) .................................................................................................... 76

4.6.2 Sequence Disjunction (or) .......................................................................................…… 76

4.6.3 Sequence Non-Length-Matching (and) .............................................................………. 77

4.6.4 Sequence Length-Matching (intersect) ...................................................................… 77

4.6.5 Sequence Containment (within) .........................................................................……… 78

4.6.6 Conditions over Sequences (throughout operator) ...............................................……. 79

4.7 Methods Supporting Sequences .........................................................................………… 80

4.7.1 Endpoint of a Single Clock Sequence "ended" .......................................................... 80

4.7.2 Endpoint of a Multi-Clock Sequence "matched" ...............................................…… 83

4.7.3 Triggered Method ...................................................................................................…… 84

4.7.4 Sequence events ...................................................................................................……….. 85

Exercises .................................................................................................................................... 86

5 Advanced Topics For Properties and Sequences ..............................……. 91

5.1 Data types in Properties and Sequences ...........................................................………….. 91

5.2 Misuse of Assertion Overlapping ........................................................................…………. 93

5.3 Multiple Threads Termination ........................................................................…………. 98

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

5.7.5.2 Procedural Assertion in Initial Block ........................................................................ 109

5.8 Assertion-Based System Functions ......................................................................…….. 109

5.8.1 Sampled Valued Functions ...................................................................................….. 109

5.8.1.1 Value access functions ............................................................................................... 109

5.8.1.1.1 $sampled(expression [, clocking_event]) ............................................…………… 110

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

5.8.4 Assertion-Control System Tasks .....................................................................………. 117

5.9 Clocked Sequence and Multi-Clocking ........................................................……………. 118

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

vi SystemVerilog Assertions Handbook

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

5.10 SystemVerilog Scheduling semantics for Assertions ...........................................….. 131

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

5.12.1.4 Action-block ........................................................................................................... 137

5.12.2 assume Directive ...............................................................................................……. 138

5.12.3 cover Directive ........................................................................................................... 140

5.12.4 Expect Construct ...............................................................................................…… 142

5.13 Binding Properties to Scopes or Instances ........................................................…… 143

5.14 Verifying VHDL Models with SystemVerilog Assertions ..............................……… 148

5.14.1 The Concept ............................................................................................................….. 148

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

6.2 Design Process with ABV using SVA as vehicle ............................................………… 154

6.2.1 System-level Assertions ..................................................................................………... 155

6.2.2 Interface Assertions ................................................................................................…. 161

6.2.3 Architectural Plan ................................................................................................……. 161

6.2.4 Verification Plan ................................................................................................…….. 162

6.2.5 RTL Design ............................................................................................................……. 163

6.2.6 Write Testbench and Simulate ................................................................................ 164

6.2.7 Analyze the Simulation Results and Coverage ......................................................... 164

6.2.8 Formal Verification (FV) ...................................................................................…… 169

6.3 Case Study - Synchronous FIFO ......................................................................……….. 170

6.3.1 Synchronous FIFO Requirements ......................................................................…… 170

6.3.2 Verification Plan ................................................................................................…….. 182

6.3.3 RTL Design ............................................................................................................…... 191

6.3.4 Simulation .............................................................................................................……. 193

6.3.5 Formal Verification ...............................................................................................……. 193

Exercises .................................................................................................................................. 195

剩余360页未读，继续阅读

gxy198715a

2019-10-12

书挺不错，上次下载完，不小心给删除了

ysnysn

粉丝: 2
资源: 11

会员权益专享

SystemVerilog Assertion Handbook

评论1

会员权益专享

最新资源

SystemVerilog Assertion Handbook

评论1

systemverilog assertion

systemverilog_assertion.pdf

systemverilog硬件设计及建模

如何快速学习systemverilog

systemverilog 副教授 日本

SystemVerilog 事件 信箱 旗语

systemverilog项目

vscode配置systemverilog

systemverilog this 跟super的差别

systemVerilog学习笔记PPT

systemverilog 位拼接运算符 数组

vscode中关于systemverilog uvm verilog的好的插件

systemverilog查找字符串

systemverilog

systemverilog和verilog区别

用systemverilog写一个UART验证平台

systemverilog与功能验证

verilog与systemverilog区别

systemverilog绿皮书中文pdf

systemverilog clocking

会员权益专享

最新资源

systemverilog 副教授日本

SystemVerilog 事件信箱旗语

systemverilog 位拼接运算符数组