摘要： 在数据控制流图(CDFG)结构的基础上,结合模拟验证和模型检测的优点,对需要验证的系统性质进行分类,采用不同的验证方法,提高验证的能力。通过对OVL语言和CTL描述进行改进,针对模拟验证、CDFG图匹配、模型检测3种方法设计相应的性质,实验结果表明这种分治验证策略有助于提高系统验证的效率和规模。
关键词:
模拟,
形式验证,
性质,
模型检测,
数据控制流图
Abstract: Based on the advantages of simulation and formal verification with CDFG structure, classified properties are proposed to activate their good qualities respectively. Improving on OVL assertions and CTL properties, three kinds of properties are defined and verified, and the experimental results demonstrate the scheme improves the verification efficiency and scale.
中图分类号:
朱明,边计年,吴为民. 基于CDFG和OVL的系统验证性质分类[J]. , 2005, 31(10): 57-59.
ZHU Ming, BIAN Jinian, WU Weimin. Property Classification for System Verification on CDFG Structure[J]. , 2005, 31(10): 57-59.