当前位置:首页 >> 信息与通信 >>

systemverilog assertion


芯片设计:verilog 断言(SVA)语法
(2014-01-23 13:51:36)

转 载



作者:白栎旸 断言 assertion 被放在 verilog 设计中,方便在仿真时查看异常情况。当异常出现时,断言会 报警。一般在数字电路设计中都要加入断言,断言占整个设计的比例应不少于 30%。以下

是断 言的语法: 1. SVA 的插入位置:在一个.v 文件中: module ABC (); rtl 代码 SVA 断言 endmodule 注意:不要将 SVA 写在 enmodule 外面。 2. 断言编写的一般格式是: 【例】 断言名称 1:assert property(事件 1) $display("........",$time); //有分号 else $display("........",$time); //有分号

//没有分号

断言名称 2:assert property(事件 2) $display("........",$time); else $display("........",$time); 断言的目的是:断定“事件 1”和“事件 2”会发生,如果发生了,就记录为 pass,如果没发生, 就记录为 fail。注意:上例中没有 if,只有 else,断言本身就充当 if 的作用。 上例中,事件 1 和事件 2 可以用两种方式来写: (1) 序列块: sequence name; 。。。。。。。。。; endsequence (2) 属性块: property name; 。。。。。。。。。; endsequence

从定义来讲,sequence 块用于定义一个事件(砖),而 property 块用于将事件组织起来,形 成更复杂的一个过程(楼)。sequence 块的内容不能为空,你写乱字符都行,但不能什么都没 有。sequence 也可以包含另一个 sequence, 如: sequence s1; s2(a,b); endsequence //s1 和 s2 都是 sequence 块 sequence 块和 property 块都有 name,使用 assert 调用时都是:“assert property(name);” 在 SVA 中,sequence 块一般用来定义组合逻辑断言,而 property 一般用来定义一个有时间 观念的断言,它会常常调用 sequence,一些时序操作如“|->”只能用于 property 就是这个原因。 注:以下介绍的 SVA 语法,既可以写在 sequence 中,也可以写在 property 中,语法是通用 的。 3. 带参数的 property、带参数的 sequence property 也可以带参数,参数可以是事件或信号,调用时写成:assert property (p1(a,b)) 被主 sequence 调用的从 sequence 也能带参数,例如从 sequence 名字叫 s2,主 sequence 名字 叫 s1: sequence s1; s2(a,b); endsequence 4. property 内部可以定义局部变量,像正常的程序一样。 property p1; int cnt; ..................... endproperty

【注】在介绍语法之前,先强调写断言的一般格式: 一般,断言是基于时序逻辑的,单纯进行组合逻辑的断言很少见,因为太费内存(时序逻辑 是每个时钟周期判断一次,而组合逻辑却是每个时钟周期内判断多次,内存吃不消)。 因此,写断言的一般规则是: time + event,要断定发生什么 event,首先要指定发生 event 的时间,例如 每个时钟上升沿 + 发生某事 某信号下降时 + 发生某事

5. 语法 1:信号(或事件)间的“组合逻辑”关系: (1) 常见的有:&&, ||, !, ^

(2) a 和 b 哪个成立都行,但如果都成立,就认为是 a 成立:firstmatch(a||b),与“||”基本相同, 不同点是当 a 和 b 都成立时,认为 a 成立。 (3) a ? b:c ———— a 事件成功后,触发 b,a 不成功则触发 c

6. 语法 2:在“时序逻辑”中判断独立的一根信号的行为: @ (posedge clk) A 事件; ———— 当 clk 上升沿时,如果发生 A 事件,断言将报警。 边沿触发内置函数:(假设存在一个信号 a) $rose( a );———— 信号上升 $fell( a );———— 信号下降 $stable( a );———— 信号值不变 7. 语法 3:在“时序逻辑”中判断多个事件/信号的行为关系: (1) intersect(a,b)———— 断定 a 和 b 两个事件同时产生,且同时结束。 (2) a within b ———— 断定 b 事件发生的时间段里包含 a 事件发生的时间段。 (3) a ##2 b ———— 断定 a 事件发生后 2 个单位时间内 b 事件一定会发生。 a ##[1:3] b ———— 断定 a 事件发生后 1~3 个单位时间内 b 事件一定会发生。 a ##[3:$] b ———— 断定 a 事件发生后 3 个周期时间后 b 事件一定会发生。 (4) c throughout (a ##2 b) ———— 断定在 a 事件成立到 b 事件成立的过程中,c 事件“一直” 成立。 (5) @ (posedge clk) a |-> b ———— 断定 clk 上升沿后,a 事件“开始发生”,同时,b 事件发 生。 (6) @ (posedge clk) a.end |-> b ———— 断定 clk 上升沿后,a 事件执行了一段时间“结束”后, 同时,b 事件发生。 注:"a |-> b" 在逻辑上是一个判断句式,即: if a b; else succeed;

因此,一旦 a 发生,b 必须发生,断言才成功。如果 a 没发生,走 else,同样成功。

(7) @ (posedge clk) a |=> b ———— 断定 clk 上升沿后,a 事件开始发生,下一个时钟沿后, b 事件开始发生。 (8) @ (posedge clk) a |=>##2b ———— 断定 clk 上升沿后,a 事件开始发生,下三个时钟沿后, b 事件开始发生。 (9) @ (posedge clk) $past(a,2) == 1'b1 ———— 断定 a 信号在 2 个时钟周期“以前”,其电平值 是 1。 (10) @ (posedge clk) a [*3] ———— 断定“@ (posedge clk) a”在连续 3 个时钟周期内都成立。

@ (posedge clk) a [*1:3] ———— 断定“@ (posedge clk) a”在连续 1~3 个时钟周期内都成立。 @ (posedge clk) a [->3] ———— 断定“@ (posedge clk) a”在非连续的 3 个时钟周期内都成 立。 举一个复杂点的例子: property ABC; int tmp; @(posedge clk) ($rose(a),tmp = b) |-> ##4 (c == (tmp*tmp+1)) ##3 d[*3]; endproperty 上例的一个 property 说明:当 clk 上升沿时,断言开始。首先断定信号 a 由低变高,将此时 的信号 b 的值赋给变量 tmp,4 个时钟周期后,断定信号 c 的值是 4 个周期前 b^2+1,再过 3 个 周期,断定信号 d 一定会起来,再过 3 个周期,信号 d 又起来一次。。。。。。。只有这些断 定都成功,该句断言成功。otherwise,信号 a 从一开始就没起来,则断言也成功。

8. 语法 4:多时钟域联合断言:一句断言可以表示多个时钟域的信号关系,例如: @ (posedge clk1) a |-> ##1 @ (posedge clk2) b 当 clk1 上升沿时,事件 a 发生,紧接着如果过来第二个时钟 clk2 的上升沿,则 b 发生。“##1” 在跨时钟时不表示一个时钟周期,只表示等待最近的一个跨时钟事件。所以此处不能写成##2 或其他。但是可以写成: @ (posedge clk1) a |=> @ (posedge clk2) b

9. 语法 5:总线的断言函数 总线就是好多根 bit 线,共同表示一个数。SVA 提供了多 bit 状态一起判断的函数,即总线断 言函数: (1) $onehot(BUS) ————BUS 中有且仅有 1 bit 是高,其他是低。 (2) $onehot0(BUS) ————BUS 中有不超过 1 bit 是高,也允许全 0。 (3) $isunknown(BUS) ————BUS 中存在高阻态或未知态。 (4) countones(BUS)==n ————BUS 中有且仅有 n bits 是高,其他是低。

10. 语法 6:屏蔽不定态 当信号被断言时,如果信号是未复位的不定态,不管怎么断言,都会报告:“断言失败”,为 了在不定态不报告问题,在断言时可以屏蔽。 如: @(posedge clk) (q == $past(d)),当未复位时报错,屏蔽方法是将该句改写为: @(posedge clk) disable iff (!rst_n) (q == $past(d)) //rst 是低电平有效

10. 语法 6:断言覆盖率检测: name: cover property (func_name)

11. 在 modelsim 中开启断言编译和显示功能: (1)【编译 verilog 代码时按照 system verilog 进行编译】 vlog -sv abc.v (2)【仿真命令加一个-assertdebug】 vsim -assertdebug -novopt testbench (3)【如果想看断言成功与否的分析,使用打开断言窗口的命令】 view assertions

12. 在 VCS 中加入断言编译和显示功能: 在 fsdb 文件中加一句话:$fsdbDumpSVA 在 VCS 编译参数:system "vcs $VCS_SIMULATION" 中加入一些 options: -assert enable_diag\ -assert vpiSeqBeginTime\ -assert vpiSeqFail\ -assert report=路径\ -assert finish_maxfail=100 ********************************************************************************** ************* 【经验】以下是一些编写断言的经验: 1. 断言的目的:传统的验证方法是通过加激励,观察输出。这种方法对案例的依赖严重,案例 设计不好,问题不便于暴露。而断言是伴随 RTL 代码的,不依赖测试案例,而是相对“静态”。 例如:我们要测试一个串行数据读写单元,数据线只有一根,先传四位地址,再传数据。 (1)案例验证法:写一个地址,再写一段数据,然后读取该地址,看输出的是不是刚才写的 数据。 (2)断言法:不需要专门设计地址和数据,当发起写时,在地址传输的时间里将地址存储到 一个变量里,在数据传输的时间里将数据存储到一个变量里,观察 RAM 中该地址是否存在该 数据就可以了。 断言设计相当于在电脑上把 RTL 实现的功能再实现一遍。 2. 断言中可以包含 function 和 task。而且 function 经常用于断言,因为有的处理很复杂,而断 言又是“一句式”的,无法分成好几句进行表达,所以需要 function 替断言分担工作。 3. 断言允许规定同时发生的事件,就是组合逻辑,你可以写成:a && b,也可以写成 a ##0 b, 不能写 ##0.5,不支持小数。 4. 断言是用电脑模仿 RTL 的运行过程,当 RTL 功能复杂时,你必须用到变量。断言中支持 C 语言的 int 和数组声明,但在赋值时“不能”写成:##4 var = Signal,其中 var 是断言中的变量, 和 RTL 无关,Signal 是 RTL 中的一个信号。本句是想在第 4 周期将 Signal 的值赋给 var,以便 在后面使用该值。但本句只有变量赋值,没有对 RTL 信号的任何断言,就会报错,解决方法

是:##4 (“废话”,var = Signal),一定要有断言的话我们就写“废话”,例如:data == data 等。如 果有多个变量要赋值也可以,##4 (废话,变量 1 赋值,变量 2 赋值...........) 5. 关于断言的表达风格:语法介绍的 “a |-> b”,实际上是 “if a, then b”的逻辑,当 a 不发生,b 也不会被判断,该断言自然成功。但当我们的逻辑是 if a1 { if a2 then b } 该如何用断言表达???? 或许可以写成:“a1 |-> a2 |-> b”,也可以,但常用的表达是: “a1 && a2 |-> b” 或者 “a1 ##3 a2 |-> b” 6. 关于断言的时序:时序逻辑的断言需要注意的一个问题: 例如:假设当 clk 上升沿到来时,b<=a。将上述逻辑写成断言时,如果写成“@(posedge clk) b==a”,看起来和 b<=a 一样,但实际上是错的。因为当时钟上升时,b 还没有得到 a 的值,a 还需要一段保持时间。即,断言中的信号值实际上是时钟沿到来之前的值,而不是时钟沿到来 后他们将要编程的值。所以,b<=a 逻辑的断言应该是:“@ (posedge clk) (a==a,tmp=a) |=> (b==tmp);” 针对上述几点,举一个复杂的例子: 断言 wr 的功能是检查串行地址输入是否正确,串行地址输入线是 DataIn 。$time 返回值以 0.1ns 为单位(因为我在 testbench 中的单位规定是`timescale 1ns/100ps,精度是 100ps = 0.1ns), 所以$time/10 才是 ns。 ///////////////////////////////////////////////////////////////////////////// wr: assert property(wr_p) $display("succeed:",$time/10); else $display("error: ",$time/10); ///////////////////////////////////////////////////////////////////////////// //断言可以声明一个 int 数组 arr[4], //“@(posedge clk) !vld_pulse_r[0] && !DataIn”是真实的预备条件 //“##4 (read==read, arr[0] = DataIn)”只是为了在特定时间内赋值,有用的语句是“arr[0] = DataIn”, //“read==read”是废话,为了编译通过。 //arr 赋值完毕后,进入 function 进行处理,判断实际地址 addr 跟 junc 处理过的数据是否相同。 //“addr == junc(arr[0],arr[1],arr[2],arr[3]);”就是 junction 调用。 property wr_p; int arr[4]; @(posedge clk) !vld_pulse_r[0] && !DataIn ##4 (read==read, arr[0] = DataIn)

##1 (read==read, arr[1] = DataIn) ##1 (read==read, arr[2] = DataIn) ##1 (read==read, arr[3] = DataIn) |=> addr == junc(arr[0],arr[1],arr[2],arr[3]); endproperty ////////////////////////////////////////////////////////////////////////// function [3:0] junc; input a,b,c,d; reg [3:0] a1; reg [3:0] b1; reg [3:0] c1; reg [3:0] d1; a1 = {3'b0,a}; b1 = {3'b0,b}; c1 = {3'b0,c}; d1 = {3'b0,d}; junc = a1+(b1<<1)+(c1<<2)+(d1<<3); $display(junc); endfunction //////////////////////////////////////////////////////////////////////// 7. 如果想在 SVA 中使用类似 for(){....}的功能,别忘了语法中介绍的[*3],这是在断言中实现 for 的唯一方式。 ##4 (废话, cnt = 0, arr[cnt] = DataIn, cnt++) //初始化一下, ##1 (read==read, arr[cnt] = DataIn, cnt++)[*3] //循环 3 次 8. 每句断言都是一个小程序:如上例,在##4 时间点上,(废话, cnt = 0, arr[cnt] = DataIn, cnt++) 就是一个小程序,信号断言必须是第一句,其他运算按照顺序进行。

9. 断言的变量除了可用 C 语言中的 int,float 外,还可以是 reg [n:0]等数字电路类型。

10. 注意: 像这种写法: property ept_p; @(posedge rd_clk) ((rd_num == 0) |-> rd_ept) && (rd_ept |-> (rd_num == 0)); endproperty 是错误的,写了|->,就不能再用 && 等事件组合逻辑了。

解决方法是使用 2 个断言,没更好的方法。


相关文章:
systemverilog assertion
systemverilog assertion_信息与通信_工程科技_专业资料。芯片设计:verilog 断言(SVA)语法 (2014-01-23 13:51:36) 转载 ▼ 作者:白栎旸 断言 assertion 被放在...
systemverilog_断言_快速教程
Bind: very useful in systemverilog. Assertion: 1.## “a ##3 b”意思是 a 之后 3 个周期 b…. 2.“|->”表示如果先行算子匹配,后序算子在同一周期...
system_verilog教程
* Data types * RTL design * Interfaces * Clocking * Assertion-based ...在 SystemVerilog,中,数组可以具有压缩数组或是非压缩数组的属性,也可以同时具有...
SystemVerilog语言教程
SystemVerilog 语言简介 SystemVerilog 是一种硬件描述和验证语言 (HDVL) 它基于 IEEE 1364-2001 Verilog , 硬件描述语言(HDL),并对其进行了扩展,包括扩充了 C ...
An overview of SystemVerilog 3.1
SystemVerilog provides special language constructs to verify design behavior. An assertion is a statement that a specific condition, or sequence of conditions...
一个牛人的Systemverilog总结
一个牛人的Systemverilog总结_计算机软件及应用_IT/计算机_专业资料。一个牛人的Systemverilog总结 Systemverilog 数据类型 l 合并数组和非合并数组 1)合并数组: 存储...
Systemverilog的数据类型教程
Systemverilog的数据类型教程_IT/计算机_专业资料 暂无评价|0人阅读|0次下载|举报文档 Systemverilog的数据类型教程_IT/计算机_专业资料。SystemVerilog的新数据类型...
systemverilog验证学习笔记
systemverilog验证学习笔记_计算机软件及应用_IT/计算机_专业资料 暂无评价|0人阅读|0次下载|举报文档systemverilog验证学习笔记_计算机软件及应用_IT/计算机_专业资料...
system verilog笔记
第三章 3.3 整数数据类型 shortint int longint byte bit logic reg integer time 数据类型 两态 SystemVerilog 数据类型,16位有符号整数 两态 SystemVerilog ...
SystemC和SystemVerilog的比较
SystemC 和 SystemVerilog 的比较时间:2010-03-18 20:49 来源:未知 作者:admin 点击: 356 次 SystemC、SystemVerilog 已经继 VHDL 和 Verilog 之后,成为 HDL ...
更多相关标签:
systemverilog | assertion | systemverilog assert | systemverilog验证 | verilog assertion | system verilog 教程 | systemverilog验证pdf | systemverilog bind |