一、序言

本文是读《Formal Verification An Essential Toolkit for Modern VLSI Design》第三章，做的一些笔记。

SVA，即SystemVerilog Assertion，在simulation和Formal都有极为广泛的应用，这里介绍一些基本的概念和常用的语法。

二、一个简单的例子

以一个arbiter仲裁器作为例子来阐述一些概念，这个仲裁器有4个request来自不同的agent，req的每个bit表示相应的仲裁请求发起。gnt信号每个bit表示相应的请求被允许。同时，这里还有一个opcode输入，用来override正常的请求，例如强制某个agent获得grant，或者让所有的gnt都无效一段时间。error信号表示一些错误的输入序列或者错误的opcode。模块框图如下所示：

interface代码如下：

typedefenum logic[2:0 {NOP,FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON} t_opcode;

 module arbiter(
     input logic [3:0] req,
     input t_opcode opcode,
     input logic clk, rst,
     output logic [3:0] gnt,
     output logic op_error
 );

三、基本概念

在介绍SVA之前，我们先来澄清几个容易混淆的概念，尤其是assertion和assumption，傻傻分不清。

3.1 Assertion

assertion一般用来表示一个表达式恒为True，比如agent0未发起request，则gnt[0]不应该被拉起来。这种情形我们可以用assertion来加以检查。

 check_grant: assert property (!(gnt[0] && !req[0])) else $error(“Grant
 without request for agent 0!”);

3.2 Assumption

assertion一般用于检查DUT内部的状态，而Assumption则主要用于约束验证环境，主要用于约束输入。例如我们期望opcode应该是合法的一些参数，就可以用assumption语句来进行约束。

 good_opcode: assume property (opcode inside {FORCE0,FORCE1,FORCE2,
 FORCE3,ACCESS_OFF,ACCESS_ON}) else $error(“Illegal opcode.”);

在simulation中，assumption跟assertion运行效果一样，都是用来检查输入。但在Formal里面，二者则有很多的区别。对于上面那个assumption，在simulation中，不断的检测opcode，不在这些数里面则报一个assertion failure。在Formal里面，这是表示opcode激励只能在这些数里面取值，大家可以将其理解成一个输入的constraint。

3.3 COVER POINTS

这个没什么好说的，在simulation和formal里面都是一致，用来表征覆盖率。

不过需要注意的是，FV通常可以全覆盖。但是因为有assumption，我们有时候会overconstraint ，这样有些东西就可能被漏掉。所以coverpoint在FV里面至关重要。

一般来说，FV上来就先写coverpoint，先规划好哪些点需要覆盖。其次还是assertion和assumption。这样就不会出现过overconstraint而不自知的情形。

四、SVA 语法介绍

SVA Asssertion 语言分为几个等级，自下而上，可以分成四个等级，即boolean、sequence、property和assertion statement，如下图所示：

Booleans
Booleans 即布尔表达式，一些与或非的逻辑，例如:

     (req[0]&&req[1]&&req[2]&&req[3])

Sequences
Sequences 顾名思义，就是boolean 表达式的序列，也就是说一段时间（几个cycle）的booleans的组合，以来与clock event来定义这个区间，例如req0有效两个cycle后gnt0有效

 req[0]##2gnt[0]

Properties
Properties 则是进一步将sequences和一些操作符组合起来，表示一个implication或者其他的。比如：
```
req[0]##2gnt[0]|->##1!gnt[0]
```
Assertion Statements
Assertion Statements 则是用assert, assume, cover等关键词将properties例化，把SVA property 转换成真正意义的assertion, assumption, cover point. 例如：

     gnt_falls:assertproperty(req[0]##2gnt[0]|->##1!gnt[0]);

另外还有两个概念需要明确:

immediate assertions
Immediate assertion 简单的assertion语句，只能用于procedural 语句里面。只支持booleans，不能有clock， reset或者property语句。

  imm1: assert (!(gnt[0] && !req[0]))

concurrent assertions
Concurrent assertion 语句则一般用于检查多个cycle期间段的一些property，一般我们说SVA基本代指Concurrent assertion
```
conc1: assert property (!(gnt[0] && !req[0]))
```

五、CONCURRENT 语法

concurrent assertion的一般写法如下例所示:

 safe_opcode:assertproperty(
 @(posedgeclk)
 disableiff(rst)
 (opcodeinside{FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))
 else$error(“Illegalopcode.”);

一般包含下面几点：

带关键词assert property.
带clock
可选的disable iff语句

5.1 常用函数

SVA自带了一些系统函数，这里列出一些常用的供参考。

5.2 Disable iff

Disable iff (iff表示if and only if)语句，顾名思义就是在某个条件成立的时候将assertion语句disable掉。但这里有点需要特别注意的是，diasable iff里面的逻辑采样不是基于clock的，或者说相对clock来说是异步的。建议里面只放reset逻辑，不要放其他的逻辑。我们举个例子，如果有gnt，那么铁定有个req，两种写法：

 bad_assert: assert property (@(posedge clk)
 disable iff
 (real_rst || ($countones(gnt) == 0))
 ($countones(req) > 0));

 good_assert: assert property (@(posedge clk)
 disable iff (real_rst)
 (($countones(req) > 0) ||
 ($countones(gnt) == 0)));

表面上看，二者似乎一样。仔细分析下，在clock 8的phase，由于gnt=0，整个assertion直接被disable，我们也就没法检测出上一个cycle的failure。

这里其实是涉及到SVA的采样时间问题，或者说systemverilog的region问题，建议翻阅<<writing testbench in systemverilog>> 这本书，里面有非常详细的解读。

六、SEQUENCE 语法

6.1 delay

sequence 基本的操作符是#,即delay，##n (延时特定个cycle) or ##[a:b] (延时 a 到b 个cycle) 。

6.2 repetition

repetition 操作符 [*m:n] ，表示subsequence 重复多少次。

6.3 logical ops

Sequences 可以通过and 或者or组合起来。

and: 两个sequence同时start，但它们的结束点未必相同。

or: 两个sequence至少有一个match

throughout : Boolean expression remains true for the whole execution of a sequence

within: one sequence occurs within the execution of another

6.4 go to repetetion

goto repetition 操作符，即 [- > n] 和 [ =n] ，表示有value重复了正好n次，未必是连续的cycle。

这两个操作符如果后面不接其他的东西的话，是等价的。如果后面带有其他的sequence的话，意义有点不一样：

[->n]: goto repetition，下一个sequence必须紧接着。
[=n]: nonconsecutive goto repetition，下一个seuquece出现前允许插入若干个cycle的空闲

6.5 Implication

sequence |-> property ：sequence match后立即检查property

sequence |=> property. ：sequence match后delay一个cycle再检查property

左边称为antecedent （先决条件），必须为sequence；右边称为consequence （结果），可以是squence或者property。

需要强调一点，如果antecedent 在整个过程都不满足的话，这个assertion也不会fail，这种情形在formal中称为vacuously，即空的pass。

还有一些SVA语法，不是很常用，可以用到时候翻阅手册查询

六、MULTITHREADING

MULTITHREADING，即多线程。这里需要强调下，assertion的多线程属性；每次antecedent为真，工具都将新启动一个线程来check，我们以一个例子来进行说明。

req信号有效后，10个cycle之后gnt信号应该有效。代码如下：

delayed_gnt: assert property (req[0] |-> ##10 gnt[0])

由于req和gnt之前隔了10个cycle，很有可能在这中间req信号再次被拉起，如果这样的话，工具会启多个线程，每个线程检查相应的req和gnt对应的关系。

七、总结

SVA语法较多，需要反复练习才能掌握和精通。尤其是它的debug，需要反复实践，加以体会。不建议写很复杂的SVA，不方便debug。

欢迎大家留言探讨，祝大家元旦快乐。

作者：木马哥
文章来源：验证工程师的自我修养

推荐阅读

更多IC设计技术干货请关注IC设计技术专栏。
迎添加极术小姐姐微信（id:aijishu20)加入技术交流群，请备注研究方向。

形式验证中的SVA