一種在LEC中識別斷點的獨特技術可解決中止問題

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

　　i)復雜的數(shù)據(jù)路徑;

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

　　iii)大量未關注的細節(jié)問題。

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

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

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

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