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

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

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

• 摘要4-6
• ABSTRACT6-12
• 第一章 緒論12-18
• 1.1 研究背景及意義12-13
• 1.2 國內外研究現(xiàn)狀13-15
• 1.3 課題研究的主要內容15
• 1.4 本文組織結構15-18
• 第二章 形式化方法18-32
• 2.1 形式化方法簡介18-19
• 2.2 模型檢測19-20
• 2.3 等價性檢測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語言23-25
• 2.5.3 HOL邏輯與類型25-27
• 2.5.4 HOL的證明方法27-31
• 2.6 本章小結31-32
• 第三章 二階Booth乘法器的形式化分析與建模32-52
• 3.1 Booth算法32-33
• 3.2 二階Booth乘法器的電路實現(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 本章小結50-52
• 第四章 二階Booth乘法器的可靠性驗證52-70
• 4.1 Booth算法的形式化驗證52-55
• 4.2 Booth編碼模塊的形式化驗證55-61
• 4.3 壓縮模塊的形式化驗證61-63
• 4.4 最終求和模塊的形式化驗證63-65
• 4.5 組合模塊的形式化驗證65-68
• 4.6 本章小結68-70
• 第五章 總結與展望70-72
• 5.1 總結70
• 5.2 展望70-72
• 參考文獻72-76
• 致謝76-78
• 研究成果及發(fā)表的學術論文78-80
• 作者與導師簡介80-81
• 附件81-82

【參考文獻】

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

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

2 楊澤民;范全潤;;硬件設計的形式化驗證技術[J];太原師范學院學報(自然科學版);2007年02期

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

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

1 陳波;基于定理證明器HOL的硬件驗證研究[D];蘭州大學;2006年

，

本文編號：946295