标签：
System Verilog Assertion是非常好的验证方法，通过SVA可以显式描述需要验证的电路逻辑，并且仿真工具可以在仿真的过程中自动输出波形出错信息，从而替代传统的看波形调试方法，提高前端设计验证效率。
`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
System Verilog Assertion for debug
标签：
原文地址：http://www.cnblogs.com/QifanHu/p/5199012.html
