System Verilog Assertion是非常好的驗證方法，通過SVA可以顯式描述需要驗證的電路邏輯，并且仿真工具可以在仿真的過程中自動輸出波形出錯信息，從而替代傳統的看波形調試方法，提高前端設計驗證效率。

?RTL代碼結構

`ifdef SVA module m_sva(input wire signal);property p1;expression;endpropertya: 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

?

???

轉載于:https://www.cnblogs.com/QifanHu/p/5199012.html

總結

以上是生活随笔為你收集整理的System Verilog Assertion for debug的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。