A Practical Introduction to PSL

jmwen

A Practical Introduction to PSL
A Practical Introduction to PSL.rar (1.08 MB, 下载次数: 183 )

2008-9-15 21:08 上传

点击文件名下载附件

Cindy Eisner
IBM Haifa Research Laboratory
Haifa 31905 Israel

Dana Fisman
The Weizmann Institute of Science
Rehovot 76100 Israel

Contents
Foreword . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .VII
Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . IX
1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
2 Basic Temporal Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.1 The always and never operators . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2 The next operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.3 Variations on next including next event . . . . . . . . . . . . . . . . . . . 8
2.4 The until and before operators . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.5 eventually! . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3 Some Philosophy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.1 Assertions vs. properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 The notion of time . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.3 Designs and traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.4 Current cycle, sub-traces, and modularity . . . . . . . . . . . . . . . . . . 20
3.5 Reporting a failure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
4 Weak vs. Strong Temporal Operators . . . . . . . . . . . . . . . . . . . . . . 27
4.1 The next! operator. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.2 Variations on next! including next event! . . . . . . . . . . . . . . . . . 29
4.3 The until! and until! operators . . . . . . . . . . . . . . . . . . . . . . . . 31
4.4 The before! and before! operators . . . . . . . . . . . . . . . . . . . . . . 32
4.5 Operators without weak or strong versions . . . . . . . . . . . . . . . . . . 33
5 SEREStyle. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5.1 Suffix implication (|-> and |=>). . . . . . . . . . . . . . . . . . . . . . . . . . . 36
5.2 Weak and strong SEREs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.3 The never operator applied to a SERE . . . . . . . . . . . . . . . . . . . . 42
XII Contents
5.4 SERE repetition operators ([*n], [=n], and [->n]) . . . . . . . . . 43
5.5 Concatenation (;) and fusion ( . . . . . . . . . . . . . . . . . . . . . . . . . . 47
5.6 Compound SEREs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
5.7 More about suffix implication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
5.8 The built-in function ended() . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.9 Overlapping matches of a SERE. . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.10 How not to use SEREs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
6 Clocks. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6.1 Edge-triggered designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
6.2 Level-sensitive designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
6.3 Sampling semantics and the granularity of a cycle . . . . . . . . . . . 73
6.4 Placement of the clock . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.5 Checking for glitches in a clocked design . . . . . . . . . . . . . . . . . . . . 76
6.6 Checking for races with the clock in a clocked design . . . . . . . . . 77
6.7 Using the clock operator to simplify properties . . . . . . . . . . . . . . 78
6.7.1 Simplifying properties for a cycle-based trace . . . . . . . . . 78
6.7.2 Simplifying properties for a non-cycle-based trace . . . . . 79
6.8 The default clock . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
6.9 Embedding asynchronous properties . . . . . . . . . . . . . . . . . . . . . . . 81
7 Aborting a Property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
7.1 Properties whose outermost operator is not always . . . . . . . . . . 86
7.2 Synchronous vs. asynchronous abort . . . . . . . . . . . . . . . . . . . . . . . 89
8 Some Convenient Constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
8.1 Comments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
8.2 Named properties and SEREs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
8.3 The forall operator. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
8.4 Parameterized properties and SEREs . . . . . . . . . . . . . . . . . . . . . . 95
8.5 Macros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
9 The Simple Subset. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
10 The Boolean, Modeling, and Verification Layers . . . . . . . . . . . 103
10.1 The Boolean layer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
10.2 The modeling layer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
10.3 The verification layer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
10.3.1 Verification units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
10.3.2 Verification directives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
11 Advanced Topics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
11.1 Finite traces – the four levels of satisfaction . . . . . . . . . . . . . . . . . 109
11.2 LTL style vs. SERE style . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
11.3 Common equivalences in LTL style . . . . . . . . . . . . . . . . . . . . . . . . 113
11.4 PSL for formal verification. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
Contents XIII
11.4.1 Infinite traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
11.4.2 The Optional Branching Extension (OBE) . . . . . . . . . . . . 115
11.4.3 The union operator and the built-in function nondet() 116
11.4.4 The built-in function next() . . . . . . . . . . . . . . . . . . . . . . . . 117
11.4.5 Vunit scoping rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
11.4.6 Safety and liveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
11.5 Vacuity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
11.6 Flavor issues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
12 More Philosophy – High- vs. Low-level Assertions . . . . . . . . . 123
12.1 A simple state machine. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
12.2 A simple fifo. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126
12.3 A simple bus interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
12.4 Summing up . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
13 Common Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
13.1 Common errors with implications . . . . . . . . . . . . . . . . . . . . . . . . . . 131
13.1.1 Confusing a logical implication with a suffix implication 131
13.1.2 Confusing a logical implication with an “and” . . . . . . . . . 132
13.1.3 Confusing a logical implication with a concatenation . . . 133
13.1.4 Confusing a suffix implication with a concatenation . . . . 134
13.1.5 Using never with implications . . . . . . . . . . . . . . . . . . . . . . 135
13.1.6 Negating implications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
13.1.7 Incorrect nesting of implications . . . . . . . . . . . . . . . . . . . . . 138
13.1.8 Incorrect placement of the suffix implication operator . . 141
13.1.9 Applying eventually! to an implication . . . . . . . . . . . . . 141
13.2 Common errors with abort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
13.2.1 Confusing abort and until . . . . . . . . . . . . . . . . . . . . . . . . 143
13.2.2 Confusing abort with an “or” . . . . . . . . . . . . . . . . . . . . . . 145
13.2.3 Incorrectly aborting a never property. . . . . . . . . . . . . . . . 146
13.2.4 Incorrectly aborting an initial condition . . . . . . . . . . . . . . 147
13.3 Thinking you are missing a “first match” operator . . . . . . . . . . . 148
13.4 Assertions that may say less than you think . . . . . . . . . . . . . . . . 150
13.4.1 “Extraneous” assertions of signals . . . . . . . . . . . . . . . . . . . 150
13.4.2 Specifying a one-to-one correspondence between signals 150
13.5 Assertions that may say more than you think . . . . . . . . . . . . . . . 156
13.6 A False “equivalence” . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
13.7 Unspoken assumptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
14 Multiply-clocked Designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
14.1 Declaring auxiliary clocks. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
14.2 Multiply-clocked designs vs. properties . . . . . . . . . . . . . . . . . . . . . 167
14.3 Nesting of clocks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
14.4 A “behind the scenes” view of clocking . . . . . . . . . . . . . . . . . . . . . 168
14.5 Clocks that are not well-behaved . . . . . . . . . . . . . . . . . . . . . . . . . . 172
XIV Contents
A Syntax Rule Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
A.1 Conventions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
A.2 Tokens . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
A.3 hdl dependencies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
A.3.1 verilog extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179
A.3.2 Flavor macros. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179
A.4 Syntax productions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
A.4.1 Verification units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
A.4.2 PSL declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182
A.4.3 PSL directives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
A.4.4 PSL properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
A.4.5 Sequential Extended Regular Expressions (SEREs) . . . . 186
A.4.6 Parameterized Properties and SEREs . . . . . . . . . . . . . . . . 187
A.4.7 Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187
A.4.8 Forms of expression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188
A.4.9 Optional Branching Extension . . . . . . . . . . . . . . . . . . . . . . 189
B Formal Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
B.1 Typed-text representation of symbols . . . . . . . . . . . . . . . . . . . . . . 191
B.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
B.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
B.3.1 Semantics of FL formulas. . . . . . . . . . . . . . . . . . . . . . . . . . . 193
B.3.2 Semantics of OBE formulas . . . . . . . . . . . . . . . . . . . . . . . . . 197
B.4 Syntactic Sugaring. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198
B.4.1 Additional SERE operators . . . . . . . . . . . . . . . . . . . . . . . . . 198
B.4.2 Additional FL operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199
B.4.3 Parameterized SEREs and formulas . . . . . . . . . . . . . . . . . . 200
B.5 Rewriting rules for clocks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201
C Operator Precedence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203
D Quick Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205
D.1 Logical operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205
D.1.1 Verilog, SystemVerilog and SystemC flavors. . . . . . . . . . . 205
D.1.2 Logical operators in the VHDL flavor . . . . . . . . . . . . . . . . 206
D.1.3 Logical operators in the GDL flavor . . . . . . . . . . . . . . . . . 207
D.2 LTL style. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
D.2.1 always, never and eventually! . . . . . . . . . . . . . . . . . . . . 208
D.2.2 The next* operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
D.2.3 The next event* operators . . . . . . . . . . . . . . . . . . . . . . . . . 209
D.2.4 The until* and before* operators . . . . . . . . . . . . . . . . . . 210
D.2.5 Abort operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210
D.2.6 LTL operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211
D.3 SERE style . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 212
D.3.1 Consecutive repetition operators . . . . . . . . . . . . . . . . . . . . 212
Contents XV
D.3.2 Non-consecutive and goto repetition operators. . . . . . . . . 213
D.3.3 Other SERE operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 214
D.3.4 Common SERE style properties . . . . . . . . . . . . . . . . . . . . . 215
D.4 Clocking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
D.4.1 Clocking properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
D.4.2 Clocking SEREs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
D.5 Boolean, modeling and verification layers . . . . . . . . . . . . . . . . . . . 217
D.5.1 Built-in functions concerning time . . . . . . . . . . . . . . . . . . . 217
D.5.2 Other built-in functions and the union operator . . . . . . . 218
D.5.3 Verification directives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
D.5.4 Verification units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 220
D.6 Some convenient constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
D.6.1 Comments and Macros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
D.6.2 Named properties and SEREs . . . . . . . . . . . . . . . . . . . . . . . 222
D.6.3 The forall operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223
Bibliographic Notes. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225
References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235

fslrayman

很早这里就有这个书了，没必要再传吧
而且现在SV这么火，为啥不去学SVA，而要学PSL呢？

jmwen

thanks

原帖由 reynold256 于 2008-9-17 12:47 发表

                               
登录/注册后可看大图

good!!!!!!!!!!!!!!!!!!!!!!!!!!

hwlyic

适合使用ncverilog工具的兄弟，用vcs推荐使用sva

jmwen

确实

原帖由 hwlyic 于 2008-9-28 11:36 发表

                               
登录/注册后可看大图

适合使用ncverilog工具的兄弟，用vcs推荐使用sva

honghf2275

dingdingding

WAXABC

不错,学习一下

pmsvq

多谢楼主共享这本书。

yjj1001

Good!
Thank you for your sharing!
Good!
Thank you for your sharing!

yjj1001

Good!
Thank you for your sharing!