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

• 作者: 刘树锟 彭浩 王雅琳
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 关联矩阵 量化调度 最小生存量化跨度 映像计算
• 年，卷（期）: 2010,（3）
• 所属期刊栏目: 基金项目论文
• 页码范围: 120-123
• 页数: 4页
• 分类号: TP3
• 字数: 4618字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386X.2010.03.038

摘要

在目前VLSI设计流程中,采用模型检测技术来实现形式化验证对可靠的硬件设计具有重要的意义.在以有序二值决策图(OBDD)为基础的符号综合和验证过程中,需要对有限状态机各传输关系合取运算的先后顺序进行量化调度,从而降低求解过程中各临时OBDD所消耗的内存资源,也就降低了对某些验证的状态空间爆炸的风险.调度策略通过对各传输关系与量化变量构成的关联矩阵的分析,以不断降低变量的平均生存量化跨度为目标,提出了能减少变量参与合取运算次数的MSTA(Minimum Subsistence Traversal Algorithm)过程、关联矩阵的连接子图分解策略和考虑关联矩阵中前后行关联程度的串接过程.实验表明了此合取量化调度过程的有效性和鲁棒性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王雅琳	中南大学信息科学与工程学院	84	519	11.0	17.0
2	彭浩	湖南涉外经济学院计算机科学与技术学部	35	50	4.0	5.0
3	刘树锟	湖南涉外经济学院计算机科学与技术学部	15	50	3.0	6.0