[發(fā)明專利]多輸出實(shí)例的CNF生成方法、等價(jià)性驗(yàn)證方法、存儲(chǔ)介質(zhì)

在審

• 申請?zhí)枺?/td>: 202111517843.5
• 申請日: 2021-12-13
• 公開（公告）號: CN114398847A
• 公開（公告）日: 2022-04-26
• 發(fā)明（設(shè)計(jì)）人: 熊繁華;劉美華;張巖;黃國勇;金玉豐;白耿
• 申請（專利權(quán)）人: 國微集團(tuán)（深圳）有限公司
• 主分類號: G06F30/33
• 分類號: G06F30/33
• 代理公司: 深圳市康弘知識產(chǎn)權(quán)代理有限公司 44247
• 代理人: 尹彥

1.一種多輸出實(shí)例的CNF生成方法，其特征在于，包括：

遍歷時(shí)，在存儲(chǔ)結(jié)構(gòu)中查找當(dāng)前的端口net的輸入端口net對應(yīng)的CNF；

如果沒找到，則計(jì)算當(dāng)前的端口net的引用次數(shù)，遍歷當(dāng)前的端口net連接的電路生成對應(yīng)的CNF，若引用次數(shù)大于1，將該CNF以及引用次數(shù)綁定后存入所述存儲(chǔ)結(jié)構(gòu)；否則將該CNF與其他端口的CNF組合；

如果找到，則直接從所述存儲(chǔ)結(jié)構(gòu)中調(diào)用所述CNF與其他端口的CNF組合，并將引用次數(shù)減1，并在引用次數(shù)為0時(shí)，從所述存儲(chǔ)結(jié)構(gòu)中刪除對應(yīng)的CNF及其關(guān)聯(lián)數(shù)據(jù)。

2.如權(quán)利要求1所述的多輸出實(shí)例的CNF生成方法，其特征在于，所述存儲(chǔ)結(jié)構(gòu)為哈希表。

3.如權(quán)利要求2所述的多輸出實(shí)例的CNF生成方法，其特征在于，當(dāng)引用次數(shù)為0時(shí)，從所述哈希表中刪除所述CNF及其對應(yīng)的節(jié)點(diǎn)。

4.如權(quán)利要求1所述的多輸出實(shí)例的CNF生成方法，其特征在于，所述當(dāng)前的端口net的引用次數(shù)為該端口net連接的實(shí)例的輸出端口數(shù)量的總和。

5.一種基于SAT的等價(jià)性驗(yàn)證方法，其特征在于，采用如權(quán)利要求1至4任意一項(xiàng)所述的多輸出實(shí)例的CNF生成方法生成對應(yīng)的CNF。

6.一種計(jì)算機(jī)可讀存儲(chǔ)介質(zhì)，用于存儲(chǔ)計(jì)算機(jī)程序，其特征在于，所述計(jì)算機(jī)程序運(yùn)行時(shí)執(zhí)行如權(quán)利要求1-4任意一項(xiàng)所述的多輸出實(shí)例的CNF生成方法。

7.如權(quán)利要求6所述的計(jì)算機(jī)可讀存儲(chǔ)介質(zhì)，其特征在于，所述計(jì)算機(jī)可讀存儲(chǔ)介質(zhì)包括堆棧，所述CNF存儲(chǔ)在堆棧上。