有界模型檢驗與時序深度計算算法研究.pdf

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

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