本文簡單介紹了形式化方法的起源、發(fā)展、關鍵技術，并與傳統(tǒng)的基于模擬的驗證方法進行對比，分析它的優(yōu)點和不足。對數(shù)字硬件形式化驗證技術進行了分類，模型檢測，定理證明和等價性檢驗。本文重點是基于HOL定理證明器的驗證。為使用HOL系統(tǒng)，簡單介紹函數(shù)式編程語言MOSCOW ML，該語言是HOL系統(tǒng)的元語言。我們詳細介紹了該定理證明器所支持高階邏輯。分析了HOL系統(tǒng)的邏輯建立過程，常用的理論庫和重寫策略。特別分析了HOL系統(tǒng)的證明方法及前向證明和目標制導這兩種方法。作為上述理論的實際應用，重點給出了RSA數(shù)字硬件的一個形式化驗證實例。首先介紹如何利用HOL驗證RSA算法的正確性。然后詳細介紹如何用HOL系統(tǒng)驗證硬件設計的正確性。通過嚴密的思維和機器的輔助在嚴格的邏輯系統(tǒng)的基礎上進行的證明可以提高設計的可靠性，進一步加強了RSA算法和硬件實現(xiàn)的正確性的信心。同時培養(yǎng)我們的科學態(tài)度和利用數(shù)學工具分析和解決問題的能力。 

【文章來源】：西安電子科技大學陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：69 頁

【學位級別】：碩士

【文章目錄】：
緒論
第一章 數(shù)字硬件形式化驗證概述
    1.1 形式化
    1.2 形式化的方法
    1.3 形式化的發(fā)展
    1.4 硬件形式化描述
    1.5 硬件形式化驗證的過程
    1.6 定理證明器
第二章 HOL系統(tǒng)
    2.1 ML語言的介紹
    2.2 HOL系統(tǒng)
第三章 RSA加密算法的形式化證明
    3.1 RSA算法
    3.2 RSA的安全性
    3.3 RSA的現(xiàn)狀和前景
    3.4 RSA算法正確性的形式化驗證
第四章 RSA數(shù)字硬件的形式化驗證
    4.1 VHDL語言簡介
    4.2 RSA數(shù)字硬件的實現(xiàn)
    4.3 模和同余的轉換的形式化證明
    4.4 模乘運算模塊的形式化驗證
    4.5 加密模塊的形式化驗證
    4.6 證明思路的總結
    4.7 驗證的結果
結論
致謝
參考文獻
作者在讀期間的研究成果
附錄A 重要定理證明對策清單
附錄B RSA數(shù)字硬件VHDL程序清單


【參考文獻】：
期刊論文
[1]基于高階邏輯的硬件驗證方法[J]. 霍紅衛(wèi),韓俊剛.  計算機學報. 1993(10)



本文編號：3150895