基于Petri網(wǎng)的ASIP體系結(jié)構(gòu)形式化建模和驗(yàn)證.pdf

1、隨著大規(guī)模集成電路工藝的不斷提高以及嵌入式系統(tǒng)功能需求等多方面要求的日益增加，尋找正確有效地進(jìn)行嵌入式系統(tǒng)設(shè)計(jì)的方法成為一種普遍需求，相關(guān)的研究也被廣泛地展開。 ASIP(ApplicationSpecificInstruction-setProcessors)是針對特定應(yīng)用領(lǐng)域而設(shè)計(jì)的，是兼具ASIC(ApplicationSpecificIntegratedCircuits))的高性能和GPP(GeneralPurposeP

2、rocessor)的靈活性的一類特殊的處理器，在嵌入式系統(tǒng)中的應(yīng)用越來越多。我們采用的是基于體系結(jié)構(gòu)描述語言(ADL)驅(qū)動的體系結(jié)構(gòu)設(shè)計(jì)空間搜索DSE的ASIP設(shè)計(jì)方法，因此，在設(shè)計(jì)初期保證設(shè)計(jì)的正確性，以及在整個自上而下的設(shè)計(jì)流程中保證必要的屬性被保留，即保證設(shè)計(jì)的一致性，可以減少后期改正或重新設(shè)計(jì)的代價。業(yè)界在對設(shè)計(jì)正確性進(jìn)行檢驗(yàn)時主要是采用仿真的方法，但是由于其固有的局限性，形式化方法被提出，并得到廣泛的應(yīng)用。 本論文在對

3、國內(nèi)外主要的形式化驗(yàn)證技術(shù)進(jìn)行深入研究的基礎(chǔ)上，結(jié)合ADL驅(qū)動的ASIP設(shè)計(jì)流程的特點(diǎn)，提出一種基于Petri網(wǎng)的形式化建模和驗(yàn)證技術(shù)。主要工作如下： 提出PNP(PetriNetrepresentationforPipelinemodeling)模型，給出其定義和建模方法，以及PNP模型中的層次和等價等概念，用于基于模型的驗(yàn)證。 提出了兩種基于PNP模型進(jìn)行ASIP驗(yàn)證的方法，一是使用已有的模型檢驗(yàn)工具，用于系統(tǒng)狀態(tài)相