结合问题特征的集成电路等价性验证及不一致诊断关键方法研究

项目名称： 结合问题特征的集成电路等价性验证及不一致诊断关键方法研究

项目编号： No.61272208

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 欧阳丹彤

作者单位： 吉林大学

项目金额： 81万元

中文摘要： 形式化验证和不一致诊断方法是为了克服传统模拟方法的缺陷而兴起的智能技术，对人工智能领域的理论研究和集成电路产业发展具有重要推动作用。然而，形式化验证方法和技术无法满足当前超大规模集成电路验证的需要，验证过程已成为集成电路工业设计流程的瓶颈。 传统的系统级模型和寄存器传输级模型等价性验证和不一致诊断方法未能有效利用模型中蕴涵的诸多电路相关特征。本项目拟从模型的静态结构和动态行为出发，研究系统级和寄存器传输级模型的高效表示方法，深入挖掘电路蕴涵关系和状态转移关系等。在此基础上研究问题空间缩减方法和特征启发式可满足问题求解方法，以提高形式化验证和不一致诊断的实际执行效率。研制原型系统对本项目提出的方法进行检验。 项目的预期成果将丰富和发展形式化验证与不一致诊断的理论与方法，显著提高其实用性。

中文关键词： 等价性验证；不一致诊断；特征抽取；可满足问题；调查传播

英文摘要： As newly-raised intelligent technologies, formal verification and inconsistent diagnosis have overcome the defects of traditional ones, promoting the development of theoretical research in the field of artificial intelligence as well as the prosperity of integrated circuit industry. However, as the methods and technologies of formal verification can not satisfy the demand of super-scale integrated circuits, verification process has become a bottleneck for integrated circuit design. Traditional equivalence checking and inconsistent diagnosis methods on System Level Model (SLM) and Register Transfer Level (RTL) model have not made effective use of circuit characteristics. This project brings forward highly effective methods to express System Level Model (SLM) and Register Transfer Level (RTL) model in terms of the static architectures and dynamic behaviors of the models, exploring deeply the implication relations and state transition relations of circuits, etc. Base on this, the project puts forward resolution methods that can satisfy both space reduction methods and elicitation methods based on characteristics so as to improve the actual implementation efficiency of formal verification and inconsistent diagnosis. In addition, a prototype system is built up to check the methods we propose in this project. The achi

英文关键词： equivalence checking；inconsistent diagnosis；characteristics extraction；satisfiability problem；survey propagation