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

1、由于超大規(guī)模集成電路的快速發(fā)展，系統(tǒng)的可靠性驗證已經(jīng)成為人們研究的重點。乘法器作為高性能微處理器中的核心運算部件，對它的可靠性進行驗證是必不可少的一個環(huán)節(jié)。本文采用定理證明方法對二階Booth乘法器的可靠性進行了研究，并在定理證明器HOL4中進行了相關(guān)的驗證，主要完成的工作包括:
　　首先介紹了形式化方法的基本概念，重點說明了定理證明方法以及定理證明器HOL4系統(tǒng)，其中包括HOL系統(tǒng)的發(fā)展歷史、建模語言和證明方法等。
　　其

2、次形式化分析了二階Booth算法的實現(xiàn)和規(guī)范，并在HOL4系統(tǒng)中完成了該算法的實現(xiàn)和規(guī)范的形式化建模;針對二階Booth乘法器的結(jié)構(gòu)特點，使用形式化方法詳盡地分析了Booth編碼模塊、壓縮模塊和最終求和模塊的實現(xiàn)和規(guī)范，并在HOL4系統(tǒng)中完成了這三個模塊的實現(xiàn)和規(guī)范的形式化建模。
　　接著在壓縮模塊和最終求和模塊的基礎(chǔ)上，層次化分析了組合模塊的實現(xiàn)和規(guī)范，并在HOL4系統(tǒng)中完成了它的實現(xiàn)和規(guī)范的形式化建模。
　　最后在HOL