[發(fā)明專利]一種形式驗(yàn)證比較點(diǎn)匹配方法、系統(tǒng)、處理器及存儲(chǔ)器

有效

• 申請(qǐng)?zhí)枺?/td>: 202010632501.7
• 申請(qǐng)日: 2020-07-03
• 公開（公告）號(hào): CN111797588B
• 公開（公告）日: 2022-11-11
• 發(fā)明（設(shè)計(jì)）人: 張巖;劉美華;黃國(guó)勇;金玉豐
• 申請(qǐng)（專利權(quán)）人: 深圳國(guó)微芯科技有限公司
• 主分類號(hào): G06F30/398
• 分類號(hào): G06F30/398;G06F30/3312;G06F30/3323
• 代理公司: 深圳市康弘知識(shí)產(chǎn)權(quán)代理有限公司 44247
• 代理人: 吳敏

1.一種形式驗(yàn)證比較點(diǎn)匹配方法，包括：步驟S1:接收待驗(yàn)證的時(shí)序電路的參考電路模型和實(shí)現(xiàn)電路模型，其特征是，還包括：

步驟S2:控制參考電路模型和實(shí)現(xiàn)電路模型待匹配的比較點(diǎn)的測(cè)試向量隨機(jī)生成，使得參考電路模型和實(shí)現(xiàn)電路模型的比較點(diǎn)的輸出值可進(jìn)行二叉樹匹配，所述可進(jìn)行二叉樹匹配為使得參考電路模型的待匹配的比較點(diǎn)的輸出值之和以及實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)的輸出值之和為待匹配的比較點(diǎn)的數(shù)量的一半或待匹配的比較點(diǎn)的數(shù)量加一或減一后的一半；

根據(jù)參考電路模型的待匹配的比較點(diǎn)的輸出值以及實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)的輸出值將相同輸出值的比較點(diǎn)劃分為組，將當(dāng)前每一組中的比較點(diǎn)分別作為參考電路模型的待匹配的比較點(diǎn)以及實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)返回步驟S2繼續(xù)進(jìn)行匹配，直至每一組中作為的參考電路模型的待匹配的比較點(diǎn)或者實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)的數(shù)量小于2；

步驟S3：基于二叉樹匹配對(duì)參考電路模型的待匹配的各比較點(diǎn)的輸出值與實(shí)現(xiàn)電路模型的待匹配的各比較點(diǎn)的輸出值進(jìn)行匹配，直至參考電路模型和實(shí)現(xiàn)電路模型所有比較點(diǎn)全部一一匹配成功，則驗(yàn)證成功；若存在參考電路模型和實(shí)現(xiàn)電路模型待匹配的比較點(diǎn)匹配失敗，則驗(yàn)證失敗。

2.如權(quán)利要求1所述的形式驗(yàn)證比較點(diǎn)匹配方法，其特征是，控制參考電路模型和實(shí)現(xiàn)電路模型待匹配的比較點(diǎn)的測(cè)試向量隨機(jī)生成采用ATPG方法進(jìn)行控制，使參考電路模型的待匹配的比較點(diǎn)的輸出值之和或者實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)的輸出值之和等于待匹配的比較點(diǎn)的數(shù)量的一半或待匹配的比較點(diǎn)的數(shù)量加一或減一后的一半。

3.如權(quán)利要求1所述的形式驗(yàn)證比較點(diǎn)匹配方法，其特征是，所述步驟S2包括：

步驟S21，隨機(jī)生成參考電路模型和實(shí)現(xiàn)電路模型待匹配的比較點(diǎn)的測(cè)試向量；

步驟S22，將對(duì)應(yīng)的測(cè)試向量分別輸入至參考電路模型和實(shí)現(xiàn)電路模型，得到參考電路模型和實(shí)現(xiàn)電路模型待匹配的比較點(diǎn)的輸出值；

步驟S23，計(jì)算參考電路模型的待匹配的比較點(diǎn)的輸出值之和以及實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)的輸出值之和；

步驟S24，判斷參考電路模型的待匹配的比較點(diǎn)的輸出值之和或者實(shí)現(xiàn)電路模型的待匹配的比較點(diǎn)的輸出值之和是否等于待匹配的比較點(diǎn)的數(shù)量的一半或待匹配的比較點(diǎn)的數(shù)量加一或減一后的一半；

若否，則返回步驟S21直至參考電路模型和實(shí)現(xiàn)電路模型的比較點(diǎn)的輸出值可進(jìn)行二叉樹匹配。

4.如權(quán)利要求1所述的形式驗(yàn)證比較點(diǎn)匹配方法，其特征是，

所述參考電路模型或?qū)崿F(xiàn)電路模型第一次待匹配的比較點(diǎn)的數(shù)量為所述參考電路模型或?qū)崿F(xiàn)電路模型的總數(shù)的一半或者為總數(shù)加一或減一后的一半；

所述參考電路模型或?qū)崿F(xiàn)電路模型第n次待匹配的比較點(diǎn)的數(shù)量為上一次待匹配的比較點(diǎn)的數(shù)量的一半或者為上一次待匹配的比較點(diǎn)的數(shù)量加一或減一后的一半；直至當(dāng)前次待匹配的比較點(diǎn)的數(shù)量小于2，所述n＞1。

5.如權(quán)利要求1所述的形式驗(yàn)證比較點(diǎn)匹配方法，其特征是，所述參考電路模型或?qū)崿F(xiàn)電路模型待匹配的比較點(diǎn)的測(cè)試向量包括由外界輸入的基本輸入向量、和/或由各比較點(diǎn)的上一級(jí)比較點(diǎn)產(chǎn)生的偽主輸入向量，所述參考電路模型及實(shí)現(xiàn)電路模型的基本輸入向量相同，所述參考電路模型及實(shí)現(xiàn)電路模型的偽主輸入向量相同或不相同。

6.一種時(shí)序電路形式驗(yàn)證的比較點(diǎn)匹配系統(tǒng)，其特征是，采用權(quán)利要求1-5任一項(xiàng)所述的形式驗(yàn)證比較點(diǎn)匹配方法對(duì)時(shí)序電路進(jìn)行驗(yàn)證。

7.如權(quán)利要求6所述的時(shí)序電路形式驗(yàn)證的比較點(diǎn)匹配系統(tǒng)，其特征是，包括：

輸入模塊，用于接收所述參考電路模型和實(shí)現(xiàn)電路模型的輸入模塊；

測(cè)試向量搜索模塊，用于控制參考電路模型和實(shí)現(xiàn)電路模型待匹配的比較點(diǎn)的測(cè)試向量隨機(jī)生成，使得參考電路模型和實(shí)現(xiàn)電路模型的比較點(diǎn)的輸出值可進(jìn)行二叉樹匹配；

匹配模塊，用于基于二叉樹匹配對(duì)參考電路模型的待匹配的各比較點(diǎn)的輸出值與實(shí)現(xiàn)電路模型的待匹配的各比較點(diǎn)的輸出值進(jìn)行匹配，直至參考電路模型和實(shí)現(xiàn)電路模型所有比較點(diǎn)全部一一匹配成功。