近年來，由于電路規(guī)模不斷增大和電路功能日趨復(fù)雜，使得大規(guī)模集成電路的設(shè)計很難保證邏輯設(shè)計的正確無誤。為了設(shè)計和建立高可靠性的VLSI系統(tǒng)，必須對VLSI的設(shè)計和實現(xiàn)進行有效的驗證。目前主要的驗證方法有模擬驗證和形式驗證兩種，模擬驗證是當(dāng)前工業(yè)界使用的主要方法，但是由于單純的模擬驗證已不能滿足VLSI設(shè)計和制造的需要，形式驗證的方法越來越引起人們的重視。 模型檢驗（Model checking）方法是一種很有前途的形式驗證方法，它的驗證方法是通過對有限狀態(tài)空間的遍歷來確認規(guī)范說明（Specification）是否得到滿足。這種方法具有高度自動化，執(zhí)行速度快，能產(chǎn)生反例來幫助調(diào)試等特點，比較適合于VLSI的驗證。 有效地建立和表示時序邏輯電路的狀態(tài)轉(zhuǎn)移關(guān)系是應(yīng)用模型檢查方法驗證時序邏輯電路的關(guān)鍵技術(shù)之一。作者詳盡地討論了如何用二元判決圖（BDD）表示時序邏輯電路的狀態(tài)轉(zhuǎn)移關(guān)系，在此基礎(chǔ)之上，作者考察了一種單位時延的電位異步時序電路，提出并實現(xiàn)了表示其穩(wěn)定狀態(tài)轉(zhuǎn)移關(guān)系的算法。 符號模型檢驗（Symbolic Model checking）是時序邏輯模型檢驗的技術(shù)一種具體方法... 

【文章來源】：中國科學(xué)院大學(xué)(中國科學(xué)院計算技術(shù)研究所)北京市

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

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
目錄
第一章 綜述
    1.1 引言
    1.2 驗證的基本概念
    1.3 驗證方法綜述
        1.3.1 模擬驗證
            1.3.1.1 模擬驗證的基本原理
            1.3.1.2 事件驅(qū)動模擬和基于周期的模擬
            1.3.1.3 硬件加速和硬件仿真
            1.3.1.4 模擬驗證的特點
        1.3.2 形式驗證
            1.3.2.1 形式驗證的基本過程
            1.3.2.2 模型檢驗
            1.3.2.3 定理證明
            1.3.2.4 形式驗證方法與模擬驗證方法的比較
第二章 二元判決圖及其在電路驗證中的應(yīng)用
    2.1 引言
    2.2 二元判決圖
        2.2.1 二元判決圖的基本概念
        2.2.2 簡化有序二元判決圖(ROBDD)的性質(zhì)
        2.2.3 目前對BDD研究的新進展
    2.3 符號模型檢驗的BDD表示和操作
        2.3.1 用BDD表示基本的布爾操作
        2.3.2 用BDD表示的量詞操作
        2.3.3 用BDD表示集合和狀態(tài)轉(zhuǎn)移關(guān)系
第三章 符號模型檢驗技術(shù)
    3.1 引言
    3.2 計算樹邏輯(CTL—Computation Tree Logic)
    3.3 Kripke結(jié)構(gòu)上冪集運算的不動點特性
    3.4 符號模型檢驗技術(shù)
        3.4.1 用BDD表示被驗證系統(tǒng)
        3.4.2 符號模型檢驗的基本算法
    3.5 公平性約束檢驗(Fairness Constraints)
第四章 用符號模型檢驗技術(shù)驗證時序邏輯電路
    4.1 引言
    4.2 同步時序邏輯電路的BDD表示
    4.3 異步時序邏輯電路的BDD表示
第五章 符號模型檢驗系統(tǒng)的設(shè)計和實現(xiàn)
    5.1 引言
    5.2 SCSMV輸入語言的語法規(guī)則和編譯器的設(shè)計
        5.2.1 詞法規(guī)則
        5.2.2 語法規(guī)則
    5.3 SCSMV的數(shù)據(jù)結(jié)構(gòu)和算法實現(xiàn)
    5.4 實驗結(jié)果
第六章 結(jié)束語
    6.1 結(jié)論
    6.2 將來的工作
附錄
參考文獻
致謝
作者簡歷


【參考文獻】：
期刊論文
[1]專用集成電路的設(shè)計驗證方法及一種實際的通用微處理器設(shè)計的多級驗證體系[J]. 楊文華,羅曉沛.  計算機研究與發(fā)展. 1999(06)



本文編號：3428491