Question

一个特性定义了设计的一个行为。一个特性可以作为一个假设、一个检查器或者一个覆盖率规范被用于验证。为了将这种行为用于验证，必须使用一个断言、假设或者覆盖语句。一个特性声明本身不会产生任何结果。

一个特性可以在下列结构中声明：

• 一个模块
• 一个接口
• 一个程序
• 一个时钟控制块
• 一个包
• 一个编译单元作用域

为了声明一个特性，我们可以使用如下所示的property结构：

concurrent_assertion_item_declaration ::=           // 引用自附录A.2.10
    property_declaration
    ...

property_declaration ::=
    property property_identifier[([list_of_formals])];
        {assertion_variable_declaration}
        property_spec;
    endproperty [: property_identifier]

list_of_formals ::= formal_list_item{, formal_list_item}

property_spec ::=
    [clocking_event] [disable iff(expression_or_dist)] property_expr

property_expr ::=
    sequence_expr
  | (property_expr)
  | not property_expr
  | property_expr or property_expr
  | property_expr and property_expr
  | sequence_expr |-> property_expr
  | sequence_expr |=> property_expr
  | if (expression_or_dist) property_expr [else property_expr]
  | property_instance
  | clocking_event property_expr

assertion_variable_declaration ::=
    data_type list_of_variable_identifiers;

property_instance::=
    ps_property_identifier[([actual_arg_list])]

语法17-14 — property结构的语法（摘录自附录A）

与序列声明一样，一个特性在声明的时候可以带有可选的形式参数。当一个特性被实例化的时候，实参可以被传递到特性。通过使用实参替代形参，实参使得特性得到了扩展。语义检查被执行医确保使用实参扩展的特性是合法的。

特性的计算结果要么为“真”要么为“假”。SystemVerilog中具有七种类型的特性：序列、否定、析取（逻辑和）、合取（逻辑积）、if...else、蕴含、实例化。

1) 当且仅当序列没有空匹配的时候，作为序列的特性才计算成“真”。有可能具有空匹配的序列不允许作为特性使用。因为当且仅当具有第一次匹配的时候才具有一次匹配，这样的一个特性的计算与隐含地传递它的sequence_expr到first_match(sequence_expr)相同。只要能够确定sequence_expr的一次匹配，特性的计算结果就被认为是“真”，并且对于该次计算尝试不要求其它的匹配。

2) 如果一个特性具有下列的构成，那么它是一个否定。

not property_expr

对于该特性的每一次计算尝试，都具有一个property_expr的计算尝试。关键字not指出特性的计算返回底层的 property_expr的计算结果的“非”。因此，如果property_expr计算成“真”，那么not property_expr计算为“假”；如果property_expr计算成“”，那么property_expr计算成“真”。

3) 如果一个特性具有如下的构成，那么它就是一个析取。

property_expr1 or property_expr2

当且仅当property_expr1和property_expr2至少有一个被计算成“真”特性才被计算成“真”。

4) 如果一个特性具有如下的格式，那么它就是一个合取。

property_expr1 and property_expr2

当且仅当property_expr1和property_expr2都计算为“真”的时候该特性才被计算成“真”。

5) 如果一个特性具有或者

if (expression_or_dist)
    property_expr1

或者

if (expression_or_dist)
    property_expr1
else
    property_expr2

的构成，那么它就是一个if...else。

当且仅当或者expression_or_dist计算成“假”或者property_expr1计算成“真”的时候第一种格式的特性才被计算成“真”。对于第二种格式的特性，当且仅当expression_or_dist计算成“真”并且property_expr1计算成“真”，或者expression_or_dist计算成“假”并且property_expr2计算成“真”的时候它才被计算成“真”。

6) 如果一个特性或者具有

sequence_expr |-> property_expr

或者具有

sequence_expr |=> property_expr

的格式，那么它就是一个蕴含。

有关蕴含的含义将在17.11.1节中讨论。

7) 一个命名特性的实例可以被用作property_expr或者property_spec。通常，如果命名特性体property_spec能够被实例所替代，使用实参替代形式参数并产生一个合法的property_expr或property_spec，并忽略局部变量声明，那么这个实例就是合法的。因此，例如，如果一个命名特性的实例被用作任意特性构建操作符的一个property_expr操作数，那么这个命名特性就不需要具有一个disable iff子句。类似地，当一个命名特性在一个还调用了其它时钟事件的property_expr或property_spec中实例化的时候，这个命名特性中的时钟事件必须符合多时钟支持的规则。

下面的表格按从高优先级到低优先级的顺序列出了特性操作符，并显示了非一元操作符的关联性。

表17-2：特性操作符的优先级和关联性

SystemVerilog特性操作符	关联性
not	----
and	左
or	左
if...else	右
|-> |=>	右

一条disable iff子句可以被附加到一个property_expr以便产生一个property_spec。

disable iff (expression_or_dist) property_expr

disable iff表达式被称为复位表达式。disable iff子句允许指定异步复位。对于property_spec的一次计算，具有一个底层property_expr的计算。如果在计算完成之前复位表达式变为“真”，那么propterty_spec的整个计算都为“真”。否则，property_spec的计算与property_expr的计算结果相同。对于property_spec的不同的计算尝试，复位表达式都被独立地检测。显式地或者通过实例中的特性实现disable iff子句的嵌套是不被允许的。