本文将使用一个简单的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工具和随机机制，波形和覆盖率往往才是王道。
作者：验证哥布林
原文链接：芯片验证工程师
微信公众号：
推荐阅读
更多IC设计技术干货请关注IC设计技术专栏
