一个SVA断言应用的示例
本文将使用一个简单的Arbiter（仲裁）设计示例展示SVA断言的概念和用法。
这个仲裁器有四个请求口req ，gnt信号指示哪个请求被授权。还有一个输入opcode允许使用命令来指定某些行为，例如强制一个特定的请求口获得优先级或者在一段时间内阻挡所有访问。还有一个输出op_error ，用来告警发送了错误的opcode 。
下面是模块的接口信号：
typedef enum 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主要分为3类，assertion、assume和cover。下面将依次介绍：
什么是ASSERTIONS？
assertion 是关于设计的一种属性描述。例如，对于我们的仲裁设计，当req0没有被请求时，就不会期望被授予gnt0
check_grant: assert property (!(gnt[0] && !req[0])) else $error(“Grant
without request for agent 0!”);当在仿真器上运行仿真时，当检测到代码中的SVA断言出现错误，仿真器就会打印一些fail信息。
在上面的示例中，如果在仿真中看到gnt[0]== 1 并且req[0]== 0 ，那么就会打印“Grant without request for agent 0!”。
在运行FPV工具时，会将断言作为证明的目标：该工具的目标是从数学上证明你的RTL设计永远不能违反这个断言。
什么是ASSUMPTIONS?
Assumptions 不是指定DUT设计的行为，通常指定验证环境上的约束条件。例如，我们希望仲裁设计只能发送合法的非nop操作：
good_opcode: assume property (opcode inside {FORCE0,FORCE1,FORCE2,
FORCE3,ACCESS_OFF,ACCESS_ON}) else $error(“Illegal opcode.”);对于EDA仿真，对一个assumption 的处理方式和assertion完全相同。仿真器会检查当前的验证输入是否违反指定的条件，但是概念上还是有些区别的。从规范的角度来看，assumption应该用来检查EDA验证中的设计输入， assertion检查RTL设计中的输出（或者内部信号）。
在FV中，assumptions 和assertions就有很大的区别。见词知意，assumption 是工具的假设，从逻辑学的角度是无需证明的公理，从验证的角度是输入的合理约束。
什么是COVER ?
SVA cover与assertions 和assumptions类似，cover指定了一些场景来证明这些场景有被测试到。例如，在仲裁设计中，我们可能想要确保的请求口同时请求的场景：
cover_all_at_once: cover property
(req[0]&&req[1]&&req[2]&&req[3]);对于FV，cover 也起着重要的作用。虽然FV理论上能够覆盖设计中所有可能的行为，但是不能保证我们验证环境中没有过约。因此，确保FPV环境能够覆盖所有你关心的场景是一个非常非常关键的步骤。
最后，对于cover一定要重视。验证工程师不能过分依赖formal工具和随机机制，波形和覆盖率往往才是王道。
写一个SVA断言分几步？
SVA assertions, assumptions和cover都是采用相同的语法格式进行指定的。 刚接触SVA语法，可能觉得比较难学，语法格式很奇怪，特别是给RTL设计人员造成了一定的门槛。
化繁为简，分层用起来！
SVA可以看作是几个层次的叠加，如下图所示
01
Booleans 是标准的SVA语言中的布尔表达式。一个布尔表达式可以是单个的逻辑变量或一个公式，如前文例子中的
(req[0]&&req[1]&&req[2]&&req[3])02
Sequences 是关于布尔值或逻辑序列的语句。Sequences 依赖于一个时钟事件，例如下面的序列表示仲裁请求在2个时钟周期后被授权。
req[0] ##2 gnt[0]03
Properties 表达一些期望在设计中保持的行为。例如，一个属性可能会声明，如果我们收到一个请求2个周期后授权gnt，然后下一个周期拉低gnt：
req[0] ##2 gnt[0] |-> ##1 !gnt[0]04
Assertion 语句是断言关键字，仅仅声明一个Properties 没有任何行为，只有加上assert才能触发检查：
gnt_falls: assert property(req[0] ##2 gnt[0] |- >##1 !gnt[0]);对于assertions，我们还需要引入2个关键概念：即时断言（immediate assertions）和并发断言（concurrent assertions）
• 即时断言是一种简单的断言语句，用于在过程语句中执行检查。没有clk参数，也就无法检查事件序列，如下示例（没有property关键字）：
imm1: assert (!(gnt[0] && !req[0]))• 并发断言可以事件序列，可以描述clk时序相关的属性。因此，在数字IC中并发断言语句更有用。如下示例（有property关键字）：
conc1: assert property (!(gnt[0] && !req[0]))即时断言和并发断言非常相似，很有时候也可以相互转化，两者区别类似于SV语法中function和task的区别，一般建议只使用并发断言。
如何在实际项目中使用SVA断言
相信很多人对于SVA断言都有些基本的了解，但是在实践中并没有发挥出其最大的价值。那么在实际的项目中，设计人员和验证人员究竟应该如何合理地使用SVA断言呢？
01 设计人员使用SVA断言
在RTL开发过程中，很多优秀的设计工程师会在RTL代码中添加注释，以描述他们的实现思路以及希望验证测试的内容等等。基于这个思路，SVA断言可以被认为是“可执行的注释”。
SVA可以用来解释代码的意图，同时可以用来在仿真和FPV阶段进行检查。比较以下两个代码片段：
// Fragment 1
// We expect opcode to be in the valid range; bad
// opcode would result in bypassing these lines.
// Also, don’t forget to test each possible value.
assign forced_nodes = f_get_force_nodes(opcode);// Fragment 2
op_ok: assert property
((opcode >= 0)&&(opcode <= 5));
generate for (i = 0;i <= 5;i++) begin: b1
test_opcode: cover property (opcode == i);
end
endgenerate
assign forced_nodes = f_get_force_nodes(opcode);可以看到，上面的两个代码都传达了我们期望opcode在一个有效的范围并且两者都要求我们测试每个可能的opcode值，只有第二个代码是一种强制执行的方式。
当以后的项目需要对这些RTL进行复用时，如果仿真违反了断言就会看到断言失败的打印。如果验证工程师没有测试到这些opcode也能够很容易地被发现。
对于设计工程师来说，不应该书写assume，即使assume和assert在EDA验证中的行为是一致的，但是对于FPV工具来说容易导致过约。
1、当你在开发RTL时，每当你准备写一个关于期望值的行为或者注释，想想它是否可以被声明为一个SVA的断言。断言可以看作是一个“可执行的注释”，以更好地达到你的目的。（不要害怕断言写错被验证提缺陷单哦）
2、当你在开发RTL时，每当你准备写一个注释，希望验证能够进行某些测试，想想它是否写成SVA Cover。
02 验证人员使用SVA断言
验证工程师常常也需要编写断言已达到验证目的或者使用FPV进行形式验证。这时我们使用SVA的目的就是验证，我们需要以需求和规格为起点编写SVA断言。例如，前文提到的仲裁模块可能有以下规格：
1、当opcode ==FORCEn时，请求n获得授权。
2、当opcode ==ACCESS_OFF时，没有请求n获得授权。
3、如果opcode无效时，op_error信号为1，否则为0。
当我们有类似这样的规格时，我们通常应该尝试编写“端到端”的断言，指定输入如何对应到输出。
端到端的验证是发现bug的最有效方式。基于内部信号的白盒断言也可以提高验证完备性或者提高调试效率，但是如果只依靠白盒验证是很危险的事情，因为验证工程师太关注设计工程师的实现细节了，被设计带着走，而没有理解模块的设计意图。
对于验证，应该根据规格编写复杂的“端到端”断言，即输入如何决定输出。也要写一些cover以确认主要的场景是否已被验证。
此外，根据我们设计的复杂性，一般很难使用一组简单的断言满足我们的需求。我们可能还需要一些SystemVerilog代码来进行建模（类似于设计编写verilog代码，只是我们不关心PPA，但是我们需要注意复杂的建模容易让仿真器变慢）。
现在让我们来看看应该针对上述仲裁的规格如何编写断言：
当opcode ==FORCEn时，请求n获得授权。
这个规格看起来很简单，但是仍然有一些疑问需要设计确认或者补充规格,例如请求获得授权的延迟。另外比较重要的是，验证工程师需要提取一些隐含的规格需求，即授权应该是onehot。我们还应该增加适当的cover确保我们验证了这个规格所有相关的功能点。
parameter t_opcode fv_forces[3:0] =
{FORCE3,FORCE2,FORCE1,FORCE0};
generate for (i = 0; i <= 3;i++) begin: g1
forcei: assert property (
(opcode == fv_forces[i]) | ->
(gnt[i] == 1) && ($onehot(gnt))) else
$error(“Force op broken.”);
cover_forcei: cover property (
(opcode == fv_forces[i])
&& (gnt[i] == 1));
end
endgenerate当opcode ==ACCESS_OFF时，没有请求n获得授权。
如果opcode无效时，op_error信号为1，否则为0。
这两个规格比较简单，但要注意我们不仅需要断言无效的opcodes 会输出error，而且还需要断言有效的opcodes 不会输出error。
accessoff:
assert property ((opcode == ACCESS_OFF) | => (|gnt == 0 ))
else
$error (“Incorrect grant: ACCESS_OFF.”);
logic fv_validop;
assign fv_validop = (opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON});
error0:
assert property (fv_validop | => !op_error);
error1:
assert property (!fv_validop | => op_error);
cover_nognt: cover property (|gnt == 0);
cover_err: cover property (!fv_validop ##1 !op_error);在我们快要完成我们的验证工作时，我们一定要回过头来看看我们的规格，是否有一些规格没有明确。对于仲裁，往往还会考虑其公平性。
作者：验证哥布林
原文链接：芯片验证工程师
微信公众号：
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏
