動態(tài)可重構(gòu)系統(tǒng)形式化驗(yàn)證工具與原型平臺的設(shè)計與實(shí)現(xiàn).pdf

1、隨著計算機(jī)技術(shù)的發(fā)展，尤其是現(xiàn)場可編程門陣列(FPGA)的出現(xiàn)，使動態(tài)可重構(gòu)技術(shù)成為嵌入式領(lǐng)域研究的熱點(diǎn)和重點(diǎn)?；贔PGA的動態(tài)可重構(gòu)系統(tǒng)采用硬件電路實(shí)現(xiàn)計算功能，并允許在系統(tǒng)執(zhí)行過程中對FPGA的全部或者部分邏輯資源進(jìn)行動態(tài)的功能變換。因此，動態(tài)可重構(gòu)系統(tǒng)能夠提供接近專用電路(ASIC)的計算性能和接近軟件的可編程性。
　　動態(tài)可重構(gòu)系統(tǒng)體系結(jié)構(gòu)的復(fù)雜性，以及通過動態(tài)可重構(gòu)計算所實(shí)現(xiàn)的系統(tǒng)功能的復(fù)雜性為基于該技術(shù)的嵌入式系統(tǒng)的

2、設(shè)計帶來了巨大挑戰(zhàn)。如何在系統(tǒng)的各個設(shè)計階段，針對不同抽象級別的系統(tǒng)設(shè)計驗(yàn)證系統(tǒng)的正確性，是擺在所有系統(tǒng)設(shè)計者面前的一個亟待解決的問題。
　　基于這一背景，本文為動態(tài)可重構(gòu)系統(tǒng)的開發(fā)設(shè)計了一套完整的系統(tǒng)驗(yàn)證環(huán)境。這一環(huán)境主要包括兩個服務(wù)于不同設(shè)計階段的驗(yàn)證工具/平臺。本文設(shè)計并實(shí)現(xiàn)了一個面向高抽象級別系統(tǒng)模型的形式化驗(yàn)證工具，這一工具通過數(shù)學(xué)公式推導(dǎo)、模型檢測等理論和技術(shù)，對動態(tài)可重構(gòu)系統(tǒng)中的調(diào)度算法和放置策略等設(shè)計進(jìn)行驗(yàn)證，以保

3、證系統(tǒng)在性能、面積、可預(yù)測性等方面的需求得到滿足。此外，本文還設(shè)計實(shí)現(xiàn)了一個基于uC/OS-Ⅱ?qū)崟r操作系統(tǒng)的原型平臺，該平臺允許在實(shí)際操作系統(tǒng)環(huán)境下，對所采用的實(shí)時調(diào)度策略、軟硬件通信機(jī)制等詳細(xì)設(shè)計進(jìn)行驗(yàn)證，以保證在實(shí)際環(huán)境下策略或機(jī)制設(shè)計的正確性。
　　通過設(shè)計這樣一套完整的動態(tài)可重構(gòu)系統(tǒng)驗(yàn)證環(huán)境，使得設(shè)計者可以在動態(tài)可重構(gòu)系統(tǒng)開發(fā)的不同時期對系統(tǒng)的正確性進(jìn)行驗(yàn)證，從而保證設(shè)計質(zhì)量，提高設(shè)計效率，降低設(shè)計成本，減少基于可重構(gòu)技術(shù)