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

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

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

【學位級別】：碩士

【文章目錄】：
摘要
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 形式驗證方法與模擬驗證方法的比較
第二章 二元判決圖及其在電路驗證中的應用
    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)轉移關系
第三章 符號模型檢驗技術
    3.1 引言
    3.2 計算樹邏輯(CTL—Computation Tree Logic)
    3.3 Kripke結構上冪集運算的不動點特性
    3.4 符號模型檢驗技術
        3.4.1 用BDD表示被驗證系統(tǒng)
        3.4.2 符號模型檢驗的基本算法
    3.5 公平性約束檢驗(Fairness Constraints)
第四章 用符號模型檢驗技術驗證時序邏輯電路
    4.1 引言
    4.2 同步時序邏輯電路的BDD表示
    4.3 異步時序邏輯電路的BDD表示
第五章 符號模型檢驗系統(tǒng)的設計和實現(xiàn)
    5.1 引言
    5.2 SCSMV輸入語言的語法規(guī)則和編譯器的設計
        5.2.1 詞法規(guī)則
        5.2.2 語法規(guī)則
    5.3 SCSMV的數(shù)據(jù)結構和算法實現(xiàn)
    5.4 實驗結果
第六章 結束語
    6.1 結論
    6.2 將來的工作
附錄
參考文獻
致謝
作者簡歷


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



本文編號：3428491