一種在LEC中識別斷點(diǎn)的獨特技術(shù)可解決中止問(wèn)題

　　隨著(zhù)設計復雜度越來(lái)越高，其中也包含了復雜的數據結構，導致LEC中的中止數量增加，其主要原因在于邏輯等效性檢查(LEC)工具在處理復雜邏輯時(shí)存在的局限性。中止實(shí)際上是形式驗證工具無(wú)法解決的非確定性結果。其原因在于：

　　i)復雜的數據路徑;

　　ii)比較采用大型邏輯錐;

　　iii)大量未關(guān)注的細節問(wèn)題。

　　設計中的中止越多，LEC覆蓋率就越低，同時(shí)在設計中缺失某些非等效關(guān)系的可能性也越大。雖然有多種不同的技術(shù)能夠解決中止問(wèn)題，但是都涉及復雜的方法或需要許多手動(dòng)流程。始終要記住，任何應用的技術(shù)都需要具備較短的周轉時(shí)間、擁有最低的LEC覆蓋范圍損失并具有對設計者來(lái)說(shuō)非常友好的特性。

　　添加斷點(diǎn)是一種避免中止的首選方式，其優(yōu)勢在于不會(huì )出現LEC覆蓋范圍損失。雖然工具自身能夠在組合邏輯中的特定點(diǎn)上添加斷點(diǎn)，但是大多數時(shí)間里這些斷點(diǎn)的位置對設計沒(méi)有幫助。斷點(diǎn)的位置對于正確地進(jìn)行比較和避免出現任何錯誤的非等效關(guān)系說(shuō)是非常重要的。在層級結構中添加斷點(diǎn)實(shí)際上將有助于使相同的點(diǎn)出現在RTL和門(mén)級網(wǎng)表中。由于LEC分別處理比較元件的輸入和輸出，因此斷點(diǎn)的輸入將在LEC比較期間進(jìn)行驗證，并且添加多個(gè)斷點(diǎn)也不會(huì )導致任何問(wèn)題出現。另外，添加斷點(diǎn)會(huì )對數據路徑進(jìn)行分區，并允許工具減少數據錐，因此能夠解決中止問(wèn)題。

　　圖1(a)說(shuō)明了整個(gè)邏輯都在鎖存器(DFlop)輸入位置進(jìn)行比較的傳統方法。目前，隨著(zhù)組合邏輯不斷增加，以及采用復雜的算法對組合邏輯進(jìn)行重構，在RTL和門(mén)級網(wǎng)表比較的過(guò)程中可能會(huì )在比較點(diǎn)上出現中止。新的技術(shù)需要首先識別被中止的模塊，這可以通過(guò)運行扁平 LEC完成。一旦識別后，被中止模塊邊界輸入的引腳功能會(huì )通過(guò)關(guān)閉邊界反演和允許常數傳播經(jīng)過(guò)這些邊界輸入而被保留。允許常數傳播不僅會(huì )幫助減少和簡(jiǎn)化組合邏輯，還可以幫助在面積方面獲得更好的QoR。

　　如上圖1 (b) 中所示，在被中止模塊的邊界輸入中添加斷點(diǎn)，將大型組合云拆分為若干較小的部分。LEC將斷點(diǎn)的輸入作為比較點(diǎn)來(lái)處理，并允許輸出的矢量與其對應的比較點(diǎn)進(jìn)行比較?，F在，讓我們來(lái)比較圖1(a)和圖 1(b) 之間生成的矢量數量。