由于同步電路設(shè)計(jì)的局限性,如時(shí)鐘偏移、抖動(dòng)、噪聲和能耗方面,異步電路設(shè)計(jì)越來(lái)越受到人們的關(guān)注。異步電路已被廣泛應(yīng)用于各類電子系統(tǒng)中,因此它們的正確性必須仔細(xì)考慮。對(duì)異步電路的行為的描述和驗(yàn)證,是關(guān)于異步電路系統(tǒng)研究的關(guān)鍵問(wèn)題。近些年,大多數(shù)的模擬和驗(yàn)證使用的都是基于狀態(tài)的形式化模型,而基于動(dòng)作的形式化模型,即事件結(jié)構(gòu),因?yàn)榻＿^(guò)程復(fù)雜的原因,很少被應(yīng)用于系統(tǒng)的形式化仿真模擬和驗(yàn)證。本文選擇擴(kuò)展的綁定事件結(jié)構(gòu)（EBES）對(duì)異步電路進(jìn)行建模和驗(yàn)證,并對(duì)EBES的進(jìn)程代數(shù)語(yǔ)義進(jìn)行詳細(xì)的介紹。事件是事件結(jié)構(gòu)的基本單元,事件表示一個(gè)動(dòng)作的發(fā)生,那么如何在異步電路中獲取動(dòng)作是十分關(guān)鍵的。為此,在本文中給出了從信號(hào)傳輸波型中獲取動(dòng)作的方法。通過(guò)信號(hào)傳輸波形,將每個(gè)信號(hào)分為4個(gè)動(dòng)作,其中包含兩個(gè)穩(wěn)定動(dòng)作表示信號(hào)的有效傳輸。根據(jù)EBES的定義,文中呈現(xiàn)了簡(jiǎn)單邏輯門(mén)的標(biāo)記語(yǔ)義。由于復(fù)雜邏輯可以由基本邏輯單元組合而成,因此可以以組合的形式構(gòu)建其EBES。異步電路的驗(yàn)證主要是判斷其EBES實(shí)現(xiàn)和規(guī)范是否具有一致性。在使用互模擬等價(jià)檢驗(yàn)時(shí)發(fā)現(xiàn),要達(dá)到預(yù)想的結(jié)果,必須給實(shí)現(xiàn)添加太多的限制,但這樣的電路是很難設(shè)計(jì)出... 

【文章來(lái)源】：蘭州大學(xué)甘肅省 211工程院校 985工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：54 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

進(jìn)程代數(shù)的操作語(yǔ)義

圖 3-1 如何在波型中獲取動(dòng)作圖 3-1 中呈現(xiàn)的波形，可以通過(guò)信號(hào)波形的組合來(lái)描述一個(gè)僅僅描述信號(hào)的高低變化，而且描述了從高電平到低電平的變化趨勢(shì)。通過(guò)動(dòng)作可以自然而然地抽象出信號(hào)的變化中，可以抽象出 4 個(gè)動(dòng)作。當(dāng)信號(hào)的電壓小于 low 可以得到壓值高于 high 可以得到動(dòng)作 as+；當(dāng)信號(hào)的電壓高于 low 并于上升時(shí)，可以得到動(dòng)作 a+；但當(dāng)處于下降狀態(tài)時(shí)，相應(yīng)在實(shí)際電路中，信號(hào)也不是在最高點(diǎn)才是有效的，它是達(dá)到出去，因此上述動(dòng)作的提取方法是可以正確的描述一個(gè)信號(hào)述描述，任何信號(hào)均可被分為 4 個(gè)動(dòng)作，例如信號(hào) a 可以被+和 as-。輯門(mén)的 EBES

號(hào) a 和信號(hào) b 是無(wú)依賴關(guān)系的，以根據(jù)每個(gè)邏輯門(mén)的 EBES 圖得基本邏輯門(mén)的 EBES 后，接下介紹如何從簡(jiǎn)單邏輯門(mén)的 EB實(shí)現(xiàn)包含許多原始的與/或邏輯單元起。形式上，連接的引腳包含幾間的通信來(lái)執(zhí)行組合行為就像真，如何確保所有的通信過(guò)程跟真。通過(guò)并行組合操作，我們可以

【參考文獻(xiàn)】：
期刊論文
[1]基于高階π演算的構(gòu)件演化行為研究[J]. 何海洋,李強(qiáng),余祥,韓翔宇.  計(jì)算機(jī)科學(xué). 2017(03)
[2]基于硬件模擬的SAT求解框架[J]. 何安平,毛樂(lè)樂(lè),諶知學(xué),吳盡昭.  微電子學(xué)與計(jì)算機(jī). 2016(09)
[3]基于Spin的安全協(xié)議形式化驗(yàn)證技術(shù)[J]. 冉俊軼,吳盡昭.  計(jì)算機(jī)應(yīng)用. 2014(S2)

博士論文
[1]多項(xiàng)式代數(shù)事件結(jié)構(gòu)及其近似和近似等價(jià)[D]. 王超.北京交通大學(xué) 2016
[2]擴(kuò)展π演算的建模、驗(yàn)證與測(cè)試[D]. 羅玲.西安電子科技大學(xué) 2015
[3]基于動(dòng)作細(xì)化的異步電路自動(dòng)綜合[D]. 孫秀莉.中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所） 2005

碩士論文
[1]基于CSP的城軌CBTC聯(lián)鎖邏輯形式化建模與驗(yàn)證[D]. 馬慧.北京交通大學(xué) 2013
[2]基于Petri網(wǎng)的異步電路設(shè)計(jì)研究[D]. 謝曄.江蘇大學(xué) 2008
[3]基于SPIN的ATM交換機(jī)行為的驗(yàn)證[D]. 吳孝軍.蘭州大學(xué) 2006
[4]概率進(jìn)程代數(shù)的度量指稱語(yǔ)義[D]. 曾瓊.中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所） 2006



本文編號(hào)：3264956