systemverilog - 断言 - 快速教程

Bind: very useful in systemverilog. Assertion:

1．## “a ##3 b”意思是a 之后3个周期b….

2．“|->”表示如果先行算子匹配，后序算子在同一周期开始计算 3．“|=>”表示如果先行算子匹配，后序算子在下一个周期开始计算 4．重复操作符：

* ** ***

连续重复“[*m]”: “a[*1:3]”表示a被连续重复1~3次 跳转重复 “[->]”: “a[->3]”表示a被跳转重复3次 非连续重复 “[=m]”: “a[=3]”表示a被非连续重复3次

芯片设计：verilog断言（SVA）语法

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

1. SVA的插入位置：在一个.v文件中： module ABC (); rtl代码 SVA断言

endmodule

注意：不要将SVA写在enmodule外面。

2. 断言编写的一般格式是：

【例】断言名称1：assert property(事件1) //没有分号 $display(\有分号 else

$display(\有分号

断言名称2：assert property(事件2) $display(\ else

$display(\

断言的目的是：断定“事件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; intcnt;

..................... 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：在“时序逻辑”中判断独立的一根信号的行为：

@ (posedgeclk) 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) @ (posedgeclk) a |-> b ———— 断定clk上升沿后，a事件“开始发生”，同时，b事件发生。

(6) @ (posedgeclk) a.end |-> b ———— 断定clk上升沿后，a事件执行了一段时间“结束”后，同时，b事件发生。

注：\在逻辑上是一个判断句式，即：

if a b; else

succeed;

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

(7) @ (posedgeclk) a |=> b ———— 断定clk上升沿后，a事件开始发生，下一个时钟沿后，b事件开始发生。

(8) @ (posedgeclk) a |=>##2b ———— 断定clk上升沿后，a事件开始发生，下三个时钟沿后，b事件开始发生。

(9) @ (posedgeclk) $past(a,2) == 1'b1 ———— 断定a信号在2个时钟周期“以前”，其电平值是1。

(10) @ (posedgeclk) a [*3] ———— 断定“@ (posedgeclk) a”在连续3个时钟周期内都成立。 @ (posedgeclk) a [*1:3] ———— 断定“@ (posedgeclk) a”在连续1~3个时钟周期内都成立。

@ (posedgeclk) a [->3] ———— 断定“@ (posedgeclk) a”在非连续的3个时钟周期内都成立。

举一个复杂点的例子：

property ABC; inttmp;

@(posedgeclk) ($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：屏蔽不定态

当信号被断言时，如果信号是未复位的不定态，不管怎么断言，都会报告：“断言失败”，为了在不定态不报告问题，在断言时可以屏蔽。

如： @(posedgeclk) (q == $past(d))，当未复位时报错，屏蔽方法是将该句改写为： @(posedgeclk) disable iff (!rst_n) (q == $past(d)) //rst是低电平有效

10. 语法6：断言覆盖率检测：

name: cover property (func_name)

11. 在modelsim中开启断言编译和显示功能：

（1）【编译verilog代码时按照system verilog进行编译】 vlog -svabc.v （2）【仿真命令加一个-assertdebug】 vsim -assertdebug -novopttestbench （3）【如果想看断言成功与否的分析，使用打开断言窗口的命令】 view assertions

12. 在VCS中加入断言编译和显示功能： 在fsdb文件中加一句话：$fsdbDumpSVA

在VCS编译参数：system \中加入一些options: -assert enable_diag\\

-assert vpiSeqBeginTime\\

本文来源：https://www.bwwdw.com/article/933t.html