邏輯錐Logic Cone

從數(shù)字網(wǎng)表的角度來看，可以把設(shè)計(jì)分成若干個(gè)“以DFF為終點(diǎn)的邏輯塊”，如下圖。DFF的CK（時(shí)鐘）、Ｄ（數(shù)據(jù)）、RN（復(fù)位）、SN（置位）就是這個(gè)“邏輯塊”的終點(diǎn)，它們的輸入都是一個(gè)組合邏輯。時(shí)鐘和復(fù)位很可能是clock tree或者buffer tree，也可能有與門、或門、異或門、選擇器等稍復(fù)雜的邏輯。

（圖一）

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

（圖二）

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

（圖三）

那跨模塊優(yōu)化的又是什么情況呢？如下圖，組合邏輯分到了兩個(gè)模塊里。但如果忽略設(shè)計(jì)的層次關(guān)系，兩段組合邏輯可以合并成一段。好處是：綜合工具可以兩段組合邏輯一起考慮，看有沒有邏輯可以復(fù)用，所以面積和時(shí)序會(huì)優(yōu)化得更好。壞處是：模塊的端口可能不存了，也可能產(chǎn)生了新的端口。所以綜合和LEC的選項(xiàng)ungroup（flatten）就是這個(gè)作用，讓工具忽略層次關(guān)系。

（圖四）

因此，設(shè)計(jì)（module）就是“以DFF為終點(diǎn)的邏輯塊”組成。不僅網(wǎng)表如此，RTL也是一樣。我們知道所有數(shù)字電路都可以用always和assign這兩種語法來實(shí)現(xiàn)（latch可以看作是DFF的一種）。這些“以DFF為終點(diǎn)的邏輯塊”我們把它叫作邏輯錐。

Keypoint Mapping

有了邏輯錐的概念后，關(guān)鍵點(diǎn)映射（keypoint mapping）就好理解多了。從上文知道邏輯錐的終點(diǎn)是DFF的CK（時(shí)鐘）、Ｄ（數(shù)據(jù)）、RN（復(fù)位）、SN（置位），如果這幾個(gè)“關(guān)鍵點(diǎn)”的邏輯都相同或者等價(jià)，那么這兩個(gè)邏輯錐的邏輯就等價(jià)。對于組合邏輯直接輸出的邏輯錐來說，“關(guān)鍵點(diǎn)”就是output pin。那么，總結(jié)一下“關(guān)鍵點(diǎn)”有以下幾種：DFF的輸入（CK、Ｄ、RN、SN）頂層模塊的輸出pin
要檢查等價(jià)性，那么keypoing mapping是前提，是基礎(chǔ)。如果keypoing mapping都錯(cuò)了，等價(jià)性檢查結(jié)果一定Fail。

對于要對比的兩個(gè)設(shè)計(jì)，我們通常叫作golden和revised（S家叫reference和implement）。golden可能是RTL、綜合網(wǎng)表，也可能是APR網(wǎng)表，ECO網(wǎng)表，不是絕對的，只是表明以此設(shè)計(jì)作為基準(zhǔn)來對比。所以在做等價(jià)性檢查時(shí)golden和revised弄反了也問題不大。但是S家的工具依賴svf（setup verification file），所以還是要注意一下。

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

新加DFF刪掉DFFDFF改名

復(fù)位變成置位上升沿變下降沿還可能DFF從模塊A挪到模塊B寄存器合并寄存器復(fù)制multi bit寄存器

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

形式驗(yàn)證

在關(guān)鍵點(diǎn)（keypoint）映射正確后，就可以開始做形式驗(yàn)證了。如果邏輯錐的輸入不一致，例如下圖中修改后的設(shè)計(jì)中增加了輸入4和5，就需要分析這兩個(gè)新增加的輸入是不是與golden的輸入是等價(jià)或者反相等價(jià)的關(guān)系。如果沒有任何關(guān)系，純粹是新加的條件，那么這兩個(gè)邏輯錐一定會(huì)fail。

（圖五）

經(jīng)過上一步對邏輯錐輸入的檢查后，接下來就需要通過數(shù)學(xué)的方法來檢查等價(jià)性。這種數(shù)學(xué)的方法的原理很簡單，如下，每個(gè)keypoint的邏輯都可以用下面的公式來描述：Y ＝ F（a， b， c， ．．． ， n）

對golden和revised邏輯錐施加相同的測試向量，看是否有相同的輸入。理論上，對于有N個(gè)輸入的keypoing，一共有2＾N種輸入可能性。遍歷一下，就知道等價(jià)性的結(jié)果。

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

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