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

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

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

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

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

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

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

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

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