[發明專利]多輸出實例的CNF生成方法、等價性驗證方法、存儲介質

在審

• 申請號: 202111517843.5
• 申請日: 2021-12-13
• 公開（公告）號: CN114398847A
• 公開（公告）日: 2022-04-26
• 發明（設計）人: 熊繁華;劉美華;張巖;黃國勇;金玉豐;白耿
• 申請（專利權）人: 國微集團（深圳）有限公司
• 主分類號: G06F30/33
• 分類號: G06F30/33
• 代理公司: 深圳市康弘知識產權代理有限公司 44247
• 代理人: 尹彥

本發明公開了一種多輸出實例的CNF生成方法、等價性驗證方法、存儲介質。其中多輸出實例的CNF生成方法，包括：遍歷時，在存儲結構中查找當前的端口net的輸入端口net對應的CNF；如果沒找到，則計算當前的端口net的引用次數，遍歷當前的端口net連接的電路生成對應的CNF，將該CNF以及引用次數綁定后存入所述存儲結構；如果找到，則直接從所述存儲結構中調用所述CNF，并將引用次數減1，并在引用次數為0時，從所述存儲結構中刪除對應的CNF及其關聯數據。本發明可以減少CNF的存儲內存，并且縮短CNF的計算時間。

技術領域

本發明涉及數字電路的等價性驗證技術領域，尤其涉及一種多輸出實例的CNF生成方法、基于SAT的等價性驗證方法。

背景技術

在數字電路的等價性檢查中，基于SAT（satisfiability，布爾可滿足性問題）的等價性驗證方法被經常使用，一般布爾可滿足性問題的布爾公式都表示成合取范式(conjunctive normal from，CNF)的形式。在電路的等價性檢查中，可以將兩個設計電路的結構用合取范式的形式表現,再利用高效的SAT求解器對CNF進行求解，得到電路是否等價的結論。

現有技術中求得單輸出的實例CNF的方法較多，但電路中存在多輸出實例，現有求得CNF的方法存在耗時久，內存大的問題。由于多輸出實例有多個輸出端口，則同一個多輸出實例根據輸出端口的不同會得到多個不同的CNF，而同一個實例所連接的電路是一樣的，對不同的端口進行迭代會重復迭代同一電路，從而導致耗時久，生成CNF多，內存增大。

發明內容

為了解決現有技術中多輸出實例的CNF生成時太過于耗時、占用內存大的技術問題，本發明提出了多輸出實例的CNF生成方法、等價性驗證方法、存儲介質。

本發明提出的多輸出實例的CNF生成方法，包括：

遍歷時，在存儲結構中查找當前的端口net的輸入端口net對應的CNF；

如果沒找到，則計算當前的端口net的引用次數，遍歷當前的端口net連接的電路生成對應的CNF，若引用次數大于1，將該CNF以及引用次數綁定后存入所述存儲結構；否則將該CNF與其他端口的CNF組合；

如果找到，則直接從所述存儲結構中調用所述CNF與其他端口的CNF組合，并將引用次數減1，并在引用次數為0時，從所述存儲結構中刪除對應的CNF及其關聯數據。

進一步，所述存儲結構為哈希表。

進一步，當引用次數為0時，從所述哈希表中刪除所述CNF及其對應的節點。

進一步，所述當前的端口net的引用次數為該端口net連接的實例的輸出端口數量的總和。

本發明提出的基于SAT的等價性驗證方法，采用上述技術方案所述的多輸出實例的CNF生成方法生成對應的CNF。

本發明提出的計算機可讀存儲介質，用于存儲計算機程序，其特征在于，所述計算機程序運行時執行上述技術方案所述的多輸出實例的CNF生成方法。

進一步，所述計算機可讀存儲介質包括堆棧，所述CNF存儲在堆棧上。

本發明提出的針對多輸出實例CNF的生成方法是通過實例的net的引用次數對迭代實例的次數進行控制，生成CNF后將net與CNF綁定，并在實例的net引用次數減為0后，將該實例所對應的CNF刪除以減少內存占用。本發明對多輸出的實例的輸入端口net（與端口連接的線）的引用進行計算，對其連接的所有實例的輸出端口數量和頂層模塊的輸出端口數量進行判斷，進而計算引用次數，并將CNF與引用次數綁定。當每次迭代到同一條端口net后，從哈希表中取出第一次迭代完后的存入哈希表的CNF，并可利用其計算多輸出實例的CNF，然后將其引用次數減1，直至引用次數為0后，將對應的CNF刪除。本發明利用實例的端口net的引用次數與CNF綁定和存儲重復引用CNF的哈希表來減少迭代重復次數，從而減小內存占用和縮短求得CNF時間的方法。