基于形式化方法的Booth乘法器可靠性研究.pdf

1、由于超大規(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ǔ)言和證明方法等。
　　其

2、次形式化分析了二階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ī)范的形式化建模。
　　最后在HOL