System Verilog Assertion是非常好的驗(yàn)證方法，通過SVA可以顯式描述需要驗(yàn)證的電路邏輯，并且仿真工具可以在仿真的過程中自動(dòng)輸出波形出錯(cuò)信息，從而替代傳統(tǒng)的看波形調(diào)試方法，提高前端設(shè)計(jì)驗(yàn)證效率。

?RTL代碼結(jié)構(gòu)

`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): 在時(shí)鐘上升沿時(shí)驗(yàn)證斷言，驗(yàn)證上升沿的前一個(gè)周期信號(hào)值 ?
$past(signal, n): signal信號(hào)往前數(shù)n個(gè)周期 ?
signal_a |-> signal_b: signal_a與signal_b信號(hào)的關(guān)系，signal_a可以是組合邏輯，結(jié)果為真時(shí)判斷與signal_b的關(guān)系 ?

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): 數(shù)signal信號(hào)值為1的比特位數(shù) ?

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): 斷言信號(hào)處在上升沿

$fell(): 斷言信號(hào)處在下降沿

$stable(): 斷言信號(hào)不變化
##[m, n]: 在[m, n]的時(shí)間窗內(nèi)信號(hào)變化，如果`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

?

???

轉(zhuǎn)載于:https://www.cnblogs.com/QifanHu/p/5199012.html

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。