没有合适的资源?快使用搜索试试~ 我知道了~
首页System Verilog Assertion 简介
资源详情
资源评论
资源推荐
SystemVerilog Assertion 简介
在验证环境中,测试平台承担的三个不同的任务:
(1) 产生激励
(2) 自检机制:包括协议检验和数据检验。协议检验的目标是控制信号。数据检验
的目的是检验正在处理的数据的完整性。
(3) 衡量功能覆盖:包括协议覆盖和测试计划覆盖。协议覆盖用来衡量一个设计的
功能说明书中确定的所有功能是否都测试过。测试计划覆盖用来衡量测试平台的穷尽性。
SVA 着重处理在测试平台中被分散在不同部分中讨论的两大类:
(1) 协议检验
(2) 协议覆盖
1. SVA 定义
断言,又被称为监视器或者检验器。如果一个在模拟中被检查的属性(property)不象
我们期望的那样表现,那么这个断言失败。
Verilog 也能用来实现一些检查,但相比较而言 SVA 有如下优点:SVA 是一种描述性
语言,可以完美的描述时序相关的状况,语言本身非常精确且易于维护。SVA 提供若干个
内嵌函数来测试特定的设计情况,并且提供了一些构造来自动收集功能覆盖数据。
SVA 中定义了两种断言:并发断言和即时断言。
并发断言是基于时钟周期的,在时钟边缘根据调用的变量的采样值计算测试表达式,
可以在静态验证和动态验证中使用。
例如:a_cc:assert property(@(posedge clk) not(a && b));
即时断言是基于模拟事件的语义,测试表达式的求值与时序不相关,只可以在动态验
证中使用。
例如:always_comb
begin
a_ia:assert (a && b);
end
区别并发断言和即时断言的关键词是 property。
2. SystemVerilog 的调度
在每个 time slot,许多事件按照安排的顺序发生。这些事件的列表依照标准定义的算
法执行。依照这个算法,模拟器可以防止任何在设计和测试平台互动中的不一致。
1
图 2 SystemVerilog 事件进程安排流程表
断言的评估和执行包括以下三个阶段:
(1) 预备(Preponed)采样断言变量。
(2) 观察(Observed)对所有的属性表达式求值。
(3) 响应(Reactive)调度评估属性成功或失败的代码。
3. 建立 SVA 块
SVA 用关键词 sequence(序列)来表示设计中的逻辑事件。序列的基本语法是:
sequence name_of_sequence
<test expression>
endsequence
许多序列可以逻辑或者有序的组合起来生成更复杂的序列。SVA 提供了一个关键词
property(属性)来表示这些复杂的有序行为。属性的基本语法是:
property name_of_property
<test expression>;or
<complex sequence expressions>
endproperty
属性必须在模拟过程中被用于断言(assert)、假设(assume)或覆盖(cover)语句来发挥作用。
2
SVA 提供了关键词 assert 来检查属性。其基本语法是:
assertion_name: assert property (property_name);
SVA 提供了关键词 assume 来假设属性。其基本语法是:
assertion_name: assume property (property_name);
SVA 提供了关键词 cover 来衡量协议覆盖。其基本语法是:
cover_name: cover property (property_name);
上图表明了 SVA 语言的基本构成。布尔表达式将设计中的信号组合起来,组成序列。
然后序列逻辑或者有序的组合起来得到属性。最后通过关键词 assert,cover 和 assume 指示
属性的具体作用。
4. SVA 序列和属性
4.1 简单序列举例
首先以一个只做组合逻辑检查(检查布尔表达式)的序列为例:
sequence s1
@(posedge clk) a;
endsequence
序列 s1 检查信号 a 在每个时钟上升沿都为高电平。
图 1 序列 s1 的波形
从波形图可以看出,一个向上的箭头表示一次成功,一个向下的箭头表示一次失败。
并且并行断言使用进程安排中预备(preponed)阶段采样到的值。此例中序列开始时间和
3
结束时间相同。
接下来,介绍一个时序关系的序列:
sequence s2
@(posedge clk) a ##2 b; // ##表示时钟周期延迟
endsequence
图 2 序列 s2 的波形
序列 s2 检查的是如果 a 在任何一个给定的时钟上升沿为高电平,b 应该在两个 cycle 之
后为高电平。与上例中不同的是,序列 s2 开始时间和结束时间可能不同。
从波形图中可以看出,如果 a 为低电平,检查失败,s2 开始并结束于同一时间。如果
a 为高电平,序列开始进行时序关系的检查。时序检查的第一个失败开始于 2,结束于 4;
时序检查的第一个成功开始于 5,结束于 7。注意表示序列成功或失败的箭头都是标注在序
列结束的位置。
4.2 蕴含操作符
上一小节中序列 s2 的失败由两个原因:(1)a 为低电平;(2) a 为高电平,b 在两个 cycle
之后不为高电平。通常我们只关心第二种错误,第一种错误是一个无效的错误信息。因而
我们希望通过定义某种约束技术,在检查的起始点无效时忽略这次检查。SVA 提供了蕴含
(Implication)实现这一目的。
蕴含的左边叫做先行算子(antecedent),右边叫做后续算子 (consequent)。当先行算子成
功时,后续算子才会被计算;如果先行算子不成功,那么整个属性被默认为“空成功”。另
外要注意的是,蕴含只可用于属性定义中,不可用于序列中。
蕴含分为两类:
(1) 交叠蕴含(Overlapped implication)
4
用符号”|->”表示。如果先行算子匹配,在同一个时钟周期计算后续算子表达式。 也可
以加入固定延时”|-> ##2”,表示如果先行算子匹配,在两个时钟周期之后计算后续算子表
达式。
(2) 非交叠蕴含(Non-overlapped implication)。
用符号”|=>”表示。如果先行算子匹配,在下一个时钟周期计算后续算子表达式。
利用蕴含,序列 s2 可以改为更符合我们需要的时序检查的属性 p3:
property p3
@(posedge clk) a |-> ##2 b; // ##表示时钟周期延迟
endproperty
图 3 属性 p3 的波形
从波形图中可以看出,失败只有一个(开始于 2,结束于 4),真正的成功只有一个
(开始于 5,结束于 7),其余的成功都为空成功。
4.3 SVA 检验器的时序窗口
上面讨论的延迟的例子都是固定的正延迟。延迟也可以用时序窗口的方式定义,从而
给延迟限定一个范围。
例如:
(a&&b) |-> ##[1:3] c;
上述表达式实际上以下面三个线程展开:
(a&&b) |-> ##1 c 或
(a&&b) |-> ##2 c 或
(a&&b) |-> ##3 c
时序窗口可以用于属性以及序列。不同的是,第一个成功的线程将使整个属性成功,
5
剩余26页未读,继续阅读
kriayamatoo
- 粉丝: 15
- 资源: 69
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 2022年中国足球球迷营销价值报告.pdf
- 房地产培训 -营销总每天在干嘛.pptx
- 黄色简约实用介绍_汇报PPT模板.pptx
- 嵌入式系统原理及应用:第三章 ARM编程简介_3.pdf
- 多媒体应用系统.pptx
- 黄灰配色简约设计精美大气商务汇报PPT模板.pptx
- 用matlab绘制差分方程Z变换-反变换-zplane-residuez-tf2zp-zp2tf-tf2sos-sos2tf-幅相频谱等等.docx
- 网络营销策略-网络营销团队的建立.docx
- 电子商务示范企业申请报告.doc
- 淡雅灰低面风背景完整框架创业商业计划书PPT模板.pptx
- 计算模型与算法技术:10-Iterative Improvement.ppt
- 计算模型与算法技术:9-Greedy Technique.ppt
- 计算模型与算法技术:6-Transform-and-Conquer.ppt
- 云服务安全风险分析研究.pdf
- 软件工程笔记(完整版).doc
- 电子商务网项目实例规划书.doc
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论7