基于投影時序邏輯的片上系統(tǒng)形式化描述和驗證.pdf

1、隨著大規(guī)模集成電路技術(shù)和EDA技術(shù)的發(fā)展，片上系統(tǒng)(SoC)成為嵌入式系統(tǒng)的發(fā)展方向。片上系統(tǒng)帶來了一些技術(shù)上的問題，對設(shè)計正確性的要求更加迫切。如何減少系統(tǒng)設(shè)計中的錯誤，提高系統(tǒng)設(shè)計的可靠性成為備受關(guān)注的問題。傳統(tǒng)的設(shè)計方法由于系統(tǒng)規(guī)范缺少精確性，而驗證也不能提供百分之百的覆蓋，出錯的可能性很大。為了解決這個問題，形式化方法被應(yīng)用在軟硬件設(shè)計中。所謂形式化方法，就是利用嚴(yán)格的數(shù)學(xué)方法，從給出系統(tǒng)設(shè)計的規(guī)范開始并逐步地推導(dǎo)或者驗證系統(tǒng)的

2、方法。 投影時序邏輯PTI(projectiontemporallogic)是一種具有離散的時間模型的時序邏輯，可處理同時具有順序和并行的復(fù)合計算，為復(fù)雜系統(tǒng)的設(shè)計提供了強大的規(guī)范和證明技術(shù)。程序設(shè)計語言ExtendedTempura是PTL的一個可執(zhí)行的子集，可用來開發(fā)系統(tǒng)的原型，對系統(tǒng)進(jìn)行模擬。 本文介紹了形式化方法及投影時序邏輯和其可執(zhí)行子集的基本內(nèi)容，討論了PTL對SoC不同層次的描述方法，對把狀態(tài)圖轉(zhuǎn)換為PTL