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

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

　　i)復雜的數據路徑;

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

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

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

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

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

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