一个简单的断言(SVA)示例

[导读]断言的英文是Assertion，就是对一些设计属性的推断。大型的硬件设计中会有各种各样的协议接口。这些协议接口定义中一般都会有include文件，这些include文件中包含了接口的断言描述，主要用于协议的时序检查。除了这种把断言语句放到接口协议里还可以放到具体的design里面...

断言的英文是Assertion，就是对一些设计属性的推断。

大型的硬件设计中会有各种各样的协议接口。这些协议接口定义中一般都会有include文件，这些include文件中包含了接口的断言描述，主要用于协议的时序检查。

除了这种把断言语句放到接口协议里还可以放到具体的design里面，也可以单独做成一个module的checker，把module checker和设计bind在一起。

断言可以用Verilog实现，也可以用SystemVerilog Assertion（SVA）实现。由于要检查时序，过程性语言Verilog并不是很好的选择，一般会选择描述性语言SVA实现，SVA对时序的描述近乎完美。

本文讲介绍一下SVA的简单例子。如果想系统的学习SVA，可以买一本书《SystemVerilog Assertions 应用指南》。

方法1: 直接放到到design里面的方式如下。

//文件dut.v ， dut很简单，每个clk上升沿到来时对输入a取反。`timescale 1ns/1nsmodule DUT (clk,a,b);input clk;input a;output b;reg b; always @ (posedge clk )begin b<=~a;end`include "assertion.svh"endmodule

//文件 test.v`timescale 1ns/1nsmodule TOP;reg clk;reg a;wire b;always #5 clk=~clk;initial begin clk <=0; a <=1;#30 $finish;endDUT dut(.clk(clk),.a(a) ,.b(b));//bind TOP.dut dut_assertion dut_assertion_check(.a_(a),.b_(b),.clk_(clk));endmodule每个clk上升沿，如果a=0，则是空成功，不满足第一个a=1的条件，b就不需要判断是否等于1，直接判断为成功。如果a=1，则对b进行判断，b为1则为成功，否则断言失败。

//assertion.svh文件property check_p; @(posedge clk) a |->b;endpropertycheck_a : assert property (check_p);运行命令：irun -sv dut.v test.v

ERROR：ncsim: *E,ASRTST (./assertion.svh,6): (time 5 NS) Assertion TOP.dut.check_a has failed

ERROR现象符合预期。

方式2：单独定义一个module 检验器，然后通过bind实现。

注释DUT.v 中`include "assertion.svh"，打开test.v中的bind。

Module检验器文件

module dut_assertion(a_,b_,clk_);input logic a_,b_,clk_;property check_p;@(posedge clk_) a_ |->b_;endproperty check_a : assert property (check_p);endmodule运行命令：

irun -sv dut.v test.v assertion_module.sv

ERROR：ncsim: *E,ASRTST (./assertion_module.sv,12): (time 5 NS) Assertion TOP.dut.dut_assertion_check.check_a has failed