基于HOL4的有限域乘法器的形式化研究.pdf

1、有限域乘法是數(shù)據(jù)編碼、解碼及數(shù)據(jù)加密算法中的核心運(yùn)算。為了保證算法正確地完成編解碼和加密的功能，必須對(duì)有限域乘法電路設(shè)計(jì)的可靠性進(jìn)行驗(yàn)證。與此同時(shí)，隨著硬件設(shè)計(jì)技術(shù)不斷發(fā)展，硬件電路性能快速提升，其設(shè)計(jì)也日趨復(fù)雜，如何保障硬件設(shè)計(jì)的正確可靠成為人們面臨的重大挑戰(zhàn)。傳統(tǒng)驗(yàn)證方法，如模擬/仿真的方法存在測(cè)試空間不完備的問(wèn)題，難以滿足硬件電路可靠性的需求。本文將使用定理證明方法對(duì)實(shí)現(xiàn)GF(2m)乘法的時(shí)序邏輯電路進(jìn)行形式化研究。在高階邏輯定理

2、證明器HOL4中完成驗(yàn)證，保障硬件設(shè)計(jì)的可靠性和功能正確性。本文主要完成以下幾個(gè)部分的工作:
　　一、對(duì)形式化方法的原理進(jìn)行簡(jiǎn)單介紹，比較形式化驗(yàn)證常見(jiàn)的四種方法，闡述各自的優(yōu)缺點(diǎn)并對(duì)定理證明器HOL4系統(tǒng)進(jìn)行深入研究，詳細(xì)剖析其發(fā)展歷程，編程語(yǔ)言，邏輯基礎(chǔ)和驗(yàn)證方法等。
　　二、對(duì)有限域及有限域乘法進(jìn)行詳細(xì)分析，總結(jié)其工作原理和硬件實(shí)現(xiàn)方法并剖析LSB-First算法的基本原理和演變過(guò)程。
　　三、在HOL4系統(tǒng)中使