没有合适的资源?快使用搜索试试~ 我知道了~
首页SystemVerilog Assertion Handbook
SystemVerilog Assertion Handbook
5星 · 超过95%的资源 需积分: 50 111 下载量 171 浏览量
更新于2023-05-25
评论 5
收藏 21.98MB PDF 举报
SystemVerilog Assertion Handbook, 学习systemverilog中断言必备。
资源详情
资源评论
资源推荐
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 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页未读,继续阅读
ysnysn
- 粉丝: 2
- 资源: 11
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- RTL8188FU-Linux-v5.7.4.2-36687.20200602.tar(20765).gz
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
- SPC统计方法基础知识.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论1