[發(fā)明專利]集成電路驗(yàn)證方法及其系統(tǒng)

有效

• 申請(qǐng)?zhí)枺?/td>: 200910244172.2
• 申請(qǐng)日: 2009-12-30
• 公開（公告）號(hào): CN101794330A
• 公開（公告）日: 2010-08-04
• 發(fā)明（設(shè)計(jì)）人: 張弢;呂濤;李曉維
• 申請(qǐng)（專利權(quán)）人: 中國科學(xué)院計(jì)算技術(shù)研究所
• 主分類號(hào): G06F17/50
• 分類號(hào): G06F17/50
• 代理公司: 北京律誠同業(yè)知識(shí)產(chǎn)權(quán)代理有限公司 11006
• 代理人: 祁建國;梁揮

1.一種集成電路驗(yàn)證方法，其特征在于，包括：

步驟1，抽象引擎對(duì)待驗(yàn)證的集成電路進(jìn)行抽象，生成對(duì)應(yīng)的抽象模型， 并且在所述抽象模型上進(jìn)行形式化計(jì)算，以獲得形式化信息；

步驟2，激勵(lì)生成引擎初始化根據(jù)待驗(yàn)證的集成電路的規(guī)范建立的馬爾可 夫模型；

步驟3，激勵(lì)生成引擎由馬爾可夫模型生成激勵(lì)，將所述激勵(lì)輸入仿真器， 所述仿真器對(duì)所述待驗(yàn)證的集成電路進(jìn)行仿真；

步驟4，所述激勵(lì)生成引擎依據(jù)所述形式化信息比較本周期仿真結(jié)果和上 周期仿真獲得的仿真結(jié)果，如果本周期仿真結(jié)果更接近目標(biāo)狀態(tài)，則調(diào)整所述 馬爾可夫模型中參數(shù)；

步驟5，如果待驗(yàn)證的集成電路未達(dá)到目標(biāo)狀態(tài)并且仿真次數(shù)未超過預(yù)設(shè) 次數(shù)，則執(zhí)行所述步驟3；否則，終止仿真，并報(bào)告成功或者運(yùn)行超時(shí)。

2.根據(jù)權(quán)利要求1所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟1進(jìn)一步為，

步驟21，建立數(shù)據(jù)依賴圖；

步驟22，在所述數(shù)據(jù)依賴圖上進(jìn)行抽象，生成抽象模型；

步驟23，在所述抽象模型上進(jìn)行形式化計(jì)算，獲得形式化信息。

3.根據(jù)權(quán)利要求2所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟21進(jìn)一步為，

步驟31，根據(jù)待驗(yàn)證的集成電路的硬件描述語言的描述，依據(jù)存儲(chǔ)目標(biāo) 狀態(tài)的目標(biāo)狀態(tài)變量建立數(shù)據(jù)依賴圖；所述數(shù)據(jù)依賴圖中，每一個(gè)結(jié)點(diǎn)代表一 個(gè)寄存器變量，兩個(gè)結(jié)點(diǎn)之間的有向箭頭表示目標(biāo)結(jié)點(diǎn)對(duì)源結(jié)點(diǎn)存在數(shù)據(jù)依賴 關(guān)系。

4.根據(jù)權(quán)利要求3所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟22進(jìn)一步為，

步驟41，在所述數(shù)據(jù)依賴圖中，從目標(biāo)狀態(tài)變量出發(fā)，按照邏輯依賴關(guān) 系由近及遠(yuǎn)的回溯，并采用廣度優(yōu)先搜索方式將遍歷到的寄存器變量加入到抽 象模型；如果兩個(gè)存在依賴關(guān)系的寄存器變量被加入到所述抽象模型中，則兩 個(gè)所述寄存器變量之間的組合邏輯也被加入到所述抽象模型中。

5.根據(jù)權(quán)利要求3所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟22進(jìn)一步為，

步驟51，在所述數(shù)據(jù)依賴圖中，將所述目標(biāo)狀態(tài)變量劃分為組，從各個(gè) 組的目標(biāo)狀態(tài)變量出發(fā)，按照邏輯依賴關(guān)系由近及遠(yuǎn)的回溯，并采用廣度優(yōu)先 搜索方式將遍歷到的寄存器變量加入到抽象模型的對(duì)應(yīng)子抽象模型中；如果兩 個(gè)存在依賴關(guān)系的寄存器變量被加入到所述子抽象模型中，則兩個(gè)所述寄存器 變量之間的組合邏輯也被加入到所述子抽象模型中。

6.根據(jù)權(quán)利要求2所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟23進(jìn)一步為，

步驟61，采用基于二分決策圖的形式化計(jì)算工具在所述抽象模型上進(jìn)行 形式化計(jì)算，獲得形式化信息，將所述形式化信息記錄到抽象距離信息表中， 所述形式化信息包括抽象狀態(tài)和抽象狀態(tài)對(duì)應(yīng)的抽象距離。

7.根據(jù)權(quán)利要求5所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟23進(jìn)一步為，

步驟71，采用基于二分決策圖的形式化計(jì)算工具在每個(gè)所述子抽象模型 上進(jìn)行形式化計(jì)算，獲得形式化信息，將所述形式化信息記錄到所述子抽象模 型對(duì)應(yīng)的抽象距離信息表中，所述形式化信息包括抽象狀態(tài)和抽象狀態(tài)對(duì)應(yīng)的 抽象距離。

8.根據(jù)權(quán)利要求1所述的集成電路驗(yàn)證方法，其特征在于，

所述步驟3進(jìn)一步為，

步驟81，所述激勵(lì)生成引擎在仿真的每一周期之前，根據(jù)馬爾可夫模型 的當(dāng)前配置生成一個(gè)周期的激勵(lì)，并提供給仿真器進(jìn)行仿真。