有界模型檢驗(yàn)與時(shí)序深度計(jì)算算法研究.pdf

1、隨著集成電路技術(shù)的飛速發(fā)展，電路的規(guī)模不斷增大。電路驗(yàn)證領(lǐng)域正面臨前所未有的挑戰(zhàn)，如何快速并且完備地完成超大規(guī)模集成電路的設(shè)計(jì)驗(yàn)證，已經(jīng)成為當(dāng)前的研究熱點(diǎn)。與傳統(tǒng)的基于模擬的驗(yàn)證方法相比，形式化驗(yàn)證方法中的模型驗(yàn)證方法由于具有完備性的優(yōu)點(diǎn)被廣泛使用。為了擴(kuò)大模型檢驗(yàn)的驗(yàn)證范圍，被稱為有界模型檢驗(yàn)的驗(yàn)證方法被提出。然而，有界模型檢驗(yàn)算法最主要的缺點(diǎn)是驗(yàn)證的不完備性，即我們不知道驗(yàn)證所需的深度。為了克服有界模型檢驗(yàn)算法的這個(gè)缺點(diǎn)，本文提出的

2、時(shí)序深度計(jì)算的算法。該算法創(chuàng)新之處分為兩點(diǎn)：(1)基于可滿足算法引擎的后續(xù)狀態(tài)的計(jì)算。由于本文在后續(xù)狀態(tài)的計(jì)算中使用了可滿足算法引擎，大大提高了后續(xù)狀態(tài)的計(jì)算速度和計(jì)算的能力。并且我們計(jì)算的規(guī)模較小，每次運(yùn)算后可滿足問題的子句數(shù)目變化很小，因此一直可以保持比較快速和高效的計(jì)算。(2)基于高度平衡二叉搜索樹的歷史狀態(tài)的存儲(chǔ)方法。由于本文所提的算法需要大量的查找歷史狀態(tài)的操作，因此如何得到一個(gè)穩(wěn)定的平均查找時(shí)間就成為了本算法的一個(gè)要點(diǎn)。因此