邏輯錐Logic Cone

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

（圖一）

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

（圖二）

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

（圖三）

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

（圖四）

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

Keypoint Mapping

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

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

當修改RTL或者網表ECO后，邏輯錐的“關鍵點”可能發生較大的變化，比如：

新加DFF刪掉DFFDFF改名

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

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

形式驗證

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

（圖五）

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

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

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

為了節省測試時間，LEC工具需要對邏輯錐進行優化。現在市場上已經出現一些基于機器學習（Machine Learning）和深度學習（deep learning）的形式驗證算法的LEC工具。