提示：文章写完后，目录可以自动生成，如何生成可参考右边的帮助文档

---

前言

• SVA是SystemVerilog中提供的一种强大的语言特性，可以用于写constraints, checkers和cover points。与普通的SV语法相比，在对design进行检查时可以起到事半功倍的效果。
• DE通常在rtl module内编写assertion，一方面可以检查设计的正确性，一方面还可以检查激励的合法性。DV通常在单独的interface/module中写assertion，然后使用bind将sva module和design module进行绑定。
• 笔者参考了一些资料，整理了一些有关SVA的简介、语法构成此篇学习札记。并且笔者认为，只需要了解以下这些知识，就可以上手写assertion了。

---

一、立即断言和并发断言

1. 立即断言（intermediate assertion）

类似if-else statement，需要放在procedural block中，但不依赖clock edge或reset。评估expression的结果后会立即执行pass/fail statement(action block)，因此是立即断言。
【常见语法形式】

assertion_label: assert(expression) pass_statement;
                                   else fail_statement;

• assertion_label: 对assertion块进行命名，可以用%m打印；optional，可以不写label。如下面的代码，如果expression为false，则会报assertion error并打印“assertion_label failed.”

assertion_label: assert(expression) pass_statement;
                                   else $error("%m failed.");

• expression: 通常是一个布尔表达式（Boolean expression）。如果结果是X, Z或0则false，否则为true。
• pass_statement/fail_statement: 统称action block，指断言成功或失败时进行的操作；optional，可以不写，但fail_statement默认$error。此外还可以使用$fatal/$warning/$info。

2. 并发断言（concurrent assertion）

同样类似if-else statement，可以放在procedural block/module/interface/self-defined program中。但只能在clocking blocks中发生，在边沿对变量进行采样，然后根据变量的采样值对expression进行评估。与立即断言不同，并发断言是一个连续运行的模块，在整个仿真过程中检查信号的值。
【常见语法形式】

//format 1
assertion_label:
    assert
        property (
        @(posedge clk) disable iff(rst)
        expression
        ) pass_statement;
        else fail_statement;

//format 2
property property_label;
   @(posedge clk) disable iff(rst)
   expression;
endproperty
assertion_label: assert property(property_label) 
                        pass_statement;
                        else fail_statement;

• 简单来说，可以用property来区分立即断言和并发断言。
• @(posedge clk)代表在clk上升沿对expression内的变量进行采样。
• disable iff(rst)代表在rst为高时不进行断言检查。
• property内可以使用 |-> 和 |=> 操作符，相比立即断言可以对更复杂的场景进行检查。

二、常用System Function和Operator

1.System Function

function	description
$rose	如果信号发生从0到1的跳变则返回true，否则返回false；
$fell	如果信号发生从1到0的跳变则返回true，否则返回false；
$stable	如果信号未发生跳变则返回true，否则返回false；
$past(expression, num_cycles)	返回该expression在num_cycles个周期前的值；
$countones	返回expression中1的个数；
$onehot	如果有且仅有一个bit为1则返回true，否则返回false；
$onehot0	如果仅有一个bit为1或所有bit都为0则返回true，否则返回false；
$isunknown	如果expression中含有X或Z则返回true，否则返回false；

2.Operator

• Delay Operator 延时操作符（##n, ##[n:m]): 延时n个周期、延时n~m个周期；
• Boolean Operator布尔操作符（!, ||, &&): 取反、或、与；
• Implication Operator蕴涵操作符 (|->, |=>) :
  o Overlapping implication operator(|->): the RHS is evaluated from the same cycle LHS is true
  o Non-overlapping implication operator(|=>): the RHS is evaluated one clock cycle after LHS is true
  o To keep your code consistent, use |-> only.
• Repetition Operator重复操作符:
  o Continuous repetition operator ([*n], [*m:n]);
  o Go-to repetition operator ([->n], [->m:n]);
  o Nonconsecutive repetition operator ([=n], [=m:n])

//continuous repetition operator
a ##1 b [*5]  //如果a为高，则1周期后b连续5周期为高
a ##1 b [*5:10]  //如果a为高，则1周期后b连续5~10周期为高

//go-to repetition operator
a ##1 b[->2:10] ##1 c //如果a为高，则1周期后b为高2~10周期的1周期后，c为高
                      //b不必是立即、连续2~10周期为高，但1周期后c为高需连续
                      //eg: a, !b, b, b, !b, b, c
                      
//nonconsecutive repetition operator
a ##1 b[=2:10] ##1 c //如果a为高，则1周期后b为高2~10周期的1周期后，c为高
                      //b不必是立即、连续2~10周期为高，1周期后c为高也不必是连续
                      //eg: a, !b, b, b, !b, b, !b, c

• property operator: not, and, or;
• and vs &, or vs | in SVA
  o &, | 只能用于布尔表达式中，且只能用于同一cycle的变量值的布尔逻辑运算。
  o and, or 可用于布尔表达式或sequence中，用于sequence时可以对不同cycle的表达式进行布尔逻辑运算，如：

//布尔表达式中可以用&或and
a & b
a and b

//左右两个sequence并不在同一cycle发生，只能用and而不能用&
(a ##3 b) and (a ##5 c) 

三、在什么地方写SVA

DE通常在rtl module内编写assertion，一方面可以检查设计的正确性，一方面还可以检查激励的合法性。DV通常在单独的interface/module中写assertion，然后使用bind将SVA module和design module进行绑定。

---

参考文献

[1] https://www.systemverilog.io/sva-basics
[2] https://blog.csdn.net/weixin_39060517/article/details/116002244
[3] https://cloud.tencent.com/developer/article/1653764