rockeric.com

前言

基于断言的验证已成为现代设计验证的一个组成部分。并发（concurrent）SVA是一种强大的断言语言，它以简洁的符号和规则表达属性的定义；它的适用范围非常广泛，被强烈推荐使用。

但是，SVA是为静态世界而设计的，这也就造成了一些局限性：

（1）它无法轻松地根据单元变量（模块，检查器，接口）的值解决延迟和重复的使用问题；

（2）它不能引用非静态类属性或方法；

（3）访问大型数据结构，特别是大型动态数据结构时应特别小心；

（4）sequence_match_item不能直接修改单元变量；

（5）在序列的ORing和ANDing中处理属性局部变量（property localvariables）以及这些变量的流程，有非常严格的规则。

SVA可以轻松解决芯片设计要求中最常见的情况，因此这些限制不应被视为SVA的缺点。此外，本文中提供的替代方案仅适用于仿真（simulation），但绝对不适用于形式验证，因为只有断言语言（SVA，PSL）支持形式验证。

本文首先解释了断言基本概念，然后通过示例说明了如何使用SystemVerilog的task在没有SVA的情况下编写相对简单的断言；这为理解多线程和线程退出的概念提供了基础。然后，本文提供了一些示例，演示了如何在保持SVA精神的同时，通过任务来克服某些SVA限制。处理这些问题的另一种方法是使用检查器库，例如OVL，Go2UVM2，（本文并没有涉及）。要强调的是，只有在出现这些限制情况时才能使用具有任务的替代解决方案。

一、概念

断言由两部分组成：

1.属性（property）：属性描述了需求的主体，但不是它在仿真中的启动行为。可以使用automatic task模拟该属性，该任务在触发时启动可以跨越一个或多个周期的独立线程。

2.断言语句（assert statement）：断言语句是在时钟事件中触发属性的机制。该操作可以使用always块进行模拟，在时钟事件中，使用fork/ join_none语句启动自动任务；这更像是从尝试点开始对属性的自动线程进行即发即弃（fire-and-forget）。

任务模型

在对包含前提（antecedent）和结果（consequent）的属性建模时，任务使用if语句模拟SVA前提，并在if语句为false时模拟断言空白（vacuity）的return语句。如果if语句为真（即成功尝试），则任务继续模拟其他序列元素，直到它到达先行端点（antecedent endpoint），但在每个时钟事件处检查该序列是否为真。如果为false，则返回。

在成功完成前提后，任务继续模拟结果。此过程类似于前提中使用的步骤，但它在退出任务之前返回失败消息，return或disable。任务的通用结构如下：  

断言模型

下面是断言语句的模型。在此示例中，下面讨论的任务t_a2b_then_3c与可能使用时钟事件的其他任务并行触发。所有示例的断言语句的仿真如下所示：

二、一个简单的assertion替换示例

（1）常规断言替换：

使用第1节中定义的结构，该断言的属性可表示为：

使用SVA和任务仿真模拟断言产生以下结果：

（ 2）基于单位变量的延迟

考虑与上面类似但稍有不同的断言：

在这个断言中期望的是使延迟由变量中设置的动态值定义。 SVA1800-2017不允许动态定义延迟或重复运算符，它们在elaboration后必须是静态的。为了解决这个问题，在SVA中，必须在属性中定义一组局部变量，然后在成功尝试时设置它们，然后将这些变量用作计数器。除此之外，在某些情况下还必须使用first_match()运算符来强制结束计数。下面是一个解决方案，但看起来相当复杂。

使用任务表示代码更简单，如下所示：

（3）基于单位变量的重复

上述断言是非法的，因为范围range必须在elaboration时进行静态定义。以下是一种解决方法。

使用任务，可以更简单地表达，如下所示：

三、类里的并行断言

数据在类和接口（例如虚拟接口）内可用，但并发断言在类中是非法的。解决方法是将类中的变量复制到接口中，并在这些接口中执行断言。但是，任务的使用减弱了这种复制需求。下面是一个简单的示例，演示了如何在类中使用任务来表达并发断言的概念。

四、用SVA较难描述的复杂断言

SVA的一个问题是在处理ORed序列时局部变量的传递。另一个问题是在多个ORed和ANDed线程中分配和读取局部变量时如何处理局部变量。

考虑一个来自Verification Academy论坛中的实际示例，此模型的要求如下：

1.go升起后，data在数据总线上发送

2.data仅在vld信号为真时有效

3.校验和（chksum）位于数据总线上，并在go下降时断言

4.在校验和（checker sum）的初始化之后，在每个循环vld为真时计算具有溢出的运行和（running sum withoverflow）

5.在chksum循环中，必须将校验和与数据总线上出现的chksum进行比较

Assertion要求的时序图

下图所示的断言看起来应该可以正常工作，但无法编译：

这个属性的问题是局部变量结果不会流出结果中两个序列的ORing；代码无法编译。

另一种SVA解决方案是将错误消息放入函数（选项1）中，同时将结果嵌入到后续的第二个序列中，从而避免上述问题；尽管解决了编译问题，但这个解决方案还是错误的。如下所示：

上面的断言试图表明，在一个go的上升沿之后，sum = 0。然后，在vld == 1的每个时钟周期，我们计算总和sum（局部变量sum = sum + data）。这个过程会重复多达100,000次。除非我们得到了一个go的下降，才会将总和与数据线提供的校验和进行比较。如果计算的校验和与数据行上提供的校验和不匹配，则chek_sum函数将0赋给局部变量结果；这会强制断言失败。这里的想法是，如果没有这种强制值，SVA断言将不会作为失败退出。然而，这个断言也存在逻辑错误，因为在结果中有两个序列的ORing，如果其中一个序列失败，则断言等待第二个序列是否成功；因此它可能等待100,000个周期。

避免这种等待所有可能性的潜在解决方案是使用SVA属性中止操作符(accept_on, reject_on, sync_accept_on, sync_reject_on)。该解决方案无法编译，因为在中止条件下无法引用局部变量。

可以正常工作的SVA解决方案如下所示。它需要两个断言：

1.断言ap_check_msg_OK要求在go的一个上升时，每次出现vld时计算一个cheksum。该操作一直持续到第一次go出现下降（这就是需要first_match操作符的原因）。此后，进行检查以将呈现的校验和与动态计算的校验和进行比较。

2.上述断言要求在一个go的上升沿和下降沿之间必须至少有一个vld；以下断言解决了这种情况：

请注意，尽管SVA确实提供了明确的解决方案，但上述讨论强调了一些可能导致误解的限制。

用任务模拟这个SVA ASSERTION

使用任务消除了线程对局部变量可见性的问题，并使代码更易读和易懂。该任务的以下代码演示了这些概念：

五、结论

并发SVA是一种非常强大的语言，以简洁易读的方式表达相对简单的属性。 SVA在形式验证方面也得到很好的支持。但是，SVA具有一些限制，导致需要使用复杂的方式（例如计数器）来规避语言限制。SVA的替代解决方案有助于解决这些问题，并在某些情况下简化断言的定义。该解决方案依赖于在每个时钟事件中触发的automatic tasks，从而允许充分利用SystemVerilog的所有功能；这些功能包括automatic variable，loop（repeat, forever, while, for）,return，disable，fork-join和立即断言。断言只是一个判断属性为真的声明，因此，用task实现断言是可以接受的。SVA只是一个较短的符号，它能适用于大多数情况，但并非所有情况。

原文来自verificationacademy  

“sva-alternative-for-complex-assertions”

往期精彩：

2019验证VIP春季班   早鸟报名通道扫码报名稿！