你知道用于AMBA协议的“Checker IP”是如何构建的吗

你知道用于AMBA协议的“Checker IP”是如何构建的吗

译者小注:本文主要阐述了verification IP中的一个子集:checker IP。这一术语由本文的作者提出,用于区别传统的VIP。在文中,作者分享了自己的搭建经验和指导。同时,本文路桑已在路科公众号发布过一篇小结性的文章:《我敢说能做好验证IP的verifier是验证顾问的不二人选

摘要:检查器是设计验证流程的关键部分。随着随机约束技术的出现,各种语言,方法和工具都支持了许多的激励生成功能。使用各种形式的检查器可以确保设计符合规范。术语 "checker" 对不同的使用者意味着不同的事物。SystemVerilog 2009标准加入 "checker" 作为关键字,我们希望将它用于使用断言的时间检查。在本文中,我们分享了面向典型协议设计 Checker IP(检查IP,CIP)的经验

 

I.简介

电子系统设计领域在复杂性方面可以说是突飞猛进。同时,新产品及其衍生产品的上市时间也在不断缩短。由于IP(Intellectual Properties,直译为知识产权,在IC中一般是指用于ASIC或FPGA中的预先设计好的电路功能模块)的存在,设计方面和验证方面都表现出了这一趋势。在验证方面,这些IP通常被称为VIP(Verification Intellectual Properties,验证IP )。这是一个在业界宽泛使用的术语,表示基于模拟,模拟驱动和记分板的组件。在典型的基于SystemVerilog UVM的环境中,这些IP通常称为UVC(Universal Verification Components,通用验证组件)。

VIP通常有两个重要部分:1.由序列测试序列库配置等组成;2.主要负责执行检查(例如记分板,检查器)和跟踪覆盖率(功能和断言)。

在这两个部分中,上述第一个部分在基于验证的模拟中是非常必要的。但是,诸如形式化验证(Formal Verification,FV)之类的相邻技术仅需要检查器/属性和一组覆盖点。借助被检查的内容,FV工具倾向于探索整个状态空间,并尝试对给定DUT的属性进行证明或伪造。在 "探索" 的过程中。只能被设计人员给出的约束模型所限制。尽管FV并没有采用基于激励的传统方法,而是严格意义上的数学 "探索"。但是在某种程度上,很多繁琐的激励生成都是由封装中的形式化引擎完成的。我们使用术语 " Checker IP ",来区别于传统的VIP。严格来说,CIP是标准VIP的子集。在本文中,我们介绍了构建CIP——checker IP的经验。这一IP用于关注设计的 "属性" 检查,覆盖和约束。如果在设计这些IP时考虑的足够充分,那么这些CIP可在模拟和形式验证中实现复用。

II. CHECKER IP(检查IP,CIP)

Checker IP(CIP,检查IP)是一种以SystemVerilog声明,覆盖和假设的形式捕获给定协议属性的IP[1]。创建CIP的动机是重点从预期行为,意外协议违规,预期场景等方面关注  DUT的预期输出。在CIP中,我们将 " 能否工作 "," 工作是否完成 " 的查询与查询的执行方式(模拟或形式化)分开。

对于标准协议,例如ARM的AMBA协议[2],通常从协议本身定义了一些规范性检查[3]。考虑到围绕标准总线构建的系统数量,对业界而言利用标准CIP来检查定义良好的规范规则列表是非常有必要的。但是,一系列的属性和其周围的断言并不是CIP的可复用部分——它们只是属性的集合。有一些技术和方针将这样的属性列表转换为IP(CIP)。

III. 构建检查IP

对于任何IP而言,最基本也是最重要的要求是可以将其设置为应用到不同协议/系统的配置。以具有主机和从机通信的AMBA AXI3协议为例,图1显示了AXI总线上主从接口的示意图[2]。

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                     图1 主从结构的AXI总线的简单示意图[2]

在上图中,仅显示了主机和从机。在完整的AXI子系统中,可能会有其他组件。例如互连、仲裁器、解码器等。由于该协议已经完全公开,因此可以提取到AXI3的规范检查列表(ARM在[3]中发布了一个版本)。

在将检查列表 " 翻译 " 到执行用检查器时,仅将英语规范翻译为一组SystemVerilog断言可能是一个不错的开始。但是,在本例中,如此简单的属性列表很难在模拟设置中作为CIP使用。这是因为主机接口和从机接口中可能存在不同的端口。另外,有一些可选功能会添加其他端口(例如,保护、锁定、授权等)。这些端口可能仅在主接口中存在,而在从接口中不存在,反之亦然。

通常,给定属性可以是某个接口上的断言,而同一接口上的另一个断言则被认定为是假设(例如,主机的awvalid是断言类型,因此对主机接口进行断言或检查;而同一个awvalid在从机接口则是输入,在这里awvalid又是一个假设类型)。从语言角度来看,SystemVerilog具有:

  • 断言(用于检查);

  • 假设(约束);

  • 覆盖(针对所需行为);

       典型的CIP会在每个接口上使用上述的三种类型。例如,主机接口应分别包含断言、假设和覆盖的属性。

      考虑AXI3协议,该规范(表4-3中的4.4节)提到了ARBURST和AWBURST的合法值,如图2所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                                   图2 ARM AXI3协议规范摘录

可以将此规范转换成如图3所示的可执行属性:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                       图3 符合AWBURST要求的CIP实例代码

典型的AXI系统在 " 写 " 通道中利用如下所示的信号:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

      

                                                                                       图4 AXI 写通道示意图

AWBURST是主机的输出,也是从机的输入。如图3中所编写的属性适用于主机和从机。但是,从主机的角度来看,这一属性应为checker;从从机的角度来看,应为assumptionconstraint。因此,AXI3的CIP必须通过声明一次通用属性的方式进行构建。

作为检查器的属性

一个 master_checker(主机检查器)文件应将如图5所示的属性用于断言:

       你知道用于AMBA协议的“Checker IP”是如何构建的吗图5 AXI3主机检查器

在上面的断言中,操作块用于通过UVM的报告组件标记错误。使用UVM搭建测试平台是非常高效的,因此强烈建议集成UVM。这种错误报告日志文件更易于阅读,分析/排除故障。使用UVM也可以增强对错误报告及其相关操作的可控性。

作为约束的属性

当被测试模块接收到相应的信号时,描述一系列信号行为的属性应当被配置为约束。由于AWBURST是AXI3从机模型的输入,因此应将此属性用于假设或约束。AXI3从机的CIP示例代码如图6所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                                    图6 AXI3 从机约束

为了更好的展示复杂度,下表总结了AXI3 CIP的检查程序和约束的大致数量。

Category

Number of entities

(asserts/assumes)

AXI3 Master CHeckers

102

AXI3 Master Constraints

20

AXI3 Slave Checkers

43

AXI3 Slave Constraints

67

 

IV. 构建检查IP的指导

System Verilog提供了功能强大和丰富的构造集,以简单明了的方式为设计的时间行为进行建模[1]。然而,并非所有构造都与形式验证兼容。虽然没有根据LRM形式化的SVA标准子集,但是根据我们对各种EDA工具的长期经验,已经得到了一个通用的最小子集。我们在本文中分享了我们在该领域的一些经验教训。

使用 " checker "构造

CIP的理想结构是相对较新的 " checker……endchecker " 结构。这一结论在DVCon2010的论文中进行了展示[4]。根据我们的经验,这一结构在各种工具中都没有得到很好的支持。其语言本身在参数等方面也存在某些限制[1]。但是,checker  " 结构在实例化方面(过程、内联、并发等)提供了更大的灵活性。因此,对于较小的基于断言的实体(例如OVL-type[5]),我们认为 " checker " 非常有用。不过,将它们用于复杂的CIP会付出更大的代价。

使用 " module " 作为容器

" module " 是Verilog和SystemVerilog中最常见的容器之一。在SystemVerilog中,使用 " module " 作为容器或封装单元进行断言是很常见的。为了使断言与设计分离,工程师经常使用将设计模块和检查器模块通过 " bind " 连接。

《System Verilog Assertions handbook》的第4.7章节中[6],存在一个设计模块 " dut " 和一个检查器模块 " vf "。图7中展示了如何使用 " bind " 构造连接两个模块。

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

      

                                                                          图7 使用SystemVerilog 中的 " bind "

模拟器中详细说明了SystemVerilog中的 " bind " ,并在它所绑定的模块内被例化为了绑定实体。为了演示这一概念,在使用工具进行详细描述后,得到了图7中的等效示例:对 " dut " 中的 " vf " 模块进行了实例化。如图8所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                             图8 SystemVerilog " bind " 的内部机制

 

使用 " interface " 作为容器

鉴于业界广泛的使用SystemVerilog和基于UVM的测试平台,许多团队使用SystemVerilog中的 " interface "作为测试平台和DUT的主要通信方式。尽管在SystemVerilog LRM[1]中," interface "有许多和" module "一样的功能,但是" interface "无法实例化一个" module "。下面借助图9和图10对此进行说明。

你知道用于AMBA协议的“Checker IP”是如何构建的吗

             

                                                                            图9 " module " 可以实例化 " interface "

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                               图10 " interface "不能实例化" module "

 

这为什么很重要?以基于UVM的VIP进行验证的AXI子系统为例进行说明。AXI的端口使用SystemVerilog接口进行建模,该接口可以根据需要来多次实例化。SystemVerilog接口是基于 UVM类的系统与基于SystemVerilog模块的设计之间的主要通信手段。现在,假设一个场景:为了增强验证的质量,将CIP连接到AXI接口。如果CIP容器是一个 " module ",则工具中会给出一个编译错误,就如同图10中所显示的问题。

这个问题的解决方法是使用 " interface "作为CIP的容器。SystemVerilog允许一个 " interface " 例化另一个 " interface "因此可以将一个使用" interface "建模的良好CIP连接到一个DUT的内部 " module "或基于使用" interface "的仿真设置的VIP。如图11所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

      

                                                                       图11 " interface " 可以例化" interface "

使用文本宏保护特定的仿真结构

SystemVerilog是一种具有许多功能的语言。但是在使用时,其所有的功能不一定被完全支持。在CIP的文中,希望能保证CIP在模拟和形式验证流程中均可用。在专用于形式验证的IP中,还是用了一些高级不确定性功能。做为编码指南,建议根据需要使用适当的文本宏覆盖来自模拟器和FV工具的部分代码

一个常见的示例是使用带有断言的UVM消息系统的操作块。鉴于UVM很大程度上是基于类的不可综合代码,而且FV工具通常不喜欢这种代码。因此文本宏(VM_CIP_SIM)用于保护操作块代码免受FV工具的利用,并且仅在模拟中使用。如图12所示:

       你知道用于AMBA协议的“Checker IP”是如何构建的吗

图12 在操作块中使用文本宏

在值改变时添加适当的延时

SystemVerilog提供了丰富的功能集用于对时间行为的建模。某些值访问功能(例如$past,$sampled等)是指向来自先前时钟周期的信号值。类似地,一些值变化函数(例如$rose,$fell等)依赖于相对于时钟而言的,被监视信号的先前的值。尽管这是SystemVerilog语言中很方便的功能,但是在编码时应格外注意避免在模拟和形式验证中出现"false failures"。以图13中的断言为例(来自网络论坛[7])。

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                 图13 当在断言中使用 " $past "时,应当小心

上面代码的问题是:"$past在DLY之前的时钟中返回什么值?"在模拟中,答案是X。这可能会花费一些调试时间。但是,在FV工具中,这可能会导致错误。原因在这一示例中,工具可以在" DLY "之前的时钟中假设" req "信号为任何值(DLY是一个参数)。

推荐的解决方案是向这种属性的检查添加适当时钟周期的延时。图14展示了解决上述问题的代码。

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                  图14 将 " ## delay " 添加到属性的开来避免未初始化的值

对每个断言进行单元测试

如何验证断言是设计的" 检查器 ",还是 " 验证器 " 的核心?考虑到一个全面的CIP由复杂的代码组成的,因此其本身就需要彻底的验证。我们在Go2UVM框架[8]中开发了一系列单元来解决这个问题。简而言之,这涉及为每个断言使用简单的UVM测试来创建PASS和FAIL跟踪。这些单元测试足够 " 聪明 "来进行自我检测。我们使用了来自开源SVUnit架构[9]的UVM报告模拟程序来围绕断言对每个单元进行测试

考虑AHB协议对htrans信号的要求,如图15所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                                 图15 AHB协议对htrans信号的要求

 

SVA中此要求代表的属性如图16所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                                   图16 htrans信号的检查

为了确保上述断言确实 " 验证 " 了仲裁器,需要测试这些代码。作为对比,考虑了通过和失败的情况。图17和图18记录了一些失败的情况。

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

      

                                                                                        图17 AHB ntrans 无效转换-1

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

      

                                                                                       图18 AHB ntrans 无效转换-2

一旦确定了所需的方案,问题就是我们可以在UVM框架中对其进行编码吗?一个成熟的UVM平台进行此测试将是overkill。

我们已经在UVM上使用了一个简单的测试层,名为Go2UVM[8]测试,如图19所示:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

      

                                                                                        图19 Go2UVM 测试基类

使用Go2UVM软件包可以回避异议、各种组件等问题。可以使用很少的代码编写质量跟踪。图20显示了Go2UVM框架中上述声明的PASS追踪。

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                             图20 AHB ntrans Go2UVM的测试(PASS追踪)

FAIL追踪或断言应当触发却没有的情况对于验证更为重要。在Go2UVM中对它们进行编码非常简单。但是难点在于将这些单元的测试自动化并将它们分类为PASS或FAIL(在测试中,预期失败的测试应当以UVM_ERROR失败)。在单元测试中,需要根据用户的目标实现自动声明 " PASS/FAIL " 。这个挑战不仅仅是典型的DUT PASS/FAIL声明(它可能基于日志文件中存在的UVM_ERROR)。

在单元测试中,通过定义分类好的预期UVM_ERROR实现 " 错误场景 " 的注入不可行的。我们使用了Nei Johnson开发的uvm_report_mock功能作为SVunit的一部分[9]。现在,这一基类也是最新的Go2UVM软件包的一部分。参见图21中的htrans断言跟踪。       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                                        图21 AHB htrans 的无效传输(否定测试)

在第六个时钟周期,我们预计断言会触发。如果我们不做修改就运行,它将报告如图22所示的UVM_ERROR:

       

你知道用于AMBA协议的“Checker IP”是如何构建的吗

                                                        图22 由于失败追踪而导致的示例UVM_ERROR(否定测试)

作为开源SVUnit的一部分,可以使用一个非常有用的软件包uvm_mock_pkg。这个程序包在比较高的级别提供了三个功能:

  • 捕获来自仿真的所有UVM错误的回调;

  • 用于指定用户所期望的错误的API;

  • 一个用于比较预期错误和实际错误并记录不匹配项的API。

uvm_report_mock::expect_error() API在内部生成了一个 " 预计错误 " 的队列。例如,在AHB CIP单元测试中,将expect_error称为否定追踪。如图23所示。

       你知道用于AMBA协议的“Checker IP”是如何构建的吗

图23 带有expect_error调用的自检Go2UVM单元测试

有了这样一个方便的报告模型,单元测试模块就可以进行自我检测。我们坚信,良好的CIP应当配有一套质量优质的单元检测,可以在CIP发生错误修复后随时进行回归。

 

V. 总结

设计带有SystemVerilog 断言的验证在业界已经流行了十多年了。尽管可以开发快速简单的检查器并在设计中使用,但是全面的CIP  (Checker IP) 采用了良好的体系结构和一组编码标准确保了它们可以重复使用。在本文中,我们分享了将一组简单的属性转换为可复用CIP的经验和如何使用自检单元测试框架来验证CIP中的每个断言。

VI.参考文献

[1] System Verilog LRM-http://standards.ieee.org/getieee/1800/download/1800-2012.pdf;

[2] ARM AXI specification – https://www.arm.com/products/system-ip/amba-specifications;

[3] ARM releases assertion models - https://www.arm.com/about/newsroom/12266.php;

[4] Experiencing Checkers for a Cache Controller Design

http://systemverilog.us/DvCon2010/DvCon10_Checkers_paper.pdf;

[5] Accellera Open Verification Library (OVL) http://accellera.org/activities/working-groups/ovl;

[6] SystemVerilog Assertions handbook, www.systemverilog.us, www.verifnews.org/publications/book;

[7] "What are $past compared to on first clock event?" http://bit.ly/2hkb7nV;

[8]  Go2UVM open-source test layer, www.go2uvm.org.;

[9] SVUnit - http://www.agilesoc.com/open-source-projects/svunit/.

 

原文来自:DVCon2017_USA, 点击阅读原文去路科官网下载DVCon2017论文合集,还有更多资料等你来哦!

你知道用于AMBA协议的“Checker IP”是如何构建的吗

扫描上图二维码可直达课程页面,马上试听

往期精彩:

获取验证通关密语,就在本周日开班的验证V2课程

30w+还送股送房?60+IC企业2019薪资全面攀升!

UVM RAL模型:用法和应用

我们准备做第二期线下培训,依旧认真且严肃

如果你突然被裁员了,你的Plan B是什么?

[彩虹糖带你入门UVM]

理解UVM-1.2到IEEE1800.2的变化,掌握这3点就够

你知道用于AMBA协议的“Checker IP”是如何构建的吗