基于断言的验证简介 – 第 1 部分

这篇具有很好参考价值的文章主要介绍了基于断言的验证简介 – 第 1 部分。希望对大家有所帮助。如果存在错误或未考虑完全的地方,请大家不吝赐教,您也可以点击"举报违法"按钮提交疑问。

基于断言的验证简介 – 第 1 部分

基于断言的验证(ABV)是一种与传统方法相比可以大大减少验证过程的技术.

ABV主要用于 ASIC 领域,但由于FPGA 设备的复杂性不断增加,事实证明它在 FPGA 验证流程中同样至关重要。

然而,在我们开始庆祝芯片项目验证周期大幅缩短的可能性之前,我们需要了解断言以及如何将它们有效地集成到验证方法中。

为了便于技术消化,断言的介绍将分为两部分。第一部分将解释什么是断言,讨论语言并发展基本术语和思想。在第二部分中,我们将深入挖掘并介绍蕴涵的使用和“空洞真理”的概念以及断言和覆盖。

什么是断言?

断言最简单的定义是“设备行为的抽象表示,在规范、验证和实现中很有用……”

稍后我们会看到这个定义可以扩展为更准确的描述,但现在就用这个定义了。

有两种语言可用于表达断言的实际应用,即属性规范语言(PSL)和SystemVerilog断言子集(SVA) 。

PSL 可用于 VHDL、Verilog、 SystemVerilog和SystemC ,并且是 VHDL-2008 的子集。

SVA 是SystemVerilog语言的断言相关子集,基于Superlog和OpenVera捐赠。它的断言和属性功能也借鉴了 PSL。

两种语言都是 IEEE 标准。

哪种语言?

VHDL 设计人员可以同时使用 SVA 和 PSL,但通常选择 PSL,因为它可以直接放入 VHDL 代码中并有助于设计文档,而 SVA 则不能。此外,PSL 现在是 VHDL 标准 (2008) 的一部分,因此这意味着只需要使用一种语言。

Verilog 设计人员可以同时使用 PSL 和 SVA,但通常使用 SVA,因为当直接放入 Verilog 代码中时,它比 PSL 具有更多可用功能。此外, SystemVerilog和 Verilog 现在合并为一个标准 - SystemVerilog 。

好消息是 PSL 和 SVA 属性看起来几乎相同。

为什么使用断言?

断言已经成为 ASIC 设计中一种既定且流行的验证方法,因此 FPGA设计可以从这一领域学习。重要的是,它们受 IEEE 标准(PSL、 SystemVerilog和 VHDL)管辖。

面向对象编程中处理类、对象、继承等要容易得多。它们基于您作为设计师所熟悉的设计规范,因此更容易实施。

断言在模拟中创建了额外的安全层,因为它们是对原始规范的引用,并且在进行综合和实现迭代时非常有用。

断言本质上以它们的编写方式创建“实时文档”,这使得设计的管理变得更加容易。它们非常容易阅读和解释,这使得与设计团队的共享变得更容易管理。

在哪里放置断言?

所有工具都允许您将断言放置在单独的单元或文件中,并将它们“绑定”到常规 RTL 代码。验证工程师喜欢这个想法,因为它允许文件独立性,而 HDL 设计人员通常更喜欢将断言直接放入代码中以减少所需的文件量。

大多数模拟器允许您直接在 RTL 代码中放置断言。对于 PSL,这表示为注释。对于SystemVerilog ,断言可以直接放入代码中。

例如: – psl属性 p1 是… 或 // psl属性 p2 是…

VHDL-2008 允许将 PSL 断言直接放入代码中(无需注释)。

将断言放入代码中时需要小心,因为综合工具通常不支持某些断言,因此需要使用综合编译指示来管理它们。

发展基本术语和想法

术语“基于断言的验证”(ABV)通常用于描述整个验证过程,但它不仅仅涉及断言。

该流程由序列、属性、断言和覆盖组成。

ABV的基本思想是“属性”。属性是对设计的特定行为的正式描述,例如“窗户破裂触发警报”或“安全在 30 秒内响应警报”。

验证工具可以通过多种方式使用属性,通过“断言”属性来验证不会发生不好的事情,例如“断言损坏的窗户总是会触发警报”。

或者,使用“覆盖”来验证是否发生了好事,例如“在 30 秒内覆盖了对触发警报的响应”。

深入挖掘这些属性,如果你看一下典型的数字设计规范,它已经充满了用简单的英语表达的设计属性。作为设计人员,您可以将这些属性重写到 HDL 中,同时考虑到正确的硬件实现。

因此,属性、断言和覆盖代表了设计的纯粹行为(期望的或不期望的)。正如我们所说,它们可以作为非常有效的设计文档,并作为设计验证期间的参考。它们还被各种功能和形式验证工具所接受。

我们现在需要了解如何定义属性以及它如何使用“时间逻辑”的原理。

时态逻辑可以被认为是添加了时间维度的布尔逻辑。

如果我们使用“离散时间”,则属性表示设计的“状态序列”。请注意,所有流行的基于属性的设计 (PBD)/ABV 解决方案都对设计中对象的采样值进行操作。

为了及时表达这种关系,属性使用“时间”或“模态”运算符,例如下一个、最后、全局、直到(next, finally, globally, until)等。

接下来我们需要了解如何构建属性。

我们都熟悉的布尔类型表达式是属性组成的一部分,但却是最简单的部分。我们还需要了解“序列” 。

“序列”通常被认为是代表离散时间点上的一系列设计状态的属性的基本时间构建块。

典型的序列代表设计中的简单执行路径。

要从简单的序列创建真实的属性,您可以:

“融合”序列,其中一个序列在另一个序列开始的同一时刻结束。
“连接”序列,其中一个序列结束,另一个序列在下一个时间点开始
说一个序列是另一个序列的“蕴含”
“与”或“或”序列
检查一个序列是否包含在另一个序列中
检查序列是否重复给定次数(连续或不连续)

一旦设计属性正式化,所有工具都可以在两个指令之一中使用这些属性:

基于断言的验证简介 – 第 1 部分,芯片技术,fpga开发

图-1

断言——当属性不成立时会发出警报。

覆盖——确认该属性已成功测试。

一些工具(主要是形式验证,但也有一些模拟器)允许更多指令,例如控制设计刺激或限制环境条件(假设、限制、公平等)。

建立实用的断言

现在我们已经了解了属性和序列的基本元素,让我们看看如何构建实际的断言。

正如我们所提到的,最基本的属性是具有严格线性时间流的“序列”。

模拟需要线性时间流,因此属性的时间来回跳跃是不可能的,因为这会使模拟变得不可能。

序列的每个节点代表您的设计的一种状态:

某些信号所需的值
必须满足的条件

为了完成序列,您必须指定如何将这些节点连接在一起。那么,让我们看看一些“序列”属性事实。

最简单的序列是布尔表达式,但更常见的是,您会将多个表达式粘合在一起以形成“随时间扩展”的复杂序列。

要使元素在同一时钟上粘在一起,请在 PSL 中使用‘fusion’ (😃 或在 SVA 中使用“零时钟延迟”(##0) ‘zero clock delay’ (##0)。

基于断言的验证简介 – 第 1 部分,芯片技术,fpga开发

要在元素之间引入一个周期中断,请在 PSL 中使用“串联”(😉 ‘concatenation’ (;)或在 SVA 中使用“一个周期延迟”(##1) ‘one cycle delay’ (##1)。
基于断言的验证简介 – 第 1 部分,芯片技术,fpga开发

您可以使用 SVA 中的一系列值 (##[ m:n ]) 指定更长的延迟。

PSL 使用“连续重复运算符”(<序列>[ *m 到 n])([*m to n])来指定“值范围”延迟。如果没有要重复的序列,则假定“True”是重复的参数。

现在我们已经提到了重复,让我们更正式地看看这个。

如果相同的条件应保持超过一个周期,那么我们可以使用“连续重复运算符”,而不是使用串联或一个周期延迟来重复条件。

该运算符在 PSL 和 SVA 中看起来相同:序列 [* Number_or_Range ] Sequence [* Number_or_Range].。

带有数字的简单形式表示序列应该重复(保持)给定的次数: A[ *7]。

范围版本表示序列应在自然范围内保持任意数量的循环(要指定无限上限,请在 PSL 中使用“inf”或在 SVA 中使用“ ”): B [ ∗ 1 t o i n f ] B [ ∗ 1 : ”): B[*1 to inf] B[*1: ):B[1toinf]B[1:]

让我们用一个例子来说明:
基于断言的验证简介 – 第 1 部分,芯片技术,fpga开发

图3

在这里,我们看到了一个重复的例子,以及没有重复的等效序列,并显示了 PSL 和 SVA 的相同序列。

时钟序列/复位和属性

所有属性语言都使用离散时间,这意味着必须指定时钟或采样方法。

如果未指定时钟,则应用最快的可用工具默认值,在模拟器的情况下,这可能是周期等于模拟分辨率的时钟。

如果大多数属性都使用一种时钟方法,则您可以指定“默认时钟”‘default clock’。

要指定时钟事件,请在 PSL 中序列的末尾或 SVA 中的开头使用“@<时钟条件>”。

对于时钟条件,请使用本机 HDL 中首选的时钟检测器,例如VHDL 中的“ rising_edge ”函数或Verilog 中的“ negedge ”。

我们还需要能够处理重置,因为有时您可能正在进行属性评估,并且发生重置,这会导致断言失败或其他不需要的情况。

幸运的是,PSL和SVA都提供了放弃属性评估的机制,而不会产生不利影响。

PSL允许在属性末尾添加“ async_abort ”或“ sync_abort ”运算符和重置条件。

always (({(A);(B)}) async_abort C=’1′) @rising_edge(CLK);

在属性开头添加“disable iff (条件)”短语。

@(posedge CLK) disable iff © A ##1 B;

总结一下时钟和复位:

属性中没有默认重置,但您可以拥有默认时钟(采样事件)。

在 SVA 中将重置和时钟应用于属性的文本顺序是 PSL 中顺序的镜像。
基于断言的验证简介 – 第 1 部分,芯片技术,fpga开发

图4

综上所述

我们引入了断言,并发现 PSL 和 SVA 属性相似并且类似于设计要求。

我们开发了断言的基本术语和思想,并讨论了序列、属性、断言和覆盖以及它们如何形成设计属性。我们还学习了如何定义属性以及它如何遵循时序逻辑原则。最后,我们开始构建一些实际的断言来理解我们所介绍和讨论的内容。

如果您喜欢这个介绍,您可以期待第二部分,它将介绍蕴含在断言中的使用及其在断言中的重要性以及在模拟中的使用。文章来源地址https://www.toymoban.com/news/detail-785309.html

到了这里,关于基于断言的验证简介 – 第 1 部分的文章就介绍完了。如果您还想了解更多内容,请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章,希望大家以后多多支持TOY模板网!

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处: 如若内容造成侵权/违法违规/事实不符,请点击违法举报进行投诉反馈,一经查实,立即删除!

领支付宝红包 赞助服务器费用

相关文章

  • 基于QT做上位机开发,实现FPGA通过cyusb3014芯片完成数据的收发

    #任务要求: 要求用qt编写上位机程序,实现FPGA通过cyusb3014芯片完成数据的收发。下面是采用通过cypress并安装usb官方驱动的环境搭建,后续继续更新程序的编写。 一、安装nodejs ①下载地址:https://nodejs.org/en/ ①.1: 安装时,除了选择安装路径根据需要选择外,其他都可以默认

    2024年02月06日
    浏览(54)
  • FPGA基于SFP光口实现10G万兆网UDP通信 10G Ethernet Subsystem替代网络PHY芯片 提供工程源码和技术支持

    目前网上的fpga实现udp基本生态如下: 1:verilog编写的udp收发器,但不带ping功能,这样的代码功能正常也能用,但不带ping功能基本就是废物,在实际项目中不会用这样的代码,试想,多机互联,出现了问题,你的网卡都不带ping功能,连基本的问题排查机制都不具备,这样的代

    2024年02月01日
    浏览(48)
  • 基于FPGA的图像sobel边缘提取算法开发,包括tb测试文件以及matlab验证代码

    目录 1.算法运行效果图预览 2.算法运行软件版本 3.部分核心程序 4.算法理论概述 5.算法完整程序工程 vivado2019.2 matlab2022a         图像边缘检测大幅度地减少了数据量,并且剔除了可以认为不相关的信息,保留了图像重要的结构属性。有许多方法用于边缘检测,它们的绝大部

    2024年02月10日
    浏览(43)
  • Xilinx GTH 简介 ,CoaXpress FPGA PHY 部分

    GTH 是Xilinx UltraScale系列FPGA上高速收发器的一种类型,本质上和其它名称如GTP, GTX等只是器件类型不同、速率有差异;GTH 最低速率在500Mbps,最高在16Gbps CoaXpress Host/Device IP 均需要用到厂商的GT收发器模块,因此这里写一篇笔记作为开发记录 physical coding sublayer (PCS) 是Xilinx 高速收

    2024年02月08日
    浏览(38)
  • 基于 ARM+FPGA+AD平台的多类型同步信号采集仪开发及试验验证(一)

    对工程结构的服役状况进行实时的监测和诊断,及时地发现结构的损伤,评估其安 全性能,预判结构的性能变化趋势与服役期限并提出改进举措,对提高工程结构的使用 效率,保障人民生命财产安全具有极其重要的意义,已经成为工程结构越来越迫切的技 术需求 [2] 。结构

    2024年02月07日
    浏览(52)
  • USB3.0芯片FT601Q简介及FPGA实现

      FT601Q 是 FTDI 推出的一款超高速 USB3.0 芯片,提供高达 5Gbps 的带宽。该芯片不需要额外的固件开发,共有 4 个写通道和 4 个读通道,每个通道的缓冲大小均为 4KB。FT601Q 具有多种工作模式,本文介绍并实现相对简单的同步 FIFO 模式——245 mode。   FT601 工作模式在上电时检

    2024年02月05日
    浏览(44)
  • 基于 ARM+FPGA+AD平台的多类型同步信号采集仪开发及试验验证(二)板卡总体设计

    2.2 板卡总体设计 本章开发了一款基于 AD7193+RJ45 的多类型传感信号同步调理板卡,如图 2.4 所 示,负责将传感器传来的模拟电信号转化为数字信号,以供数据采集系统采集,实现了 单通道自由切换传感信号类型与同步采集多类型传感信号的功能(包含桥式电路信号、 IEPE 传感

    2024年02月06日
    浏览(56)
  • FPGA基于SFP光口实现千兆网UDP通信 1G/2.5G Ethernet PCS/PMA or SGMII替代网络PHY芯片 提供工程源码和技术支持

    目前网上的fpga实现udp基本生态如下: 1:verilog编写的udp收发器,但不带ping功能,这样的代码功能正常也能用,但不带ping功能基本就是废物,在实际项目中不会用这样的代码,试想,多机互联,出现了问题,你的网卡都不带ping功能,连基本的问题排查机制都不具备,这样的代

    2024年02月08日
    浏览(65)
  • FPGA基于SFP光口实现1G千兆网UDP通信 1G/2.5G Ethernet PCS/PMA or SGMII替代网络PHY芯片 提供工程源码和技术支持

    目前网上的fpga实现udp基本生态如下: 1:verilog编写的udp收发器,但不带ping功能,这样的代码功能正常也能用,但不带ping功能基本就是废物,在实际项目中不会用这样的代码,试想,多机互联,出现了问题,你的网卡都不带ping功能,连基本的问题排查机制都不具备,这样的代

    2024年02月08日
    浏览(47)
  • 芯片验证板卡设计原理图:446-基于VU440T的多核处理器多输入芯片验证板卡

    一、板卡概述         基于XCVU440-FLGA2892的多核处理器多输入芯片验证板卡为实现网络交换芯片的验证,包括四个FMC接口、DDR、GPIO等,北京太速科技芯片验证板卡用于完成甲方的芯片验证任务,多任务功能验证。 Figure 1.1 验证板卡框图 二、技术指标   1)FPGA 外接4 路FMC-HPC;

    2024年02月11日
    浏览(47)

觉得文章有用就打赏一下文章作者

支付宝扫一扫打赏

博客赞助

微信扫一扫打赏

请作者喝杯咖啡吧~博客赞助

支付宝扫一扫领取红包,优惠每天领

二维码1

领取红包

二维码2

领红包