赞
踩
测试平台的自检机制,通常关注两个方面:
功能覆盖用于衡量验证的完整性,衡量指标包括两项指定的信息:
SVA(SystemVerilog Assertion)着重处理两大类问题:
断言是设计的属性的表示:
示例:相互断言条件检查的Verilog 实现
// 若a和b同时为高电平,则报错(断言失败)
`ifdef ma
if(a&b)
$display("Error: Mutually asserted check failed.\n")
`endif
// 只有当需要时才被纳入设计环境中。可以通过允许 Verilog 条件编译指令 “ `ifdef ” 来实现
使用 Verilog 检查的不足:
SVA:一种描述性语言,可以很好的描述时序相关的状况;精确且易于维护;SVA提供了若干内嵌函数用来测试特定的设计情况,并且提供了一些构造来自动收集功能覆盖数据;若断言失败SVA会自动显示错误信息。
Systemverilog 语言被定义成一种基于事件的执行模式。
断言的评估和执行包括三个阶段:
SystemVerilog 语言中定义了两种断言:并发断言 和 即时断言
示例:
// 在时钟沿,a和b 不能同时为高电平
a_cc: assertproperty(@ posedge clk) not (a&b));
属性的每一个时钟的上升沿都被检验,不论信号a 和 信号b 是否有值的变换
always_comb
begin
a_ia: assert ( a && b ) ;
end
/// 即时断言 a_ia 被写成一个过程块的一部分,遵循和信号a、b 相同的事件调度。
// 当信号a 和 信号b 发生变化时,always 块被执行。
对于即时断言,当断言的信号值发生变化时,always块(断言语句)被执行
区别即时断言 和 并发断言 的关键词:** " property" **
任何设计模型中,功能总是由多个逻辑事件的组合来表示的。
SVA 用关键词** “ sequence”** 来表示这些事件。
==序列(sequence)==的基本语法:
sequence name_of_sequence;
<test expression>;
endsequence
许多序列可以逻辑或有序地组合起来成更复杂的序列。SVA 提供了关键 “property” 来表示这些复杂的有序行为。
property 基本语法:
property name_of_property;
<test expression>; or
<complex seqeunce expressions>;
endproperty
属性:是在模拟过程中被验证的单元。它必须在模拟中被断言来发挥。SVA提供了关键词**“assert”** 来检查属性。
==断言(assert)==基本语法:
assertion_name: assert property ( property_name );
建立 SVA 检验器的步骤:
步骤1: 建立布尔表达式
↓
步骤2:建立序列表达式
↓
步骤3:建立属性
↓
步骤4:断言属性
// 检查信号 a 在每个时钟上升沿都是高电平
sequence s1;
@(posedge clk) a;
endsequence
序列s1 使用的是信号的逻辑值。
SVA 也内嵌了边缘表达式,方便用户检测信号值从一个时钟周期到另一个时钟周期的跳变。 —— 使得用户能够检查边沿敏感的信号。
三种有用的内嵌函数:
示例:
// 序列s2 检查信号 " a " 在每个时钟上升沿跳变为1
sequence s2;
@(posedge clk) $rose( a );
endsequence
示例:
// 序列s3 检查每一个时钟上升沿,信号“a" 或 信号 “ b" 是高电平
sequence s3;
@(posedge clk) a || b;
endsequence
在序列定义中定义形参,相同的序列能够被重用到设计中具有相似行为的信号上。
示例:
// 定义
sequence s3_lib ( a, b );
a || b;
endsequence
// 通用的序列 s3_lib 能重用在任何两个信号上
sequence s3_lib_inst1;
s3_lib ( req1, req2 );
endsequence
一些在设计中常见的通用属性都可以被开发成一个库便于重用,如 one-hot 状态机检查,等效性检查等。
时序检查 :检查的信号需要几个时钟周期才能完成事件
SVA 中,时钟周期延迟 用 ” ## “ 表示。如 ##3 表示3个时钟周期
示例:
// 序列s4:检查信号 " a “ 在 一个给定的时钟上升沿为高电平后,信号"b" 在两个时钟周期后为高电平
// 注意:序列以 信号"a" 在时钟上升沿为高电平开始
sequence s4;
@(posedge clk) a ##2 b;
endsequence
注意:断言成功的序列总是标注在序列开始的位置
Copyright © 2003-2013 www.wpsshop.cn 版权所有,并保留所有权利。