System Verilog Assertion for debug

摘要: 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