基于形式驗證的毛刺檢測技術(shù)

朱秋巖，李東方

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

0 引 言

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

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

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

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

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

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

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

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

組合邏輯中，邏輯門輸入信號的路徑延時不同，到達門的時間也不一致，可能導致電路輸出信號中出現(xiàn)“毛刺”。布爾表達式由3種類型的基本布爾邏輯門組成：單輸入反相器，雙輸入與門和雙輸入或門。對于反相器，僅有一個輸入，不會發(fā)生競爭冒險帶來毛刺，所以本文僅分析邏輯與門和邏輯或門毛刺的產(chǎn)生情況：

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

圖1 邏輯與門

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

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

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

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

圖3 邏輯或門

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

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

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

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

1.3 毛刺檢測方法

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

Propertyglitch_Detection_1;

@(posedge clk)

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

Endproperty

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

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

用斷言描述圖5屬性為：

property glitch_Detection_2;

@(posedge clk)

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

Endproperty

即等價于：

property glitch_Detection_2;

@(posedge clk)

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

Endproperty

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

2 基于毛刺檢測電路的故障分析

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

2.1 毛刺功能錯誤分析

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

2.2 毛刺故障等價電路

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

圖6 毛刺在時序邏輯影響

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

圖7 相同時鐘下毛刺故障等價電路

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

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

2.3 故障傳播模型

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

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

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

(1)邏輯門：

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

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

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

(3)條件：

考慮以下條件邏輯：

if (F)

Out<=A;

else

Out<=B;

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

基于以上分析，可以通過計算毛刺故障對可視點的覆蓋評估毛刺故障傳播的影響[9]。

(1)毛刺故障起始點

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

對于起始頂點b∈B，插入毛刺故障并且沒有前向頂點。

(2)監(jiān)控值

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

(3)毛刺故障覆蓋點

CovGLI(O)表示所有可觀毛刺故障覆蓋點。可觀察頂點

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

毛刺故障RTL級評估為毛刺故障覆蓋點占所有可觀測點的比例[10]。

3 實驗驗證

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

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ù)形式驗證工具報出的不通過，篩選出可能發(fā)生毛刺的組合邏輯，驗證了毛刺檢測電路有效性。

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

表3 毛刺故障覆蓋率

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

4 結(jié)束語

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