[發(fā)明專利]用于使用下界距離來執(zhí)行抽象-精化的方法和裝置

有效

• 申請?zhí)枺?/td>: 200910207629.2
• 申請日: 2009-10-28
• 公開（公告）號: CN101794324A
• 公開（公告）日: 2010-08-04
• 發(fā)明（設(shè)計）人: I-H·穆恩
• 申請（專利權(quán)）人: 新思科技有限公司
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 北京市金杜律師事務(wù)所 11256
• 代理人: 王茂華;陳宇萱

技術(shù)領(lǐng)域

本公開一般地涉及電子設(shè)計自動化(EDA)。具體而言，本公 開涉及用于通過使用抽象-精化技術(shù)來驗(yàn)證電路設(shè)計的功能的方法和 裝置。

背景技術(shù)

半導(dǎo)體制作技術(shù)的發(fā)展已經(jīng)造成每半導(dǎo)體器件的晶體管數(shù)量 的急劇增加。晶體管計數(shù)的這一增加使得計算機(jī)架構(gòu)師能夠創(chuàng)建具 有急劇增加的設(shè)計復(fù)雜度的數(shù)字電路設(shè)計。因而，隨著數(shù)字電路設(shè) 計變得更復(fù)雜，也更多地涉及到為了驗(yàn)證它們的實(shí)施的正確性而需 要的工作。

為了驗(yàn)證電路設(shè)計的功能，電路設(shè)計驗(yàn)證團(tuán)隊(duì)通常執(zhí)行基于模 擬的驗(yàn)證方法、形式驗(yàn)證方法或者這二者的組合。在基于模擬的驗(yàn) 證期間，驗(yàn)證團(tuán)隊(duì)通常將隨機(jī)輸入激勵施加到待驗(yàn)證的電路設(shè)計 (CUV)以對CUV進(jìn)行模擬并且對來自模擬的響應(yīng)與預(yù)計的響應(yīng)進(jìn) 行比較。按照隨機(jī)輸入激勵對CUV進(jìn)行模擬在性質(zhì)上是概率性的并 且依賴于大量輸入向量以實(shí)現(xiàn)對CUV的行為的合理覆蓋。然而隨著 電路設(shè)計變得更復(fù)雜，隨機(jī)輸入激勵在覆蓋CUV的重要拐角情況時 變得不太有效。

在形式驗(yàn)證期間，驗(yàn)證團(tuán)隊(duì)通常嘗試證實(shí)或者反證CUV的功 能的正確性。形式驗(yàn)證通常涉及到構(gòu)造對CUV的正確功能進(jìn)行限定 的形式規(guī)范和/或性質(zhì)匯集、然后使用形式證據(jù)以確定CUV的實(shí)施是 否滿足形式規(guī)范和/或性質(zhì)匯集。然而，如果沒有使用具體技術(shù)以使 驗(yàn)證更高效，則形式規(guī)范可能計算成本高。

抽象-精化是這樣一種方式，該方式創(chuàng)建CUV的抽象數(shù)學(xué)模型 并且展開抽象模型直至滿足性質(zhì)或者為CUV發(fā)現(xiàn)反例。具體而言， 如果抽象-精化程序確定抽象模型滿足性質(zhì)，則它確定CUV也滿足 性質(zhì)。另一方面，如果抽象模型在功能上變得等效于CUV并且形式 驗(yàn)證技術(shù)發(fā)現(xiàn)反例，則抽象-精化程序確定CUV不滿足性質(zhì)。遺憾 的是，抽象-精化方式甚至可能計算成本高。因此，希望對使用抽象- 精化的形式驗(yàn)證技術(shù)的效率進(jìn)行改進(jìn)。

發(fā)明內(nèi)容

一些實(shí)施方式提供用于驗(yàn)證電路設(shè)計的功能的方法和裝置。具 體而言，一些實(shí)施方式通過確定使用抽象-精化的形式驗(yàn)證工具何時 可以避免執(zhí)行可達(dá)性分析來提高該形式驗(yàn)證工具的性能。

可以使用狀態(tài)變量集合來限定性質(zhì)，從而各狀態(tài)變量與CUV 中的順序要素相關(guān)聯(lián)。在兩個順序要素之間的路徑的長度可以至少 部分地基于路徑中的順序要素數(shù)量，從而在兩個狀態(tài)變量之間的距 離等于在與兩個狀態(tài)變量相關(guān)聯(lián)的兩個順序要素之間的最短路徑的 長度。

抽象模型的下界距離(LBD)可以定義如下。如果抽象模型包 含CUV中的與性質(zhì)中的狀態(tài)變量的距離為k或者更少的所有狀態(tài)變 量，則抽象模型的LBD等于k。換而言之，抽象模型的下界距離k 是距離值，從而距離為k或者更少的所有狀態(tài)變量在抽象模型中。

用于抽象模型的上界距離可以被定義為在抽象模型中的狀態(tài) 變量與性質(zhì)中的狀態(tài)變量之間的最大距離值。

在一些實(shí)施方式中，系統(tǒng)可以構(gòu)造稱為LBD抽象模型的如下 抽象模型，該抽象模型包括CUV中的與性質(zhì)中的狀態(tài)變量的距離為 k或者更少的所有狀態(tài)變量。注意這一抽象模型的LBD為k。然后， 系統(tǒng)可以通過使用LBD抽象模型來確定對于性質(zhì)而言是否存在反 例。如果存在反例，則系統(tǒng)可以存儲值k，從而抽象-精化技術(shù)可以 使用存儲的LBD值以確定是否可以略過可達(dá)性分析。另一方面，如 果不存在反例，則系統(tǒng)可以確定CUV滿足性質(zhì)。

具體而言，抽象-精化技術(shù)可以針對抽象模型計算上界距離并 且確定當(dāng)前LBD值是否大于或者等于上界距離。如果當(dāng)前LBD值 大于或者等于上界距離，則抽象-精化技術(shù)可以推斷抽象模型不滿足 性質(zhì)，并且抽象-精化技術(shù)可以決定不對抽象模型執(zhí)行可達(dá)性分析。 注意系統(tǒng)可以與抽象精化并行地執(zhí)行LBD計算。

系統(tǒng)可以使用諸多技術(shù)來確定反例，這些技術(shù)包括但不限于基 于二元決策圖(BDD)的技術(shù)、基于自動測試圖案生成器(APTG) 的技術(shù)和基于可滿足性(SAT)的技術(shù)?；赟AT的技術(shù)包括但不 限于有界模型檢驗(yàn)(BMC)、歸納和插值。

附圖說明

圖1圖示了根據(jù)一個實(shí)施方式的在集成電路的設(shè)計和制作過 程中的各種階段；

圖2圖示了根據(jù)一個實(shí)施方式的驗(yàn)證環(huán)境；

圖3圖示了根據(jù)一個實(shí)施方式的用于與CUV相關(guān)聯(lián)的多個抽 象模型的示例性圖示；