16.5 Concurrent assertions overview

并发断言概述：并发断言用于描述随着时间推移的行为，不像立即断言，计算模型基于一个时钟，所以只在时钟节拍出现时计算并发断言。

除了禁用情况和禁用事件，并发断言使用其表达式的采样值，并发断言在观察去被计算。

1、采样

        并发断言和一些其它的结构（比如在一个检查器的always_ff程序中引用的变量）会有特殊的规则用于对其表达式的值进行采样，这些结构之一的表达式的采样值被称作sampled value,在大多数实例中，表达式的采样值是其在前置区域中的值，然而这个规则有一些重要的例外。

        表达式的默认采样值被定义如下所示：（1）静态变量的默认采样值是其声明中指定的值，或者，在没有此类指定的情况下，它是相应类型的默认（或未初始化）值。

（2）任何其它的变量或者网表的默认采样值是相应类型的默认值，例如，类型为logic的变量y的默认采样值是1'bx.

（3）触发事件属性的默认采样值和触发及匹配的序列方法是错误的（1'b0）。

（4）表达式的默认采样值是通过使用其组件子表达式和变量的默认采样值对表达式求值来递归定义的。

        如下文所述，在表达式的采样值定义中使用默认采样值，并且在需要在时间0之前引用表达式的采样值时，在采样值函数的定义中使用默认采样值。

        表达式的采样值的定义是基于变量采样值的定义，变量采样的一般规则如下所示：（1）与大于0的时间相对应的时隙中变量的采样值，是该时隙的前置区域中该变量的值；

（2）与时间0对应的时隙中变量的采样值是其默认采样值。

        表达式的采样值被定义如下所示：

（1）由单个变量组成的表达式的采样值就是该变量的采样值；

（2）常量（const）强制转换表达式的采样值定义为其参数的当前值。例如，如果a是一个变量，那么const'（a）的采样值就是a的当前值。当采样值函数引用常量强制转换表达式的过去值或未来值时，取而代之的是该表达式的当前值。

（3）触发事件属性和触发并匹配（triggered and matched）的序列方法的采样值，定义为事件属性或序列方法返回的当前值。当采样值函数引用事件属性或序列方法的过去或未来值时，该值在相应过去或未来时钟节拍的延迟区域进行采样。

（4）任何其他表达式的采样值都是使用其参数值递归定义的。例如，表达式e1&e2的采样值（其中e1和e2是表达式）是e1和e2的采样值的按位与。特别是，如果表达式包含函数调用，为了计算该表达式的采样值，将在表达式计算时根据其参数的采样值调用该函数。例如，如果a是一个静态模块变量，s是一个序列，f是一个函数，f的采样值（a，s.triggered）是将f应用于a和s.triggered的采样值的结果，即，应用于从预先定义的区域（前置区域）获取的a值和s.triggered的当前值。

2、断言时钟

并发断言规范中采用的计时模型基于时钟信号，并使用时钟周期的广义概念，时钟的定义由用户明确指定，并且可以根据表达式的不同而变化。

        时钟节拍是时间上的一个原子时刻，它本身不跨越任何时间。时钟在任何仿真时间只能标记（tick）一次，该仿真时间的采样值用于评估并发断言。在断言中，采样值是一个时钟周期内变量的唯一有效值。图16-1显示了时钟进程中变量的值，信号req在时钟节拍1和2的值是低（low），在时钟节拍3，该值被采样为高，并保持为高直到节拍6。变量req的采样值在时钟节拍6是低，并在时钟节拍9（含9）之前保持为低。注意，仿真值在时钟节拍9时变为高。但是，时钟节拍9处的采样值是低。

 断言中使用的表达式始终与时钟定义相关联，但使用过程代码中的常量或自动值除外，采样值用于计算确定序列匹配所需的值更改表达式或布尔子表达式（Boolean subexpressions）。

        对于并发断言，如下语句适用：（1）定义的时钟行为必须无故障，这非常重要。否则，可能会采样错误的值；

（2）如果clock表达式中出现的变量，也出现在带有断言的表达式中，则该变量的两种用法的值可能不同。在时钟表达式中使用变量的当前值，而在断言中使用变量的采样值。

        控制序列计算的时钟表达式可能比单个信号名称更复杂。例如clk  &&  gating_signal和clk iff gating_signal之类的表达式可用于表示选通（门）时钟，其他更复杂的表达式也是可能的，然而，为了验证系统的正确行为并尽可能符合真正基于周期的语义，用户应确保时钟表达式无故障，并且在任何模拟时间仅转换一次。

        对$global_clock的引用，可以被理解为：对全局时钟（global clocking）声明中定义的时钟事件（clocking_event）的引用。全局时钟的行为就像其它时钟事件一样，然而在形式验证中，$global_clock（全局时钟）具有额外的意义，因为它被视为主要系统时钟。

        在下面的示例中：

global clocking @clk; endclocking
...
assert property(@$global_clock a);

        断言声明在全局时钟的每个节拍中a都为真。此断言在逻辑上等同于：

assert property(@clk a);

        并发断言的示例如下所示：

base_rule1: assert property (cont_prop(rst,in1,in2)) $display("%m, passing");
else $display("%m, failed");

        关键字property区分并发断言和立即断言，并发断言的语法如下

3、并发断言语法

        属性本身永远不会为检查表达式而求值。在断言语句中使用，以实现检查表达式的目的。

        并发断言语句可以在以下任意语句中指定：（1）always程序或者初始化程序作为语句，无论这些程序出现在何处；（2）module（模块）；（3）interface（接口）；（4）program；（5）generate block；（6）checker。

        断言语句能通过其可选名称被引用，可以使用与SystemVerilog命名约定一致的分层名称。如果未提供名称，工具应为语句指定名称，以便进行报告。

3.1 断言语句

        断言语句用来执行属性，当断言语句的属性评估为真时，动作块的pass语句会被执行；但断言语句的属性评估为假时，动作块的fail语句会被执行；当断言语句的属性评估为禁用时，不执行动作块语句。断言操作重置任务会控制pass和fail语句的执行。

        例如

property abc(a, b, c);
disable iff (a==2) @(posedge clk) not (b ##1 c);
endproperty
env_prop: assert property (abc(rst, in1, in2))
$display("env_prop passed."); else $display("env_prop failed.");

        当不需要执行任何操作时，将指定null语句（即；）。如果没有为else指定语句，则在断言失败时，将使用$error作为语句。

        动作块应不包含任何并发断言、假设、覆盖语句（assert, assume, or cover），然而，动作块能包含立即断言语句。

        并发断言操作块中默认严重性（错误）和严重性系统任务使用的约定应，与即时断言的约定相同。断言语句的pass和fail语句在反应区被执行。

3.2假设断言

        假设语句的目的是：允许将属性视为形式分析以及动态仿真工具的假设，当属性是假设时，工具会约束环境，使该属性保持不变。

        对于形式分析，没有义务验证假定属性是否成立，假设属性可以被视为证明断言属性的假设。

        对于仿真来说，环境必须别限制，这样假定的属性才能保持不变。与断言属性一样，如果假定的属性无法保存，则必须对其进行检查和报告。当假设语句的属性评估为真，动作块的pass语句会被执行；如果其评估为假，动作块的fail语句会被执行。例如：

property abc(a, b, c);
disable iff (c) @(posedge clk) a |=> b;
endproperty
env_prop:
assume property (abc(req, gnt, rst)) else $error(”Assumption failed.”);

        如果属性有一个禁用（disable）评估，动作块的pass和fail语句都不能执行，断言操作控制任务能控制pass和fail语句的执行。

        此外，对于随机仿真，输入上的偏差提供了一种进行随机选择的方法。表达式可以与偏置相关联，如下所示：

expression dist { dist_list } ;

       当属性被认为是驱动随机仿真的假设时， 偏差功能是非常有用的；在assert或cover断言语句中使用带有偏差的属性时，dist运算符等效于inside运算符，并且忽略权重规范。例如：

a1:assume property ( @(posedge clk) req dist {0:=40, 1:=60} ) ;
property proto ;
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty

等价于

a1_assertion:assert property ( @(posedge clk) req inside {0, 1} ) ;
property proto_assertion ;
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty

        在前如上示例中，假设a1中使用分布指定信号req，并将其转换为等效的断言a1_assertion。

        值得注意的是，不管有没有偏差，被假设的属性必须以同样的方法保持。当使用假设语句进行随机仿真时，在特定时间有选择时，偏置只是提供了一种根据指定权重选择自由变量值的方法。

        考虑一个指定简单同步请求和确认协议的例子，其中可以随时提出变量req，并且必须保持断言直到ack被断言。在下一个时钟周期中，必须取消对req和ack的评估。

控制req的属性如下所示：

property pr1;
@(posedge clk) !reset_n |-> !req; // when reset_n is asserted (0),
// keep req 0
endproperty
property pr2;
@(posedge clk) ack |=> !req; // one cycle after ack, req
// must be deasserted
endproperty
property pr3;
@(posedge clk) req |-> req[*1:$] ##0 ack; // hold req asserted until
// and including ack asserted
endproperty

控制rack的属性如下所示：

property pa1;
@(posedge clk) !reset_n || !req |-> !ack;
endproperty
property pa2;
@(posedge clk) ack |=> !ack;
endproperty

在验证必须响应req请求的协议控制器的行为时，应证明断言assert_ack1和assert_ack2，同时假设语句a1，assume_req1,assume_req2, and assume_req3始终有效

a1:assume property (@(posedge clk) req dist {0:=40, 1:=60} );
assume_req1:assume property (pr1);
assume_req2:assume property (pr2);
assume_req3:assume property (pr3);
assert_ack1:assert property (pa1)
else $display("\n ack asserted while req is still deasserted");
assert_ack2:assert property (pa2)
else $display("\n ack is extended over more than one cycle");

覆盖语句Cover statement

        目前感觉用到不多，之后再补吧。