Question

主题

主题	描述
17.1 简介（一般信息）	SystemVerilog加入了为一个系统指定断言的功能。断言说明了系统的一个行为。断言主要用来验证一个设计的行为。另外，断言可以被用来提供功能覆盖以及产生验证的输入激励。 SystemVerilog具有两种类型的断言：并发断言和即时断言。 即时断言的执行遵从仿真事件语义并且像一个过程块中的一条语句一样执行。即时断言的主要目的是与仿真一起使用。 并发断言基于时钟语义并使用变量的采样值。SystemVerilog断言的目标之一就是为断言提供一个公共的语义，这样它们可以被用来驱动不同的设计和验证工具。许多工具，例如形式验证工具，使用基于周期的语义来评估电路描述，典型情况下这种方法依赖于一个时钟信号或者信号组来驱动电路的评估。在时钟沿之间的任何时序或事件行为都会被忽略。并发断言结合了这些时钟语义。虽然这种方法通常简化了一个电路描述的评估，然而却存在一些情况，在这些情况下基于周期的评估提供了与标准的SystemVerilog基于事件的计算不同的行为。 本章表述了这两种类型的断言。
17.2 即时断言	即时断言语句是一个表达式的测试，当语句在程序代码中执行的时候完成。表达式是非时间的，并且按一个过程化if语句的条件中的表达式相同的方式解释。也就是说，如果表达式计算成X、Z或0，那么它被解释成假并且认为断言失败。否则，表达式被解释成真，并且认为断言通过。 即时断言语句是一个statement_item，并且可以在一个过程化语句被说明的任意地方说明。
17.3 并发断言概述	并发断言描述了贯穿时间的行为。与即时断言基于时钟的计算模型不同，并发断言仅在一个时钟标记出现的时候被计算。在计算中使用的变量值是采样的值。通过这种方式，我们可以获得一个可预测的结果，而不管仿真器内部的对事件进行排序和计算的机制如何。这种模型也对应于从RTL描述获得的硬件解释的综合模型。 断言中使用的变量值在一个时隙的Preponed区域被采样，并且断言在Observe区域被计算。这一点在第十四章 调度语义中解释。 一个并发断言规范采用的时序模型基于时钟标记并使用一个通用的时钟周期概念。一个时钟的定义由用户明确地说明并且在表达式之间可以存在不同。 一个时钟标记是时间上的一个原子瞬间，它本身并不具有在时间上的持续期。在任意仿真时间，一个时钟应该只标记一次，并且在这个仿真时间上采样的值被用于当前断言的计算。在一个断言中，采样值是一个时钟标记上变量唯一有效的值。图17-1显示了随着时钟的推进一个变量的值。在时钟标记1和2，req信号的值是低。在时钟标记3，采样的值为高并保持为高直到时钟标记6。变量req在时钟标记6处的采样值为低并保持为低直到时钟标记10。注意，仿真值跃变到高发生在时钟标记9。然而，时钟标记9处的采样值仍为低。 图17-1 — 在仿真标记上采样一个变量 在一个表达式中使用的表达式总是被绑定到一个时钟定义。采样值被用来计算值变化表达式或者用来确定一个序列匹配的布尔子表达式。 注意： 一个重要的一点是要确保定义的时钟行为是没有毛刺的。否则会采样到错误的值。 如果一个出现在时钟表达式中变量也出现在一个断言表达式中，那么这个变量的值在两个使用中可以是不同的。变量的当前值被用在时钟表达式中，而变量的采样值则用于断言。 控制序列计算的时钟表达式可以比仅仅是单一的信号名更加复杂。诸如(clk && gating_signal)和(clk iff gating_signal)之类的表达式可以被用来代表一个门时钟。其它更加复杂的表达式也是可能的。然而，为了确保正确的系统行为并尽可能真正地符合基于周期的语义，一个时钟表达式中的信号必须是无毛刺的，并且在任何仿真时间只能跃变一次。 并发断言的一个例子如下：
17.4 布尔表达式	在序列中使用的表达式针对表达式中出现的变量的采样值进行计算。一个表达式计算的结果是布尔值，并且与一个过程化if语句中条件表达式的解释方式相同。也就是说，如果表达式计算成X、Z、或0，那么它被解释成“假”。否则解释成“真”。 出现在并发断言中的表达式存在某些限制。对操作数类型、变量和操作符的限制在后续的章节中描述。 表达式可以包含函数调用，但存在某些语义限制。 出现在表达式中的函数不能包含输出或ref参数（允许使用const ref）。 函数应该是自动的（或者不保留状态信息）并且没有边带效应。
17.5 序列
17.6 声明序列	一个序列可以在下列单元中声明： 一个模块 一个接口 一个程序 一个时钟控制块 一个包 一个编译单元的作用范围 序列使用下列的语法进行声明：
17.7 序列操作
17.8 处理一个序列中的数据	使用一个SystemVerilog静态变量意味着仅存在它的一份拷贝。如果需要在流水线设计中检查数据值，那么对于每一个进入流水线的数据量值，我们可以使用一个单独的变量来存储预期的流水线输出，以便在真正退出管线的时候比较结果。这个存储空间可以通过使用一个变量数组来构建，并且为了最小化通过流水线的传播这个数组可以安排在一个移位寄存器中。然而，在一些更为复杂的情况下，例如管线的潜伏期是可变的并且是乱序的，那么这种结构可能就变得非常复杂并且容易出错。因此，我们需要一些局部变量，这些变量在一个特定的、能够跨越任意时间间隔的事务检查中使用，并且能够与其它事务检查重叠。所以，这样的一个变量必须能够在需要的时候在一个序列实例中动态地产生并能在序列结束的时候移除。 一个变量的动态产生极其赋值是通过在一个序列或特性声明中使用局部变量声明并在序列中赋值来实现的。
17.9 在一个序列匹配时调用子程序	任务、任务方法、void函数、void函数方法以及系统任务可以在一个序列成功匹配的结束处调用。子程序调用，例如局部变量赋值，出现在紧跟着序列的以逗号分割的列表中。子程序调用被称为附加到序列。序列以及之后的列表以括号包围。
17.10 系统函数	断言一般被用来计算一个设计实现的某些特定属性，例如一个特定的信号是否为“热点（one-hot）”。SystemVerilog中包含下列系统函数来促进这些基本的断言功能： $onehot(<expression>) ：如果表达式中只有一位为高，那么返回“真”。 $onehot0(<expression>) ：如果表达式中至少有一位为高，那么返回“真”。 $isunknown(<expression>) ：如果表达式任何一位为X或Z，那么返回“真”，等价于：^<expression> === 'bx。 所有上述的系统函数都具有一个bit类型的返回值。1'b1的返回值指示“真”，1'b0的返回值指示“假”。 为布尔表达式提供的另外一个有用的函数是$countones，它可以计算一个位向量表达式中1的数目。
17.11 声明特性	一个特性定义了设计的一个行为。一个特性可以作为一个假设、一个检查器或者一个覆盖率规范被用于验证。为了将这种行为用于验证，必须使用一个断言、假设或者覆盖语句。一个特性声明本身不会产生任何结果。 一个特性可以在下列结构中声明： 一个模块 一个接口 一个程序 一个时钟控制块 一个包 一个编译单元作用域 为了声明一个特性，我们可以使用如下所示的property结构：
17.12 多时钟的支持	多时钟序列和特性可以使用下列的语法说明。
17.13 并发断言	A property on its own is never evaluated for checking an expression. It must be used within a verification statement for this to occur. A verification statement states the verification function to be performed on the property. The statement can be one of the following: assert to specify the property as a checker to ensure that the property holds for the design assume to specify the property as an assumption for the environment cover to monitor the property evaluation for coverage A concurrent assertion statement can be specified in: an always block or initial block as a statement, wherever these... more
17.14 时钟解析	SystemVerilog具有多种方法为一个特性指定时钟。 — 具有一个时钟的序列实例，例如：
17.15 将特性绑定到作用域或实例	To facilitate verification separate from the design, it is possible to specify properties and bind them to specific modules or instances. The following are the goals of providing this feature: It allows verification engineers to verify with minimum changes to the design code/files. It allows a convenient mechanism to attach verification IP to a module or an instance. No semantic changes to the assertions are introduced due to this feature. It is equivalent to writing properties external to a module, using hierarchical path names. With this feature, a user can bind a module, interface, or program instance to a module... more
17.16 expect语句	The expect statement is a procedural blocking statement that allows waiting on a property evaluation. The syntax of the expect statement accepts a named property or a property declaration, and is given below.

链接 主题