Question

蕴含结构指出一个特性检查是在一个有序前项匹配的基础上有条件地执行的。

property_expr ::=            // 引用自附录A.2.10
    ...
  | sequence_expr |-> property_expr
  | sequence_expr |=> property_expr

语法17-15 — 蕴含语法（摘录自附录A）

上面的子句可以用于一个表达式的预处理监视，并允许将其使用在特性级。蕴含的结果要么为“真”要么为“假”。左侧操作数sequence_expr被称为前项，而右侧的操作数property_expr则被称为后项。

对于|->蕴含，我们需要注意以下几点：

• 从一个指定的起始点开始，先项sequence_expr可以具有0个、一个、或多个成功的匹配。
• 如果从一个指定的起始点开始没有前项sequence_expr的匹配，那么从这个起始点开始的蕴含的计算会无意义地成功并且返回“真”。
• 对于前项sequence_expr的每一次成功匹配，后项property_expr会被单独计算。前项sequence_expr匹配的结束点是后项property_expr计算的起始点。
• 从一个指定的起始点开始，当且仅当起始于这个起始点的前项sequence_expr匹配，并且起始于前项匹配的结束点的后项property_expr成功匹配并返回“真”的时候，蕴含的计算才会成功并返回“真”。

SystemVerilog提供了两种形式的蕴含：交迭的蕴含使用|->操作符；非交迭的蕴含使用|=>操作符。对于交迭的蕴含，如果前项sequence_expr具有一次匹配，那么该次匹配的结束点即为后项property_expr计算的起始点。对于非交迭的蕴含，后项property_expr计算的起始点位于sequence_expr匹配的结束点之后的那个时钟标记。因此：

sequence_expr |=> property_expr

等价于：

sequence_expr ##1 `true |-> property_expr

在多时钟序列和特性中使用蕴含的情况将在17.12节中详细解释。

下面的例子演示了一个总线操作，在这个例子中数据从一个主设备传输到一个从设备。当总线进入到一个数据传输阶段的时候，可能具有多个数据阶段以便传输一个数据块。对于数据传输阶段，如果在时钟信号的任一上升沿irdy有效并且trdy或stop信号有效，那么一个数据阶段结束。注意，这里的有效指的是信号的值为“低”。一个数据阶段的结束可以使用下面的方式表达：

property data_end;
    @(posedge mclk)
        data_phase |-> ((irdy==0) && ($fell(trdy) || $fell(stop)));
endproperty

每次当一个数据阶段为“真”的时候，我们识别出了一个data_phase的匹配。在时钟标记6处的计算尝试在图17-13中演示。图中所显示的信号值是相对于时钟的采样值。在时钟标记6处，data_end为“真”，因为stop信号变为有效同时irdy信号也是有效的。

图 17-13 — 有条件的序列匹配

在另外一个例子中，data_end_exp被用来确保frame在data_end_exp出现后的两个时钟标记内无效（值为“高”）。更进一步，它还要求在frame变为无效后的一个时钟标记上irdy无效（值为“高”）。

可以用来表达这个条件的一个特性如下所示：

`define data_end_exp (data_phase && ((irdy==0)&&($fell(trdy)||$fell(stop))))
property data_end_rule1;
    @(posedge mclk)
        `data_end_exp |-> ##[1:2] $rose(frame) ##1 $rose(irdy);
endproperty

特性data_end_rule1首先在每一个时钟标记上计算data_end_exp以测试它的值是否为“真”。如果它的值为“假”，那么对于data_end_rule1的计算尝试被认为是“真”。否则会计算紧随其后的序列。

##[1:2] $rose(frame) ##1 $rose(irdy)

上面的序列在接下来的两个时钟标记内寻找frame信号的上升沿。在frame反转为高后，irdy信号也必须在一个时钟标记之后反转为高。图17-14演示了在时钟标记6处的计算尝试。`data_end_exp在时钟标记6处被确认。接下来，frame信号在时钟标记7处反转为高。由于它满足由[1:2]所施加的约束，所以它满足这个序列并且继续进行下一步的计算。在时钟标记8处，irdy信号被计算。信号irdy在时钟标记8处跃变为高，对于开始于时钟标记6处的计算尝试，它完全满足序列规范。

图17-14 — 有条件的序列

通常，断言与一些先决条件相关联，因此所执行的检查也仅仅发生在某些特性的条件下。正像前一个例子所看到的那样，|->操作符提供了这种能力来说明在计算它们的结果特性之前序列必须满足的先决条件。下面的例子修改了前一个例子，通过删除了结果的先决条件，我们可以看到它对断言结果的影响。如图17-15所示。

property data_end_rule2;
    @(posedge mclk)
        ##[1:2] $rose(frame) ##1 $rose(irdy);
endproperty

图17-15 — 没有先决条件产生的结果

上述特性在每一个时钟标记处进行计算。对于时钟标记1处的计算，在时钟标记1或时钟标记2处没有出现frame信号的上升沿，所以特性在时钟标记1失败。类似的，在时钟标记2、3和4处特性也是失败的。对于起始于时钟标记5和6处的计算尝试，时钟标记7处发生的frame信号的上升沿使得特性能够得到进一步的检查。根据规范，序列在时钟标记8处结束，对于起始于5和6处的计算尝试会产生一次匹配。因为$rose(frame)没有再次发生，所以所有后续的序列匹配计算尝试都是失败的。

从图17-15中可以看出，将检查的先决条件‘data_end_exp从断言中删除会导致与验证目标不相关的失败。从确认的立场来看，确定先决条件并用其过滤掉不恰当或无关的条件是非常重要的。

蕴含操作中前项是一个序列的例子如下所示：

(a ##1 b ##1 c) |-> (d ##1 e)

如果序列(a ##1 b ##1 c)匹配，那么序列(d ##1 e)也必须匹配。换句话说，如果序列(a ##1 b ##1 c)没有匹配，那么结果为“真”。

蕴含的另外一个例子如下：

property p16;
    (write_en & data_valid) ##0
    (write_en && (retire_address[0:4]==addr)) [*2] |->
    ##[3:8] write_en && !data_valid &&(write_address[0:4]==addr);
endproperty

作为一种选择，这个特性可以被编码成一个嵌套的蕴含：

property p16_nested;
    (write_en & data_valid) |->
    (write_en && (retire_address[0:4]==addr)) [*2] |->
    ##[3:8] write_en && !data_valid &&(write_address[0:4]==addr);
endproperty

多时钟序列的蕴含操作将在17.12节中解释。