计算机应用与软件
計算機應用與軟件
계산궤응용여연건
COMPUTER APPLICATIONS AND SOFTWARE
2010年
3期
120-123
,共4页
关联矩阵%量化调度%最小生存量化跨度%映像计算
關聯矩陣%量化調度%最小生存量化跨度%映像計算
관련구진%양화조도%최소생존양화과도%영상계산
在目前VLSI设计流程中,采用模型检测技术来实现形式化验证对可靠的硬件设计具有重要的意义.在以有序二值决策图(OBDD)为基础的符号综合和验证过程中,需要对有限状态机各传输关系合取运算的先后顺序进行量化调度,从而降低求解过程中各临时OBDD所消耗的内存资源,也就降低了对某些验证的状态空间爆炸的风险.调度策略通过对各传输关系与量化变量构成的关联矩阵的分析,以不断降低变量的平均生存量化跨度为目标,提出了能减少变量参与合取运算次数的MSTA(Minimum Subsistence Traversal Algorithm)过程、关联矩阵的连接子图分解策略和考虑关联矩阵中前后行关联程度的串接过程.实验表明了此合取量化调度过程的有效性和鲁棒性.
在目前VLSI設計流程中,採用模型檢測技術來實現形式化驗證對可靠的硬件設計具有重要的意義.在以有序二值決策圖(OBDD)為基礎的符號綜閤和驗證過程中,需要對有限狀態機各傳輸關繫閤取運算的先後順序進行量化調度,從而降低求解過程中各臨時OBDD所消耗的內存資源,也就降低瞭對某些驗證的狀態空間爆炸的風險.調度策略通過對各傳輸關繫與量化變量構成的關聯矩陣的分析,以不斷降低變量的平均生存量化跨度為目標,提齣瞭能減少變量參與閤取運算次數的MSTA(Minimum Subsistence Traversal Algorithm)過程、關聯矩陣的連接子圖分解策略和攷慮關聯矩陣中前後行關聯程度的串接過程.實驗錶明瞭此閤取量化調度過程的有效性和魯棒性.
재목전VLSI설계류정중,채용모형검측기술래실현형식화험증대가고적경건설계구유중요적의의.재이유서이치결책도(OBDD)위기출적부호종합화험증과정중,수요대유한상태궤각전수관계합취운산적선후순서진행양화조도,종이강저구해과정중각림시OBDD소소모적내존자원,야취강저료대모사험증적상태공간폭작적풍험.조도책략통과대각전수관계여양화변량구성적관련구진적분석,이불단강저변량적평균생존양화과도위목표,제출료능감소변량삼여합취운산차수적MSTA(Minimum Subsistence Traversal Algorithm)과정、관련구진적련접자도분해책략화고필관련구진중전후행관련정도적천접과정.실험표명료차합취양화조도과정적유효성화로봉성.
