[發明專利]一種形式驗證比較點匹配方法、系統、處理器及存儲器

有效

• 申請號: 202010632501.7
• 申請日: 2020-07-03
• 公開（公告）號: CN111797588B
• 公開（公告）日: 2022-11-11
• 發明（設計）人: 張巖;劉美華;黃國勇;金玉豐
• 申請（專利權）人: 深圳國微芯科技有限公司
• 主分類號: G06F30/398
• 分類號: G06F30/398;G06F30/3312;G06F30/3323
• 代理公司: 深圳市康弘知識產權代理有限公司 44247
• 代理人: 吳敏

本發明公開了一種形式驗證比較點匹配方法、系統、處理器及存儲器，該方法包括：接收待驗證的時序電路的參考電路模型和實現電路模型；控制參考電路模型和實現電路模型待匹配的比較點的測試向量隨機生成，使得參考電路模型和實現電路模型的比較點的輸出值可進行二叉樹匹配；基于二叉樹匹配對參考電路模型的待匹配的各比較點的輸出值與實現電路模型的待匹配的各比較點的輸出值進行匹配，直至參考電路模型和實現電路模型所有比較點全部一一匹配成功，則驗證成功；若存在參考電路模型和實現電路模型待匹配的比較點匹配失敗，則驗證失敗。本發明降低了時序電路等價檢驗過程中對應比較點的匹配復雜度，降低了匹配時間，降低了內存的消耗。

技術領域

本發明涉及時序電路的等價性驗證技術領域，特別是涉及識別和匹配兩個時序電路的對應比較點的一種形式驗證比較點匹配方法、系統、處理器及存儲器。

背景技術

組合等價檢驗是證明或反駁兩個電路設計的功能等價性的驗證方法。這種驗證方法特別適用于僅使用組合綜合技術進行優化的情況。兩個電路設計（一個稱為參考電路，另一個稱為實現電路）的對應組合塊可以使用組合形式技術進行比較和驗證。隨著電路設計的規模越來越大和越來越復雜，利用組合等價檢驗的驗證方法，從而提供快速的周轉驗證時間和完整的驗證，正迅速地在傳統的基于仿真的驗證方法上取得進展。

對于時序電路，應用組合等價檢驗的一個重要步驟是識別和匹配待驗證的兩個電路設計中的對應比較點。電路設計中的比較點是驗證期間的組合邏輯端點。比較點可以是輸出端口、寄存器、鎖存器或黑盒輸入引腳。商業驗證工具中的比較點匹配方法大致可分為兩類：非功能匹配的方法和功能匹配的方法。

非功能匹配的方法使用名稱或結構比較來匹配電路設計中的比較點。在大多數生產驗證流程中，比較點的很大一部分通常使用非功能匹配的方法進行匹配。由于設計轉換不保留信號名稱或顯著修改部分設計的電路結構，大量比較點通常不匹配。功能匹配的方法是唯一可行的自動方法，用于匹配剩余的比較點。

目前，大部分功能匹配的方法基于定點計算的精確方法，在每個時序電路的設計中給定N個存儲元件（鎖存器，寄存器等），就有N!個可能的組合來匹配它們。在最壞的情況下，所有這些精確地方法可能都必須枚舉所有的組合，這就使得比較點匹配的復雜度很高，致使計算時間長，內存占用大。

還有基于功能匹配的啟發式方法，通過在比較點之間建立不等價關系，然后通過使用不等價信息將最有可能等價的點分組成對，假設給定N個比較點，采用這種方法的計算復雜度是N-1，比精確計算的復雜度減小。但是，當比較點較多時，計算時間依舊會很長，同時存儲不等價信息占用的內存也會很大。

因此，如何設計一種能夠快速的識別和匹配待驗證的兩個電路設計中的對應比較點的匹配方法是業界亟待解決的技術問題。

發明內容

為了解決上述現有技術中識別和匹配待驗證的兩個電路設計中的對應比較點的時間長的技術問題，本發明提出一種形式驗證比較點匹配方法、系統、處理器及存儲器。

本發明首先提出一種形式驗證比較點匹配方法，包括：步驟S1:接收待驗證的時序電路的參考電路模型和實現電路模型，還包括：步驟S2:控制參考電路模型和實現電路模型待匹配的比較點的測試向量隨機生成，使得參考電路模型和實現電路模型的比較點的輸出值可進行二叉樹匹配；步驟S3：基于二叉樹匹配對參考電路模型的待匹配的各比較點的輸出值與實現電路模型的待匹配的各比較點的輸出值進行匹配，直至參考電路模型和實現電路模型所有比較點全部一一匹配成功，則驗證成功；若存在參考電路模型和實現電路模型待匹配的比較點匹配失敗，則驗證失敗。

在一實施方式中，控制參考電路模型和實現電路模型待匹配的比較點的測試向量隨機生成采用ATPG方法進行控制，使參考電路模型的待匹配的比較點的輸出值之和或者實現電路模型的待匹配的比較點的輸出值之和等于待匹配的比較點的數量的一半或待匹配的比較點的數量加一或減一后的一半。