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

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

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

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

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


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



本文編號(hào)：3428491