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

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

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

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

【部分圖文】：

進程代數(shù)的操作語義

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

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

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

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

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



本文編號：3264956