本文關(guān)鍵詞：基于形式化方法的Booth乘法器可靠性研究

  更多相關(guān)文章： 形式化方法 定理證明 乘法器 Booth算法 HOL4

【摘要】：由于超大規(guī)模集成電路的快速發(fā)展,系統(tǒng)的可靠性驗(yàn)證已經(jīng)成為人們研究的重點(diǎn)。乘法器作為高性能微處理器中的核心運(yùn)算部件,對(duì)它的可靠性進(jìn)行驗(yàn)證是必不可少的一個(gè)環(huán)節(jié)。本文采用定理證明方法對(duì)二階Booth乘法器的可靠性進(jìn)行了研究,并在定理證明器HOL4中進(jìn)行了相關(guān)的驗(yàn)證,主要完成的工作包括：首先介紹了形式化方法的基本概念,重點(diǎn)說(shuō)明了定理證明方法以及定理證明器HOL4系統(tǒng),其中包括HOL系統(tǒng)的發(fā)展歷史、建模語(yǔ)言和證明方法等。其次形式化分析了二階Booth算法的實(shí)現(xiàn)和規(guī)范,并在HOL4系統(tǒng)中完成了該算法的實(shí)現(xiàn)和規(guī)范的形式化建模；針對(duì)二階Booth乘法器的結(jié)構(gòu)特點(diǎn),使用形式化方法詳盡地分析了Booth編碼模塊、壓縮模塊和最終求和模塊的實(shí)現(xiàn)和規(guī)范,并在HOL4系統(tǒng)中完成了這三個(gè)模塊的實(shí)現(xiàn)和規(guī)范的形式化建模。接著在壓縮模塊和最終求和模塊的基礎(chǔ)上,層次化分析了組合模塊的實(shí)現(xiàn)和規(guī)范,并在HOL4系統(tǒng)中完成了它的實(shí)現(xiàn)和規(guī)范的形式化建模。最后在HOL4系統(tǒng)中,利用建模過(guò)程中定義的定理以及內(nèi)嵌的公理、推理規(guī)則等完成了對(duì)Booth算法、Booth編碼模塊、壓縮模塊、最終求和模塊以及組合模塊的形式化驗(yàn)證,不僅證明了二階Booth乘法器的可靠性,也展現(xiàn)了HOL4系統(tǒng)在硬件驗(yàn)證與算法驗(yàn)證上的強(qiáng)大功能,對(duì)HOL4系統(tǒng)的進(jìn)一步發(fā)展起到了促進(jìn)作用。
【關(guān)鍵詞】：形式化方法 定理證明 乘法器 Booth算法 HOL4
【學(xué)位授予單位】：北京化工大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類號(hào)】：TP332.22
【目錄】：

• 摘要4-6
• ABSTRACT6-12
• 第一章 緒論12-18
• 1.1 研究背景及意義12-13
• 1.2 國(guó)內(nèi)外研究現(xiàn)狀13-15
• 1.3 課題研究的主要內(nèi)容15
• 1.4 本文組織結(jié)構(gòu)15-18
• 第二章 形式化方法18-32
• 2.1 形式化方法簡(jiǎn)介18-19
• 2.2 模型檢測(cè)19-20
• 2.3 等價(jià)性檢測(cè)20-21
• 2.4 定理證明21-22
• 2.5 HOL4系統(tǒng)22-31
• 2.5.1 HOL系統(tǒng)的歷史發(fā)展22-23
• 2.5.2 ML語(yǔ)言23-25
• 2.5.3 HOL邏輯與類型25-27
• 2.5.4 HOL的證明方法27-31
• 2.6 本章小結(jié)31-32
• 第三章 二階Booth乘法器的形式化分析與建模32-52
• 3.1 Booth算法32-33
• 3.2 二階Booth乘法器的電路實(shí)現(xiàn)33-40
• 3.2.1 Booth編碼模塊35-37
• 3.2.2 壓縮模塊37-39
• 3.2.3 最終求和模塊39
• 3.2.4 組合模塊39-40
• 3.3 二階Booth乘法器的形式化建模40-50
• 3.3.1 Booth算法的形式化建模40-42
• 3.3.2 Booth編碼電路的形式化建模42-43
• 3.3.3 壓縮模塊的形式化建模43-44
• 3.3.4 最終求和模塊的形式化建模44-48
• 3.3.5 組合模塊的形式化建模48-50
• 3.4 本章小結(jié)50-52
• 第四章 二階Booth乘法器的可靠性驗(yàn)證52-70
• 4.1 Booth算法的形式化驗(yàn)證52-55
• 4.2 Booth編碼模塊的形式化驗(yàn)證55-61
• 4.3 壓縮模塊的形式化驗(yàn)證61-63
• 4.4 最終求和模塊的形式化驗(yàn)證63-65
• 4.5 組合模塊的形式化驗(yàn)證65-68
• 4.6 本章小結(jié)68-70
• 第五章 總結(jié)與展望70-72
• 5.1 總結(jié)70
• 5.2 展望70-72
• 參考文獻(xiàn)72-76
• 致謝76-78
• 研究成果及發(fā)表的學(xué)術(shù)論文78-80
• 作者與導(dǎo)師簡(jiǎn)介80-81
• 附件81-82

【參考文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前3條

1 朱一杰,張曦,俞軍;雙字節(jié)Booth乘法器的優(yōu)化設(shè)計(jì)[J];復(fù)旦學(xué)報(bào)(自然科學(xué)版);2005年01期

2 楊澤民;范全潤(rùn);;硬件設(shè)計(jì)的形式化驗(yàn)證技術(shù)[J];太原師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2007年02期

3 趙剛;趙春娜;關(guān)永;呂興利;李曉娟;施智平;王瑞;葉世偉;;拉普拉斯變換微積分性質(zhì)在HOL4中的形式化[J];小型微型計(jì)算機(jī)系統(tǒng);2014年09期

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前1條

1 陳波;基于定理證明器HOL的硬件驗(yàn)證研究[D];蘭州大學(xué);2006年

，

本文編號(hào)：946295