System Verilog Assertion for debug

Posted 2020-06-14

System Verilog Assertion是非常好的验证方法，通过SVA可以显式描述需要验证的电路逻辑，并且仿真工具可以在仿真的过程中自动输出波形出错信息，从而替代传统的看波形调试方法，提高前端设计验证效率。

 RTL代码结构

`ifdef SVA
module m_sva(input wire signal);
    property p1;
        expression;
    endproperty
    a: assert property(p1);
endmdule
bind m m_sva m_sva_inst(signal);
`endif

主要断言语法

a: assert property(@(posedge clk) red_main && $past( red_main ) |-> $past( yellow_main, 2 ))

@(posedge clk): 在时钟上升沿时验证断言，验证上升沿的前一个周期信号值  
$past(signal, n): signal信号往前数n个周期  
signal_a |-> signal_b: signal_a与signal_b信号的关系，signal_a可以是组合逻辑，结果为真时判断与signal_b的关系  

property e2;
    @ ( posedge clk) (!reset && $countones({ce0_N,ce1_N,ce2_N,ce3_N})==3) |-> ##1 $countones({ce0_N,ce1_N,ce2_N,ce3_N})==4;
endproperty

$countones(signal): 数signal信号值为1的比特位数  

property e1;
    @(posedge clk) ( ($rose( ce0_N )) || ($rose( ce1_N )) || ($rose( ce2_N )) || ($rose( ce3_N )) ) |-> (b_ce_idle) [*1:$] ##1 adxStrb;
endproperty

$rose(signal): 断言信号处在上升沿

$fell(): 断言信号处在下降沿

$stable(): 断言信号不变化
##[m, n]: 在[m, n]的时间窗内信号变化，如果`n=$`，代表没有上界

仿真命令

vcs命令中，加入-sverilog使得可以编译SystemVerilog语法，加入+define+SVA定义宏变量，$VCS_HOME/packages/sva目录下为assert_*模块。

rm -rf simv* csrc *.vpd *.log
vcs -sverilog +define+ASSERT_ON+SVA -y $VCS_HOME/packages/sva +libext+.v +incdir+$VCS_HOME/packages/sva traffic.v
./simv -l run.log