基于形式驗證的毛刺檢測技術

朱秋巖，李東方

(北京計算機技術及應用研究所， 北京 100854)

0 引 言

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

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

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

1 毛刺檢測電路設計

本節首先分析毛刺產生機理，然后設計了一種毛刺檢測電路，并通過形式驗證技術實現該檢測電路在RTL級對毛刺的檢測。

1.1 基于斷言的形式驗證技術

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

1.2 毛刺產生電路分析

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

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

圖1 邏輯與門

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

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

表1 邏輯與門產生毛刺的情況

圖2 邏輯與門產生毛刺時序

圖3 邏輯或門

表2 邏輯或門產生毛刺的情況

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

圖4 邏輯或門產生毛刺時序

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

1.3 毛刺檢測方法

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

Propertyglitch_Detection_1;

@(posedge clk)

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

Endproperty

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

圖5 毛刺檢測電路設計

用斷言描述圖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發生變化時，如果b保持不變或者a等于b，不會產生毛刺，該屬性“通過”；②當a發生變化時，如果b不屬于上一條的情況，即為產生毛刺的情況，該屬性“不通過”；③當a保持不變時，該屬性“通過”。這樣就把產生毛刺的情況單獨分為一類，即“不通過”。形式驗證可以根據設計意圖遍歷所有的輸入情況，在組合邏輯與或門處插入上述斷言，可以檢測毛刺的產生，當斷言不通過時毛刺可能產生。

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

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

2.1 毛刺功能錯誤分析

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

2.2 毛刺故障等價電路

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

圖6 毛刺在時序邏輯影響

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

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

圖8 故障等價電路時序關系

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

2.3 故障傳播模型

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

圖9 數據傳播流圖

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

(1)邏輯門：

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

(2)算術運算符：

考慮一個表達式v(F)=v(A)v(B)。A和B是算術運算符op的操作數，F是計算的結果。令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發生毛刺故障，可能導致錯誤的分支。所以當A≠B時，毛刺故障從F到Out有效。如果條件輸入變量A具有毛刺故障，如果F為真，毛刺故障將傳播到Out[8]。

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

(1)毛刺故障起始點

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

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

(2)監控值

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

(3)毛刺故障覆蓋點

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

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

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

3 實驗驗證

本文選用商業IP核ATA-5 IDE控制器作為實驗用例，它包含一個異步FIFO用以實現AMBA AHB時鐘域數據到IDE時鐘域的數據傳輸，并選用Cadence公司的Jasper形式化驗證工具做結果監控，使用SystemVerilog斷言實現定義電路特性，采用形式驗證的方法，可以避免測試向量不完整導致的毛刺故障難以檢測問題。為了保證RTL級行為正確，使用AMBA VIP監控器和IDE設備監視器，以確保AHB和IDE接口正確。整個IP核可能存在毛刺的有5個層次結構模型：異步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));

……

根據形式驗證工具報出的不通過，篩選出可能發生毛刺的組合邏輯，驗證了毛刺檢測電路有效性。

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

表3 毛刺故障覆蓋率

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

4 結束語

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