每次看复杂断言都在考验阅读理解能力,还有没有其它解药?

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春季班   早鸟报名通道扫码报名稿!
实锤!30W+!!!2018芯片校招薪资比肩互联网!
理解UVM-1.2到IEEE1800.2标准的变化,掌握这3点就够了
Verification和Validation傻傻分不清楚?面经重点!
没想到,双十一只花10块钱,我竟然爱上了加班
人工智能和机器学习让验证更快更智能

发表评论

邮箱地址不会被公开。 必填项已用*标注

陕ICP备18003383号-1