SystemVerilog Assertion精华知识

前言

断言主要用于验证设计的行为。断言也可用于提供功能覆盖率，并标记用于验证的输入激励不符合假定的需求。

在验证平台中，通常进行三个主要任务：

产生激励
功能检查
功能覆盖率度量

在当今的设计越来越复杂情况下，像波形调试这样的方式很容易出现人为错误，因此验证平台应该有一种自动和动态地检查预期结果的方式，这将使调试过程更容易，也使回归测试更有效。功能检查通常针对两个特定领域：

协议检查：检查目标是控制信号，控制信号的有效性是任何设计验证的核心；
数据检查：检查目标是所处理数据的完整性，比如网络传输的数据包是否有损坏；

SystemVerilog中引入的SVA在协议检查和协议覆盖率方面可以发挥重要的作用，它们更接近设计信号，通过将这些断言直接连接到设计，一方面便于管理，另一方面仿真性能可以得到极大的提高。SVA语言本身非常简洁，且提供了很好的时序控制能力。

那么什么是断言(SVA, SystemVerilog Assertion)呢？我们可以找到对它的经典解释。断言是对设计属性的描述：

如果在仿真中检查的属性没有按照我们期望的方式运行，则断言失败；
如果在仿真中出现了在设计中禁止发生的行为属性，则断言失败；

其实简单来说，就是该发生的一定要发生，不应该发生的就决不能发生，否则断言就失败了，进而产生报错信息。

设计属性通常可以从设计的功能规范中提取，并转换为断言。这些断言一方面可以用于功能仿真期间持续监控设计行为，另一方面也可以通过使用Formal技术来验证设计。

SVA调度

SystemVerilog语言是基于事件(events)的执行模型。在每个time slot内，把所有发生的事件按顺序排序处理。关于SV events的调度，可以看下我之前写的一篇文章《详解SystemVerilog中time slot的调度》。通过遵循SV的调度算法，仿真器可以避免设计和验证平台交互过程的错乱，而且也让开发人员有迹可循，写出稳定的代码。断言的采样、评估和执行涉及time slot里的三个regions(区域)。

Preponed：该区域对断言变量进行采样。在这个区域内，net和variable不会改变其状态，这就允许在time slot的开始处采样到最稳定的值。
Observed：所有属性表达式(property expressions)都在该区域中求值。
Reactive：评估属性(property)的成功或失败在这个区域进行。

SystemVerilog事件调度流程图简化如图1所示。

图1 简化的SV事件调度流程图

SVA分类

SystemVerilog语言中定义了两种类型的断言：Concurrent assertions(并发断言)和Immediate assertions(立即断言)。并发断言和立即断言的关键区别是property关键字。

并发断言有这几个特性：

基于时钟周期；
基于所涉及变量在时钟边沿的采样值进行表达式求值；
变量的采样是在Preponed region中完成，表达式的求值是在Observed region中完成；
可以放在procedural block, module, interface, program, general block或checker定义中；
可以在formal和simulation工具中使用；
并发断言语句可以是assert, assume, cover或restrict
可以通过其可选名称来层次引用，当未提供名称时，工具会为其自动生成；

它的定义为：

concurrent_assertion_item ::=
    [ block_identifier : ] concurrent_assertion_statement
    ...
procedural_assertion_statement ::=
    concurrent_assertion_statement
    ...
concurrent_assertion_statement ::=
    assert_property_statement
  | assume_property_statement
  | cover_property_statement
  | cover_sequence_statement
  | restrict_property_statement
assert_property_statement::=
    assert property ( property_spec ) action_block
assume_property_statement::=
    assume property ( property_spec ) action_block
cover_property_statement::=
    cover property ( property_spec ) statement_or_null
cover_sequence_statement::=
    cover sequence ( [clocking_event ] [ disable iff ( expression_or_dist ) ] sequence_expr ) statement_or_null
restrict_property_statement::=
    restrict property ( property_spec ) ;

图2 并发断言定义

立即断言有这几个特性：

基于simulation events语义；
表达式的求值与procedural block中的任何其它Verilog表达式一样，本质上是立即求值的；
必须放在procedural block定义中；
仅用于simulation工具中使用；
立即断言语句可以是assert, assume或cover；

它的定义为：

procedural_assertion_statement ::=
    ...
  | immediate_assertion_statement
    ...
immediate_assertion_statement ::=
    simple_immediate_assertion_statement
  | deferred_immediate_assertion_statement
simple_immediate_assertion_statement ::=
    simple_immediate_assert_statement
  | simple_immediate_assume_statement
  | simple_immediate_cover_statement
simple_immediate_assert_statement ::=
    assert ( expression ) action_block
simple_immediate_assume_statement ::=
    assume ( expression ) action_block
simple_immediate_cover_statement ::=
    cover ( expression ) statement_or_null
deferred_immediate_assertion_item ::= [ block_identifier : ] deferred_immediate_assertion_statement
deferred_immediate_assertion_statement ::=
    deferred_immediate_assert_statement
  | deferred_immediate_assume_statement
  | deferred_immediate_cover_statement
deferred_immediate_assert_statement ::=
    assert #0 ( expression ) action_block
  | assert final ( expression ) action_block
deferred_immediate_assume_statement ::=
    assume #0 ( expression ) action_block
  | assume final ( expression ) action_block
deferred_immediate_cover_statement ::=
    cover #0 ( expression ) statement_or_null
  | cover final ( expression ) statement_or_null
action_block ::=
    statement _or_null
  | [ statement ] else statement_or_null

图3 立即断言定义

断言的声明关键字有以下类型：(属性大家可以把它理解成一种设计行为)

assert: 这个关键字是大家最常见的，它指定属性为要检查的设计行为，并验证该属性是否成立；
assume: 指定属性作为环境的假设。Formal工具使用该信息生成输入激励，仿真器检查属性是否成立；
cover: 收集属性是否被覆盖到；
restrict: 指定属性作为formal验证计算的约束，仿真器不需要检查该属性；（可以看出这个关键字是不用于立即断言的）

构建SVA模块

立即断言的构建比较简单，直接写上assert/assume/cover + statement就好了。这一小节主要是讲并发断言的构建，它有很多种构建方式，这里列下比较常用的方式。

在任何设计模型中，功能都由多个逻辑事件的组合表示。这些事件可以是在同一时钟边沿计算的简单布尔表达式，也可以是涉及多个时钟周期的一段时间内计算的事件。SVA提供了一个关键字来表达这些事件，称为“sequence”。sequence的基本语法如下所示：

sequence name_of_sequence;
    < test_ expression > ;
endsequence

图4 sequence的基本语法

许多sequences可以按逻辑或顺序组合以创建更复杂的sequences。SVA提供了一个关键字来表示这些复杂的顺序行为，称为“property”。property的基本语法如下所示：

property name_of_property;
    < test expression >; or
     < complex sequence expressions >;
endproperty

图5 property的基本语法

property是在仿真期间生效并进行验证的，SVA提供了一个“assert”的关键字来检查property。assert的基本语法如下所示：

assertion_name : assert property ( property_name ) ;

图6 assert的基本语法

因此，创建并发SVA断言所涉及的通用步骤如下图7所示。

图7 创建并发SVA断言通用步骤

例子

5.1 立即断言例子

下面代码为立即断言的一个简单例子：

always_comb begin
    ia_blk: assert(a && b);
end

立即断言ia_blk是作为procedural块的一部分写入的，它遵循信号“a”和“b”的相同事件调度，也就是如果信号“a”和“b”发生变化，那么always_comb块就执行。ia_blk的仿真结果如图8所示。断言成功用向上蓝色箭头表示，断言失败用向下红色箭头表示。

图8 立即断言ia_blk仿真结果

5.2 并发断言例子

下面代码为并发断言的一个简单例子：

sequence s_ab;
    a && b;
endsequence

property p_ab;
    @(posedge clk) s_ab;
endproperty

ca_blk: assert property (p_ab);

并发断言ca_blk的结果如图9所示。同样的，所有的成功用向上蓝色箭头表示，所有的失败用向下红色箭头表示。这个例子中的关键概念是，无论信号“a”和信号“b”是否改变，该属性都在时钟clk的每个上升沿上求值检查。

图9 立即断言ca_blk仿真结果

将立即断言和并发断言对a&&b的仿真检查结果放在一起，结果如图10所示。

图10 立即断言和并发断言对a&&b的仿查结果

从这个结果可以看出，立即断言procedural block中的任何其它Verilog表达式一样，都是当个cycle立即求值的。而并发断言有点像使用default input #1step的clocking block中的信号采样求值。

总结

本文主要是从大框架上梳理SVA的知识点，从为什么需要SVA，有什么好处，SVA分类，SVA调度和检查机制、以及举了两个简单直观的例子，帮忙读者们快速get到SVA的全貌。有了这个宏观了解，对于比较细节(微观)的语法，大家可以翻翻工具书看看，或者用到的时候再查找下。

往期精彩内容：

芯片验证分享系列总结及PPT分享