邏輯等價性檢查（LEC）基礎(chǔ)知識介紹

邏輯錐Logic Cone

從數(shù)字網(wǎng)表的角度來看，可以把設(shè)計分成若干個“以DFF為終點(diǎn)的邏輯塊”，如下圖。

DFF的CK（時鐘）、Ｄ（數(shù)據(jù)）、RN（復(fù)位）、SN（置位）就是這個“邏輯塊”的終點(diǎn)，它們的輸入都是一個組合邏輯。

時鐘和復(fù)位很可能是clock tree或者buffer tree，也可能有與門、或門、異或門、選擇器等稍復(fù)雜的邏輯。

（圖一）

如果設(shè)計（module）是組合邏輯輸出，也可想象在設(shè)計外面有一個DFF，如下圖。

（圖二）

而這些組合邏輯的輸入是什么呢？不外乎兩種情況：一是，前一級DFF的輸出；二是，設(shè)計（module）的輸入pin。

（圖三）

那跨模塊優(yōu)化的又是什么情況呢？如下圖，組合邏輯分到了兩個模塊里。但如果忽略設(shè)計的層次關(guān)系，兩段組合邏輯可以合并成一段。

好處是：綜合工具可以兩段組合邏輯一起考慮，看有沒有邏輯可以復(fù)用，所以面積和時序會優(yōu)化得更好。壞處是：模塊的端口可能不存了，也可能產(chǎn)生了新的端口。

所以綜合和LEC的選項ungroup（flatten）就是這個作用，讓工具忽略層次關(guān)系。

（圖四）

因此，設(shè)計（module）就是“以DFF為終點(diǎn)的邏輯塊”組成。不僅網(wǎng)表如此，RTL也是一樣。

我們知道所有數(shù)字電路都可以用always和assign這兩種語法來實現(xiàn)（latch可以看作是DFF的一種）。

這些“以DFF為終點(diǎn)的邏輯塊”我們把它叫作邏輯錐。

Keypoint Mapping

有了邏輯錐的概念后，關(guān)鍵點(diǎn)映射（keypoint mapping）就好理解多了。

從上文知道邏輯錐的終點(diǎn)是DFF的CK（時鐘）、Ｄ（數(shù)據(jù)）、RN（復(fù)位）、SN（置位），如果這幾個“關(guān)鍵點(diǎn)”的邏輯都相同或者等價，那么這兩個邏輯錐的邏輯就等價。

對于組合邏輯直接輸出的邏輯錐來說，“關(guān)鍵點(diǎn)”就是output pin。那么，總結(jié)一下“關(guān)鍵點(diǎn)”有以下幾種：

DFF的輸入（CK、Ｄ、RN、SN）

頂層模塊的輸出pin

要檢查等價性，那么keypoing mapping是前提，是基礎(chǔ)。如果keypoing mapping都錯了，等價性檢查結(jié)果一定Fail。

對于要對比的兩個設(shè)計，我們通常叫作golden和revised（S家叫reference和implement）。golden可能是RTL、綜合網(wǎng)表，也可能是APR網(wǎng)表，ECO網(wǎng)表，不是絕對的，只是表明以此設(shè)計作為基準(zhǔn)來對比。

所以在做等價性檢查時golden和revised弄反了也問題不大。但是S家的工具依賴svf（setup verification file），所以還是要注意一下。

當(dāng)修改RTL或者網(wǎng)表ECO后，邏輯錐的“關(guān)鍵點(diǎn)”可能發(fā)生較大的變化，比如：

新加DFF

刪掉DFF

DFF改名

復(fù)位變成置位

上升沿變下降沿

還可能DFF從模塊A挪到模塊B

寄存器合并

寄存器復(fù)制

multi bit寄存器

所以，keypoint mapping時，要能夠考慮到這些情況。可以手工分析，也可以參考綜合的svf文件，還可以用一些算法來測試和分析。

形式驗證

在關(guān)鍵點(diǎn)（keypoint）映射正確后，就可以開始做形式驗證了。

如果邏輯錐的輸入不一致，例如下圖中修改后的設(shè)計中增加了輸入4和5，就需要分析這兩個新增加的輸入是不是與golden的輸入是等價或者反相等價的關(guān)系。

如果沒有任何關(guān)系，純粹是新加的條件，那么這兩個邏輯錐一定會fail。

（圖五）

經(jīng)過上一步對邏輯錐輸入的檢查后，接下來就需要通過數(shù)學(xué)的方法來檢查等價性。

這種數(shù)學(xué)的方法的原理很簡單，如下，每個keypoint的邏輯都可以用下面的公式來描述： Y =F(a, b, c, ... , n) 對golden和revised邏輯錐施加相同的測試向量，看是否有相同的輸入。

理論上，對于有N個輸入的keypoing，一共有2^N種輸入可能性。遍歷一下，就知道等價性的結(jié)果。

如果其中有一個測試向量fail，那么這個keypoint就不等價，剩余的測試向量也就沒有必要繼續(xù)。如果都pass，就需要遍歷完所有的測試向量。

為了節(jié)省測試時間，LEC工具需要對邏輯錐進(jìn)行優(yōu)化?，F(xiàn)在市場上已經(jīng)出現(xiàn)一些基于機(jī)器學(xué)習(xí)（Machine Learning）和深度學(xué)習(xí)（deep learning）的形式驗證算法的LEC工具。

審核編輯：劉清