基于形式驗(yàn)證的毛刺檢測(cè)技術(shù)

朱秋巖，李東方

(北京計(jì)算機(jī)技術(shù)及應(yīng)用研究所， 北京 100854)

0 引 言

SoC(system on chip)設(shè)計(jì)的功能驗(yàn)證是SoC設(shè)計(jì)中最復(fù)雜也是最重要的任務(wù)。傳統(tǒng)檢測(cè)毛刺是在時(shí)序仿真階段，仿真對(duì)象為添加延遲文件的布局布線后網(wǎng)表，所以難以在RTL(register transfer level)驗(yàn)證階段有效發(fā)現(xiàn)毛刺及其對(duì)功能的影響[1]。此外標(biāo)準(zhǔn)RTL仿真不能模擬毛刺的影響，由于毛刺導(dǎo)致的錯(cuò)誤在RTL沒有得到解決，導(dǎo)致SoC驗(yàn)證后期出現(xiàn)功能錯(cuò)誤，造成了設(shè)計(jì)迭代并影響產(chǎn)品的上市時(shí)機(jī)。

近些年形式驗(yàn)證技術(shù)迅速發(fā)展，在集成電路驗(yàn)證中得到了廣泛應(yīng)用。在模型驗(yàn)證中，首先使用時(shí)態(tài)邏輯來描述設(shè)計(jì)意圖，其次使用數(shù)學(xué)推理來驗(yàn)證設(shè)計(jì)意圖在實(shí)現(xiàn)(RTL)中是否得以貫徹。結(jié)合形式驗(yàn)證的方法，文獻(xiàn)[2]提出了跨時(shí)鐘域中毛刺的檢測(cè)方法，但需要額外使用時(shí)鐘路徑區(qū)分控制信號(hào)，而且該方法設(shè)計(jì)的檢測(cè)電路，僅能證明時(shí)鐘路徑區(qū)分控制信號(hào)有效時(shí)無毛刺，用于糾正靜態(tài)時(shí)序分析中誤報(bào)的違例，不能用于檢測(cè)是否產(chǎn)生毛刺。文獻(xiàn)[3]提出了采用形式驗(yàn)證檢查抖動(dòng)錯(cuò)誤的方法，僅對(duì)跨時(shí)鐘域故障建模，沒有對(duì)毛刺進(jìn)行建模，也沒有考慮故障模型的可觀性。

在本文中，提出一種使用形式驗(yàn)證技術(shù)在RTL級(jí)檢測(cè)毛刺的方法，本文在文獻(xiàn)[2]作者提出的利用靜態(tài)時(shí)序分析方法基礎(chǔ)上，設(shè)計(jì)一種毛刺檢測(cè)電路，采用形式驗(yàn)證斷言的方式描述該電路屬性，用于在RTL級(jí)檢測(cè)組合邏輯中可能產(chǎn)生的毛刺，并且不需要額外的控制信號(hào)，能夠?qū)崿F(xiàn)自動(dòng)檢測(cè)；然后提出描述毛刺影響的等價(jià)電路，用以在RTL級(jí)驗(yàn)證中準(zhǔn)確體現(xiàn)毛刺現(xiàn)象的實(shí)際影響。為驗(yàn)證毛刺檢測(cè)電路和故障注入電路的有效性，本文還分析了毛刺故障傳播模型，在可觀測(cè)點(diǎn)驗(yàn)證毛刺的影響。

1 毛刺檢測(cè)電路設(shè)計(jì)

本節(jié)首先分析毛刺產(chǎn)生機(jī)理，然后設(shè)計(jì)了一種毛刺檢測(cè)電路，并通過形式驗(yàn)證技術(shù)實(shí)現(xiàn)該檢測(cè)電路在RTL級(jí)對(duì)毛刺的檢測(cè)。

1.1 基于斷言的形式驗(yàn)證技術(shù)

本文在靜態(tài)時(shí)序分析結(jié)果的基礎(chǔ)上，采用基于斷言的形式驗(yàn)證技術(shù)，用自動(dòng)化的手段檢測(cè)組合邏輯毛刺。形式驗(yàn)證是窮盡式數(shù)學(xué)技術(shù)，能夠從算法上窮盡檢查所有可能隨時(shí)間變化的輸入值，而仿真是完全經(jīng)驗(yàn)主義的做法，驗(yàn)證人員通過反復(fù)實(shí)驗(yàn)試圖設(shè)計(jì)全面的測(cè)試輸入向量，要花相當(dāng)多的時(shí)間嘗試所有可能的組合，因此永遠(yuǎn)不會(huì)完整。形式驗(yàn)證沒有必要考慮如何設(shè)計(jì)激勵(lì)或創(chuàng)建多種條件來實(shí)現(xiàn)較高的覆蓋率和可控性，在RTL級(jí)測(cè)試覆蓋更加全面，檢測(cè)毛刺的可靠性優(yōu)于基于測(cè)試激勵(lì)的時(shí)序仿真。

1.2 毛刺產(chǎn)生電路分析

組合邏輯中，邏輯門輸入信號(hào)的路徑延時(shí)不同，到達(dá)門的時(shí)間也不一致，可能導(dǎo)致電路輸出信號(hào)中出現(xiàn)“毛刺”。布爾表達(dá)式由3種類型的基本布爾邏輯門組成：?jiǎn)屋斎敕聪嗥?，雙輸入與門和雙輸入或門。對(duì)于反相器，僅有一個(gè)輸入，不會(huì)發(fā)生競(jìng)爭(zhēng)冒險(xiǎn)帶來毛刺，所以本文僅分析邏輯與門和邏輯或門毛刺的產(chǎn)生情況：

(1)邏輯與門：邏輯與門如圖1所示，a和b在產(chǎn)生競(jìng)爭(zhēng)冒險(xiǎn)時(shí)才會(huì)產(chǎn)生毛刺，與門的輸入與毛刺的關(guān)系真值見表1。

圖1 邏輯與門

由表1可知，僅當(dāng)a與b同時(shí)變化，且輸入值相反時(shí)，輸出c端可能因邏輯門延時(shí)不同產(chǎn)生毛刺，邏輯與門毛刺產(chǎn)生時(shí)序如圖2所示。

(2)邏輯或門：邏輯或門如圖3所示，a和b在產(chǎn)生競(jìng)爭(zhēng)冒險(xiǎn)時(shí)才會(huì)產(chǎn)生毛刺，或門的輸入與毛刺的關(guān)系真值見表2。

表1 邏輯與門產(chǎn)生毛刺的情況

圖2 邏輯與門產(chǎn)生毛刺時(shí)序

圖3 邏輯或門

表2 邏輯或門產(chǎn)生毛刺的情況

由表2可知，僅當(dāng)a與b同時(shí)變化，且輸入值相反時(shí)，輸出c端可能因邏輯門延時(shí)不同產(chǎn)生毛刺，邏輯或門毛刺產(chǎn)生時(shí)序如圖4所示。

圖4 邏輯或門產(chǎn)生毛刺時(shí)序

根據(jù)上面對(duì)組合邏輯毛刺電路分析可知，在與門和或門輸入端，兩路輸入信號(hào)同時(shí)變化，且輸入值相反時(shí)，才可能產(chǎn)生毛刺，其它輸入情況不會(huì)引起電路毛刺。

1.3 毛刺檢測(cè)方法

由以上分析可知，在時(shí)序仿真時(shí)才能發(fā)現(xiàn)的毛刺，在RTL級(jí)，可以通過驗(yàn)證與門和或門的a、b兩路輸入是否同時(shí)產(chǎn)生反向的變化來判斷。在此基礎(chǔ)上，本文初步設(shè)計(jì)的檢測(cè)電路如圖5方框中所示。設(shè)計(jì)思路為：當(dāng)a信號(hào)發(fā)生變化時(shí)(a!=past(a))，b信號(hào)也發(fā)生變化(b!=past(b))，并且a與b的值不同(a!=b)，當(dāng)這3個(gè)條件同時(shí)成立時(shí)，電路會(huì)產(chǎn)生毛刺。所以檢測(cè)電路中將a與a的上一周期的值進(jìn)行異或，發(fā)生變化時(shí)，輸出結(jié)果為1，同理將b與b的上一周期的值進(jìn)行異或，同時(shí)，將a與b的值異或，如果a與b不同，輸出結(jié)果為1，將3個(gè)結(jié)果進(jìn)行與運(yùn)算，表明當(dāng)這3個(gè)條件同時(shí)發(fā)生時(shí)，輸出結(jié)果為1。RTL級(jí)的行為，可以用形式驗(yàn)證的方法描述，在形式檢驗(yàn)中，設(shè)計(jì)規(guī)范的描述被稱為電路的屬性(property)，采用基于斷言的驗(yàn)證(assertion based verification，ABV)方法就是指采用斷言描述電路屬性，用斷言描述上述屬性為：

Propertyglitch_Detection_1;

@(posedge clk)

(a!=$past(a))|->(b!=$past(b))&& (a!=b);

Endproperty

根據(jù)以上斷言描述，當(dāng)a與b同時(shí)、反向變化時(shí)，屬性為真，提示“通過”，但是實(shí)際驗(yàn)證中，當(dāng)a保持不變的情況下，無法觸發(fā)進(jìn)入屬性判斷的條件，也會(huì)提示“通過”，稱之為假通過。所以在設(shè)計(jì)中，還需考慮如何排除假通過的情況。文獻(xiàn)[4]中介紹了專門檢測(cè)信號(hào)保持不變的斷言描述，如果將信號(hào)保持?jǐn)嘌院蜕鲜雒虣z測(cè)斷言結(jié)合檢測(cè)毛刺，則需要用兩個(gè)斷言來檢測(cè)毛刺，過于復(fù)雜。因此，本文的方法為在初步設(shè)計(jì)的毛刺檢測(cè)電路的輸出端增加一個(gè)反相器，如圖5所示。

圖5 毛刺檢測(cè)電路設(shè)計(jì)

用斷言描述圖5屬性為：

property glitch_Detection_2;

@(posedge clk)

(a!=$past(a))|->!((b!=$past(b))&& (a!=b));

Endproperty

即等價(jià)于：

property glitch_Detection_2;

@(posedge clk)

(a!=$past(a))|->(b==$past(b))|| (a==b);

Endproperty

含義為：①當(dāng)a發(fā)生變化時(shí)，如果b保持不變或者a等于b，不會(huì)產(chǎn)生毛刺，該屬性“通過”；②當(dāng)a發(fā)生變化時(shí)，如果b不屬于上一條的情況，即為產(chǎn)生毛刺的情況，該屬性“不通過”；③當(dāng)a保持不變時(shí)，該屬性“通過”。這樣就把產(chǎn)生毛刺的情況單獨(dú)分為一類，即“不通過”。形式驗(yàn)證可以根據(jù)設(shè)計(jì)意圖遍歷所有的輸入情況，在組合邏輯與或門處插入上述斷言，可以檢測(cè)毛刺的產(chǎn)生，當(dāng)斷言不通過時(shí)毛刺可能產(chǎn)生。

2 基于毛刺檢測(cè)電路的故障分析

SoC設(shè)計(jì)時(shí)，會(huì)盡力避免組合邏輯做寄存器的reset、clear、clock、gate端，雖然寄存器的輸入端對(duì)毛刺并不敏感，但是當(dāng)毛刺出現(xiàn)在時(shí)鐘沿并且影響到數(shù)據(jù)的建立時(shí)間和保持時(shí)間時(shí)，也會(huì)導(dǎo)致寄存器輸出錯(cuò)誤，所以本節(jié)重點(diǎn)研究毛刺在時(shí)序電路中的故障注入。為有效驗(yàn)證毛刺影響，本節(jié)首先描述毛刺在時(shí)序電路RTL級(jí)產(chǎn)生功能錯(cuò)誤的原因，然后基于RTL級(jí)毛刺檢測(cè)電路，描述毛刺現(xiàn)象的等價(jià)電路，分析毛刺故障的傳播模型和評(píng)價(jià)方法，用于驗(yàn)證毛刺故障注入電路的有效性。

2.1 毛刺功能錯(cuò)誤分析

在時(shí)序電路中，如果毛刺發(fā)生在目的寄存器的時(shí)鐘沿，并且影響到了數(shù)據(jù)的建立保持時(shí)間，則可能造成輸出的亞穩(wěn)態(tài)或采樣錯(cuò)誤。文獻(xiàn)[1]分析了亞穩(wěn)態(tài)現(xiàn)象和影響，在此基礎(chǔ)上，本文分析毛刺在時(shí)序電路的影響。如圖6所示，R1為CLKA時(shí)鐘域信號(hào)組合邏輯產(chǎn)生的毛刺信號(hào)，被CLKB時(shí)鐘域的寄存器采樣。由于CLKA和CLKB是異步時(shí)鐘，R1可能發(fā)生在CLKB時(shí)鐘域寄存器的建立時(shí)間或保持時(shí)間內(nèi)。如果R1影響CLKB時(shí)鐘域寄存器的建立和保持時(shí)間，則CLKB時(shí)鐘域寄存器將進(jìn)入亞穩(wěn)定狀態(tài)[5]。雖然亞穩(wěn)態(tài)時(shí)CLKB時(shí)鐘域寄存器的輸出信號(hào)R2最終會(huì)穩(wěn)定到邏輯0或邏輯1，但結(jié)果不可預(yù)測(cè)，毛刺對(duì)目的時(shí)鐘域的影響為一個(gè)或者兩個(gè)時(shí)鐘周期[6]，最終穩(wěn)定到正確值。如果毛刺被采樣(表現(xiàn)為cycle2的一個(gè)單脈沖或cycle3的一個(gè)單脈沖，不考慮亞穩(wěn)態(tài)更多影響周期的情況)，則會(huì)在時(shí)序電路傳播，可能導(dǎo)致電路功能錯(cuò)誤。

2.2 毛刺故障等價(jià)電路

文獻(xiàn)[1]設(shè)計(jì)了亞穩(wěn)態(tài)的等價(jià)電路，需要由外部的Sel信號(hào)控制發(fā)生亞穩(wěn)態(tài)的時(shí)刻。本文根據(jù)1節(jié)毛刺檢測(cè)電路和2.1節(jié)毛刺在時(shí)序電路影響分析，設(shè)計(jì)了一種RTL級(jí)毛刺故障等價(jià)電路，在RTL級(jí)用目的時(shí)鐘域的單脈沖模擬毛刺引起的故障，該故障等價(jià)電路融合了毛刺檢測(cè)電路，故障注入時(shí)刻與真實(shí)毛刺發(fā)生時(shí)刻一致。

圖6 毛刺在時(shí)序邏輯影響

相同時(shí)鐘下與門毛刺故障等價(jià)電路如圖7所示，該電路由原電路A、毛刺檢測(cè)電路D(取反)、毛刺采樣電路S和毛刺注入電路M組成，等價(jià)電路中各個(gè)信號(hào)時(shí)序關(guān)系如圖8所示，與門存在競(jìng)爭(zhēng)冒險(xiǎn)產(chǎn)生毛刺時(shí)，輸出R2為cycle1的一個(gè)CLK周期單脈沖，輸出R3為cycle2的一個(gè)CLK周期單脈沖，模擬毛刺被采樣的情況。將毛刺引起的單脈沖R2、R3與原電路A做或操作(out1和out2分別表示兩種錯(cuò)誤情況)，即可模擬原電路產(chǎn)生毛刺故障影響的情況。

圖7 相同時(shí)鐘下毛刺故障等價(jià)電路

圖8 故障等價(jià)電路時(shí)序關(guān)系

當(dāng)邏輯與門輸出被另外一個(gè)時(shí)鐘域采樣，根據(jù)目的時(shí)鐘域時(shí)鐘與源時(shí)鐘域時(shí)鐘的關(guān)系，更改毛刺采樣電路S的設(shè)計(jì)即可；同時(shí)，邏輯或門毛刺故障等價(jià)電路可以通過更改毛刺注入電路M完成。

2.3 故障傳播模型

毛刺故障產(chǎn)生錯(cuò)誤的采樣后，在時(shí)序電路中傳播，圖9數(shù)據(jù)傳播流圖表示毛刺故障傳播路徑的一種情況，b代表起始點(diǎn)，為故障注入點(diǎn)，o代表可觀點(diǎn)。如果R2受故障影響時(shí)，XCS保持為0，那R的毛刺故障就無法傳播到o，因此并不是所有b點(diǎn)的故障都能傳播到可觀點(diǎn)，在可觀察的情況下評(píng)估毛刺故障才有意義。

圖9 數(shù)據(jù)傳播流圖

下面分類討論時(shí)序邏輯中組合邏輯對(duì)毛刺故障傳播的影響，組合邏輯下的毛刺故障傳播是類似文獻(xiàn)[7]中描述的標(biāo)簽?zāi)M算法。

(1)邏輯門：

對(duì)于反相器，毛刺故障狀態(tài)將從輸入到輸出直接傳播。對(duì)于與門，從一個(gè)輸入毛刺故障傳播到輸出的條件為其它輸入為1。對(duì)于或門，從一個(gè)輸入毛刺故障傳播到輸出的條件為其它輸入為0。

(2)算術(shù)運(yùn)算符：

考慮一個(gè)表達(dá)式v(F)=v(A)v(B)。A和B是算術(shù)運(yùn)算符op的操作數(shù)，F(xiàn)是計(jì)算的結(jié)果。令v(AORI)表示原始值和v(AGLI)表示毛刺的值故障。然后計(jì)算v(FORI)=v(AORI)v(B)和v(FGLI)=v(AGLI)v(B)，當(dāng)v(FORI)≠v(FCDC)時(shí)，毛刺從A傳播到F。

(3)條件：

考慮以下條件邏輯：

if (F)

Out<=A;

else

Out<=B;

如果條件控制變量F發(fā)生毛刺故障，可能導(dǎo)致錯(cuò)誤的分支。所以當(dāng)A≠B時(shí)，毛刺故障從F到Out有效。如果條件輸入變量A具有毛刺故障，如果F為真，毛刺故障將傳播到Out[8]。

基于以上分析，可以通過計(jì)算毛刺故障對(duì)可視點(diǎn)的覆蓋評(píng)估毛刺故障傳播的影響[9]。

(1)毛刺故障起始點(diǎn)

使用CPf(v)來表示毛刺故障起始頂點(diǎn)。它被遞歸地定義為

對(duì)于起始頂點(diǎn)b∈B，插入毛刺故障并且沒有前向頂點(diǎn)。

(2)監(jiān)控值

對(duì)于可觀察的頂點(diǎn)o∈O，用形式驗(yàn)證監(jiān)控O的值，使用Value(o)來呈現(xiàn)一組監(jiān)視器頂點(diǎn)O值。

(3)毛刺故障覆蓋點(diǎn)

CovGLI(O)表示所有可觀毛刺故障覆蓋點(diǎn)?？捎^察頂點(diǎn)

其中，oj∈O，n=|O|，wjk∈Pre(oj)，m=|Pre(oj)|。

毛刺故障RTL級(jí)評(píng)估為毛刺故障覆蓋點(diǎn)占所有可觀測(cè)點(diǎn)的比例[10]。

3 實(shí)驗(yàn)驗(yàn)證

本文選用商業(yè)IP核ATA-5 IDE控制器作為實(shí)驗(yàn)用例，它包含一個(gè)異步FIFO用以實(shí)現(xiàn)AMBA AHB時(shí)鐘域數(shù)據(jù)到IDE時(shí)鐘域的數(shù)據(jù)傳輸，并選用Cadence公司的Jasper形式化驗(yàn)證工具做結(jié)果監(jiān)控，使用SystemVerilog斷言實(shí)現(xiàn)定義電路特性，采用形式驗(yàn)證的方法，可以避免測(cè)試向量不完整導(dǎo)致的毛刺故障難以檢測(cè)問題。為了保證RTL級(jí)行為正確，使用AMBA VIP監(jiān)控器和IDE設(shè)備監(jiān)視器，以確保AHB和IDE接口正確。整個(gè)IP核可能存在毛刺的有5個(gè)層次結(jié)構(gòu)模型：異步FIFO，異步FIFO控制，IDE時(shí)序控制和AMBA AHB DMA控制。把毛刺檢測(cè)電路用形式驗(yàn)證的斷言描述并插入到檢測(cè)點(diǎn)：

property glitch_Detection_2(a,b);

@(posedge clk)

(a!=$past(a))|->!((b!=$past(b))&& (a!=b));

Endproperty

Sig_T:assert property(glitch_Detection_2(T1,T2));

……

根據(jù)形式驗(yàn)證工具報(bào)出的不通過，篩選出可能發(fā)生毛刺的組合邏輯，驗(yàn)證了毛刺檢測(cè)電路有效性。

將毛刺故障等價(jià)電路插入到檢測(cè)出的發(fā)生毛刺的組合邏輯中，同時(shí)進(jìn)行形式化驗(yàn)證監(jiān)控。毛刺故障覆蓋被定義為所有監(jiān)控點(diǎn)中受毛刺故障影響的點(diǎn)。表3顯示了5個(gè)層次結(jié)構(gòu)電路中，毛刺故障覆蓋情況。實(shí)驗(yàn)中發(fā)現(xiàn)一個(gè)由于毛刺故障引起的功能錯(cuò)誤，在UDMA讀時(shí)序中，F(xiàn)IFO指針的毛刺故障會(huì)傳播給NIOR，具有毛刺故障的FIFO指針會(huì)誘發(fā)一個(gè)FIFO滿信號(hào)在錯(cuò)誤的時(shí)候有效，導(dǎo)致讀時(shí)序異常，違背了設(shè)計(jì)師的意圖。

表3 毛刺故障覆蓋率

毛刺故障覆蓋率不是100%說明在起始頂點(diǎn)的毛刺故障并沒有全部傳播到監(jiān)控頂點(diǎn)。

4 結(jié)束語(yǔ)

在本文中，介紹了毛刺檢測(cè)技術(shù)及毛刺故障注入。首先基于形式驗(yàn)證技術(shù)，設(shè)計(jì)了一種在RTL級(jí)檢測(cè)毛刺的電路及方法，該方法不需要控制信號(hào)，自動(dòng)檢測(cè)毛刺，并排除了信號(hào)保持不變，假通過的情況。其次，提出一種毛刺在時(shí)序電路傳播的故障模型和故障等價(jià)電路，該毛刺故障等價(jià)電路不需要控制信號(hào)，可在毛刺發(fā)生時(shí)刻自動(dòng)注入。最后，通過對(duì)故障傳播模型的建立和研究，采用形式驗(yàn)證的方法，實(shí)驗(yàn)結(jié)果驗(yàn)證了毛刺檢測(cè)方法和等價(jià)電路的有效性。本文提出的毛刺檢測(cè)及故障注入方法，能夠幫助驗(yàn)證人員在RTL級(jí)對(duì)毛刺故障做更多的驗(yàn)證工作，提早發(fā)現(xiàn)驗(yàn)證后期才可能發(fā)現(xiàn)的錯(cuò)誤。