SV断言的小技巧及实用例子

2019-10-29

SVA（SV断言手段）

SVA是一种强大的验证手段，本文将介绍一些工作中实用的方式。

验证寄存一拍
SVA调用function
SVA实现循环检查
SVA实现FIFO空满检验
references

验证寄存一拍

之前接触过一个DUT，子模块的部分输入打两拍后输出给下一级子模块。如果使用UVM，专门写一个monitor，一个scoreboard会表现出一种杀鸡焉用牛刀的感觉。其实，这种和时序密切相关的输出，可以直接使用SVA：

Title: UVM大哥和SVA小老弟
Input->Output: 寄存两拍
SVA->Output: 大哥，小弟先上！
UVM->SVA: SVA小老弟，杀鸡沿用牛刀？

property cmd_wrdata_check;
    bit[32:0] data;
    @(posedge clk_i)
        disable iff (!rstn_i) (1, data = data_i) |=>##1  (data == data_o);    
endproperty

Explain：断言中的信号值实际上是时钟沿到来之前的值。所以，对于非阻塞复制：b<=a逻辑的断言应该是：“@ (posedge clk) (1,tmp=a) |=> (b==tmp);”。上例多延时一拍”##1“，从而实现了寄存两拍的效果。

调用function

SVA还可以对保存的数据做简单的处理。这个类似于写一个reference model，并且实现每个cycle级别的检查。

1
2
3

Title: DUT大哥和SVA小老弟
Input->Output:我怎么才能知道输出不会出现01，10的情况 
SVA->Output: DUT大哥，我来调function！

property wren_check;
    @(posedge clk_i)
        disable iff(!rstn_i) (1) |-> (checking_wren()) ;
endproperty

function checking_wren();
    bit [11:0] temp;
    for(int i=0; i<12; i++) begin
        temp[i] = source_wren[2*i] ^ source_wren[2*i+1];
    end
    checking_wren = ~(&temp);
endfunction

Explain：例2使用了断言可以调用function，从而检查了相邻bit位不能出现01，10的情况。结合例1，聪明的你是否也发现，SVA还可以利用function的结果作为下一级的判断条件呢？

实现循环检查

验证小伙儿又犯难了，这次要让他验证一个clock gating。这个gating被总共例划了的12份。所有都一样，只是hierarchy中行列号不同。写12个断言吧，不是不行，只是显得冗余。

1
2
3

Title: 重复和SVA小老弟
Input->Output:我有12个clock gating呢！ 
SVA->Output: 重复劳动我也能解决！

property clock_gate_check(signal1, signal2);
	@(posedge clk_i)
		disable iff (!rstn_i) (!signal1) |-> (!signal2);
endproperty

generate
	for(genvar i=0; i<6; i++) begin: assert_ck_i
        for(genvar j=0; j<2; j++) begin: assert_ck_j
		   assert property(clock_gate_check(
                                               test_top.dut.row[i].col[j].en,
                                               test_top.dut.row[i].col[j].clk_gate.en));
		end
    end
endgenerate

Explain：例3显示利用property生成一个模板，然后使用generate语句重复调用这个模板，从而实现了对12个clock gating的验证。

FIFO空满检验

断言在验证FIFO的空满标志时也非常实用。

1
2
3

Title: FIFO和SVA小老弟
Input->Output:我的空满能验吗？ 
SVA->Output: Easy！

//counter
reg [15:0] w_cnt,r_cnt;
wire [15:0] cnt;
always@(posedge wif.clk)begin
    if(~wif.rstn)
        w_cnt<=16'b0;
    else if(wif.en)
        w_cnt<=w_cnt+1;
end
always@(posedge rif.clk)begin
    if(~rif.rstn)
        r_cnt<=16'b0;
    else if(rif.en)
        r_cnt<=r_cnt+1;
end
//check current counter
assign cnt=w_cnt-r_cnt;

//check full
property full_chk;
    @(posedge wif.clk) disable iff(~wif.rstn)
        cnt==32 && $rose(cnt[5]) |-> $rose(wif.valid);
endproperty

a_full_chk: assert property(full_chk) 
                $display("check full pass");
            else 
                $display("ERROR: check full fail");
c_full_chk: cover property(full_chk);

//check empty
property empty_chk;
    @(posedge rif.clk) disable iff(~rif.rstn)
        cnt==0 && $fell(cnt[0]) |-> $rose(rif.valid);
endproperty


a_empty_chk: assert property(empty_chk) 
                $display("check empty pass");
             else 
                $display("ERROR: check empty fail");
c_empty_chk: cover property(empty_chk);

Explain：例4验证的是一个深度为32的FIFO，通过利用读写两个counter去记录目前为止。一旦满了，cnt=32，full应该立即拉高。一旦为空，cnt=0，empty应该立即拉高。

references

Mehta A B. SystemVerilog Assertions and Functional Coverage[M]. Springer., 2014.
http://blog.sina.com.cn/s/blog_4c270c730101f6mw.html