《SVA断言系统学习之路》【03】关于布尔表达式
序列中使用的表达式基于其所含变量的采样值进行评估。
表达式评估的结果为布尔值，其解释方式与过程性if语句条件中的表达式完全相同：若表达式计算结果为X、Z 或 0，则被解释为假；否则即为真。
但是，对可出现在并发断言中的表达式存在若干限制。后续章节将具体说明对操作数类型、变量及运算符的限制。
表达式允许包含函数调用，但需遵循以下语义限制：
— 表达式中出现的函数不能包含输出（output）或引用（ref）参数（允许常量引用const ref）；
— 函数应为自动类型（automatic）（或不保留状态信息）且无副作用。
一 操作数类型
1.1 被禁止的类型
- — non-integer types (shortreal, real and realtime)
- — string
- — event
- — chandle
- — class
- — associative arrays
- — dynamic arrays
特别注意：
（1）定长数组，无论是压缩数组还是非压缩数组，都可以整体使用、部分选择使用或通过索引位/部分选择使用。其索引可以是常量、参数或变量。
（2）chandle 是一种特殊的数据类型，它允许 SystemVerilog 代码与用 C 或 C++ 编写的函数和数据结构进行交互。它是在 SystemVerilog 和外部语言（C/C++）之间搭建桥梁的关键数据类型
（3）压缩数组，但数据类型应为 bit 或 logic：typedef logic [3:0] nibble_t;
非压缩数组：typedef int int_array_u [4];
下面举例：typedef int [4] array;
typedef struct { int a, b, c,d } record;
union { record r; array a; } p, q; 允许的比较1：
p.a == q.ap.r == q.r允许的比较2：logic [7:0] arrayA [0:15], arrayB[0:15];arrayA == arrayB; arrayA != arrayB;
arrayA[i] >= arrayB[j];
arrayB[i][j+:2] == arrayA[k][m-:2];
(arrayA[i] & (~arrayB[j])) == 0;1.2 变量
在表达式中出现的变量必须是静态设计变量，或是能返回第17.4.1节所述类型值的函数调用。同时也可以访问在程序（programs）、接口（interfaces）或时钟块（clocking blocks）中声明的静态变量。若引用任务（task）中声明的静态变量，则该变量会像其他变量一样被采样，与任务的调用无关。
1.3 操作符说明
对于第17.4.1节所述类型有效的所有运算符均可使用，但赋值运算符及递增和递减运算符除外。SystemVerilog包含了C语言的赋值运算符（如 +=）以及C语言的递增和递减运算符（++ 和 --）。这些运算符不得在断言中出现的表达式中使用。此项限制可防止副作用产生。
二 序列sequence
请注意：
{} 表示“零次或多次重复”
[ boolean_abbrev ] 布尔缩写操作符（boolean_abbrev）包括：[->n] 或 [=n]：
property 通常由时序行为构建而成。序列功能提供了构建和操作时序行为的能力。最简单的时序行为是线性的。线性序列是一个以时间线性递增顺序排列的有限SystemVerilog布尔表达式列表。
当满足以下条件时，该线性序列被称为在连续时钟周期的有限时间区间内匹配：第一个布尔表达式在第一个时钟周期评估为真，第二个布尔表达式在第二个时钟周期评估为真，依此类推，直至最后一个布尔表达式在最后一个时钟周期评估为真。
单个布尔表达式就是一个简单线性序列的示例：当该布尔表达式在某个时钟周期评估为真时，它就在该时钟周期实现匹配。
更复杂的时序行为由 SystemVerilog 序列描述。序列是建立在 SystemVerilog 布尔表达式之上的正则表达式，它简洁地指定了一组包含零个、有限多个或无限多个线性序列的集合。如果该集合中至少有一个线性序列在连续时钟周期的有限时间区间内匹配，则该序列被认为在该区间内匹配。
一个属性可能涉及对在不同时间点开始的一个或多个时序行为进行检查。对序列的尝试评估即是在特定时钟周期开始搜索该序列的匹配项。为确定此类匹配是否存在，需要从该特定时钟周期开始评估相应的布尔表达式，并在每个后续时钟周期持续评估，直至找到匹配项或推断出不可能存在匹配。
序列可以通过连接组合，类似于列表的拼接。这种连接使用 ## 符号指定从第一个序列结束到第二个序列开始之间的延迟。
以下是序列连接的语法：
在此语法中：
— constant_expression（常量表达式）在编译时计算，且计算结果必须为整数值。
— constant_expression 只能为 0 或正值。
— $ 符号用于指示仿真结束。在形式化验证工具中，$ 用于表示一个有限无界的范围。
— 当使用两个表达式指定范围时，第二个表达式的值必须大于或等于第一个表达式。
序列所处的上下文环境决定了其被评估的时机。序列中的第一个表达式会在触发该序列评估的表达式生效时（或之后）的第一个时钟周期进行检查。序列中的每个后续元素（如果存在）会在紧接着的下一个时钟周期进行检查。
## 后跟数字或范围用于指定从当前时钟周期到后续序列开始之间的延迟。延迟 ##1 表示后续序列的开始时间比当前时钟周期晚一个时钟周期。延迟 ##0 表示后续序列的开始时间与当前时钟周期处于同一时钟周期。
当在两个序列之间作为连接符使用时，该延迟表示从第一个序列结束到第二个序列开始之间的时间间隔。延迟 ##1 表示第二个序列的开始时间比第一个序列的结束时间晚一个时钟周期。延迟 ##0 表示第二个序列的开始时间与第一个序列的结束时间处于同一时钟周期。
以下是延迟表达式的示例。true 是一个布尔表达式，其值始终为真，用于提升视觉清晰度。可将其定义为：
‘define true 1 ##0 a // means a
##1 a // means ‘true ##1 a
##2 a // means ‘true ##1 ‘true ##1 a
##[0:3]a // means (a) or (‘true ##1 a) or (‘true ##1 ‘true ##1 a) or (‘true ##1 ‘true ##1 ‘true ##1 a)
a ##2 b // means a ##1 ‘true ##1 b