优化OBDD性能的变量量化调度算法研究  

ON QUANTIFICATION SCHEDULING ALGORITHM OF VARIABLES IMPROVING PERFORMANCE OF OBDD

作　　者：彭浩[1] 王雅琳[2] 刘树锟[1] 

机构地区：[1]湖南涉外经济学院计算机科学与技术学部,湖南长沙410205 [2]中南大学信息科学与工程学院,湖南长沙410083

出　　处：《计算机应用与软件》2010年第3期120-123,共4页Computer Applications and Software

基　　金：湖南省自然科学基金(06FD026);湖南省教育厅基金资助项目(09C597)

摘　　要：在目前VLSI设计流程中,采用模型检测技术来实现形式化验证对可靠的硬件设计具有重要的意义。在以有序二值决策图(OBDD)为基础的符号综合和验证过程中,需要对有限状态机各传输关系合取运算的先后顺序进行量化调度,从而降低求解过程中各临时OBDD所消耗的内存资源,也就降低了对某些验证的状态空间爆炸的风险。调度策略通过对各传输关系与量化变量构成的关联矩阵的分析,以不断降低变量的平均生存量化跨度为目标,提出了能减少变量参与合取运算次数的MSTA(Minimum Subsist-ence Traversal Algorithm)过程、关联矩阵的连接子图分解策略和考虑关联矩阵中前后行关联程度的串接过程。实验表明了此合取量化调度过程的有效性和鲁棒性。In current design flow of VLSI engineering, it is of great significant for reliable hardware design to implement formal verification by the use of model checking technology. In the process of symbolic synthesis and verification based on OBDD （ Ordered Binary Decision Diagram） , it is necessary for all transmission relations of finite state machine to schedule their order of conjunction in quantification. In consequence, the memory consumed by interim OBDD is reduced, that is to say, the hazard of state space explosion for some verifications is mitigated. For the scheduling strategy in this paper, by the analysis of dependent matrix composed of transmission relations and quantified variables, we advance the MSTA （ Minimum Subsistence Traversal Algorithm） process which decreases the frequencies of conjunction in which the variables take part, the connected sub-graph decomposition strategy of the dependent matrix and the clustering process which considers the correlation degree of two pre-and post-lines in dependent matrix for achieving the goal of constantly cutting down the mean subsistence quantification traversal of variables. Corresponding tests are done and demonstrated the method is effective and robust.

关 键 词：关联矩阵 量化调度 最小生存量化跨度 映像计算 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]