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

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

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

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