SystemVerilog Assertions（SVA）本质上是一种语言结构，它为设计提供了编写constraints, checkers 和cover points 的方法。
例如，假设您的设计规范有以下2条规则：
- 每次请求
req拉高时，ack都会在3个时钟周期后到达 - 每次有效信号
vld拉高时，cnt都会增加
下面就是您使用SVA表达上述声明的方式。
// Check if ack arrives 3 clocks after a request
assert property (@(posedge clk) req |-> ##3 ack);
// Check if cnt increments everytime vld is set
assert property ((@posedge clk) vld |-> (cnt == ($past(cnt) + 1)); 现在，当您运行功能仿真时，这些断言将由仿真器监控，如果RTL违反了断言，仿真器将报告错误。这就是使用SVA编写checker的方式。
断言的类型
让我们从断言的类型开始——有两种。
即时断言
我喜欢将即时断言视为一个简单的陈述。这些断言不依赖于时钟边沿。
上述代码结构等同于always_comb块中的if条件。
always_comb begin
assert (current_state != 0) ; //do nothing;
else
$error("fail");
end当仿真运行时，仿真会持续检查表达式assert()如果它返回false，则会打印错误消息。
并发断言
并发断言允许您描述跨越时序并相对于时钟边沿触发的更复杂的表达式。
关键字property将直接断言与并发断言区分开来。有两种格式
// Format 1 - Inline expression
concurrent_assertion_name: // assertion label
assert
property (
@(posedge clk) disable iff (rst) // sampling event
req |-> ##3 gnt // expression to check
)
else // (optional) error message
$error("%m no grant after request");
// Format 2 - Separate property block
property ConcurrentPropName;
@(posedge clk) disable iff (rst)
req |-> ##3 gnt;
endproperty
AssertionName: assert property (ConcurrentPropName);上面的例子显示了并发表达式的一般结构。
- 断言在复位期间被禁用
- 表达式中的变量在指定的时钟边沿进行采样
- 该表达式检查
gnt是否在提出req后3个时钟到达。 - 如果表达式返回false，则报告错误
我喜欢将并发断言视为always_ff块中的语句。像这样
// This is just dummy code. It's an alternate way to think of concurrent assertion.
always_ff @(posedge clk) begin
if (rst) begin
// in rst
end else begin
if (assertion expression)
// do nothing;
else
$error("fail");
end
end
end当您为设计编写断言时，您会发现自己使用并发断言的频率比即时断言高得多。
