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

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

ON QUANTIFICATION SCHEDULING ALGORITHM OF VARIABLES IMPROVING PERFORMANCE OF OBDD

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 explosio...