形式驗證 | LEC, CLP, LP-EC 的區別

• 2020 年 2 月 17 日
• 筆記

年近了，寫一些不需要動太多腦子的，前幾天有小夥伴問，做了LEC 之後為什麼還需要做LP-EC? 做了LP-EC 之後為什麼還需要做CLP? 這三者之間有什麼區別呢？

LEC 做最基本的邏輯等效性檢查，需要讀入兩個設計，兩組library. 起LEC 時可用如下命令，不同的option 對應不同的license. 其中sl4 是神器smart LEC 的license.

• lec -xl/-gxl/-lp/-lpgxl/-sl4

LP-EC 在LEC 的基礎上，需要讀入兩組power intent, 在讀power intent 時，如果revised 已經插入low power cell，而Golden 未插入low power cell, 則在golden 側read power intent 時需要加option "-insert_isolation". 相對於LEC, LP-EC 會比較兩個power intent 的一致性、會做low power aware 的邏輯等效檢查、會檢查低功耗cell 的控制訊號、會比較Retention rule 的一致性。對於普通的level shifter 不論是在LEC 還是LP-EC 都當做buffer 處理，如果設計里只插了level shifter 不做LP-EC 也可以。但是isolation 在上電跟下電狀態，輸出完全不同，所以必須要run LP-EC. 起工具時用命令：

• lec -lp/lpgxl

在設計的不同階段，LP-EC 要檢查的內容：

CLP 讀入一個設計、一個power intent, 做power intent 本身quality 檢查，並以power intent 為準則來check netlist 中low power cell 是否有多插、亂插、漏插，檢查netlist 的pg 連接是否符合power intent 的定義，檢查low power cell 的控制訊號是否有問題，起工具時用如下命令，option "-verify" 是必須要加的。

• lec -lp -verify

在設計的不同階段，CLP 檢查的內容：

由上述簡短描述可知，LEC, LP-EC, CLP 覆蓋設計的不同方面，只要是插了isolation 三個check 缺一不可。一個例子：

根據isolaiton rule的定義，X2/sA 是需要在下電後clamp 成高電平的，而其他訊號是需要clamp 成低電平的，但是在優化的過程中，X2/sA 跟X2/sB 被合併成了一個訊號X2/sA. 對於這樣的電路LEC 跟CLP 都是沒問題的，必需要run LP-EC 才能暴露出問題。

驢說IC