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

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 achievements of this project are expected to enrich and develop the theories and methods of formal verification and diagnosis as well as promote significantly the practicability of formal verification and diagnosis.

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

形式化验证和不一致诊断方法是为了克服传统模拟方法的缺陷而兴起的智能技术。然而，随着集成电路规模呈摩尔规律的爆炸式增长，形式化验证和诊断技术已成为集成电路工业快速发展的瓶颈。传统的等价性验证和不一致诊断方法未能有效利用模型中蕴涵的诸多电路相关特征， 本项目根据申请报告和研究计划书对等价性验证及不一致诊断方法进行了研究，主要进展和取得的成果包括：（1）给出SLM和RTL模型高效简洁表示方法；（2）提出依据约束关系对电路结构特征进行抽取方法；（3）给出结合问题特征的割集提取方法；（4）提出基于SAT和ATPG的验证和诊断方法；（5）给出基于冲突学习和SP的优化求解方法；（6）提出基于骨架变量的优先诊断子空间提取方法；（7）开发了实验原型系统和获得了国家授权发明专利。在超额完成项目计划情况下，项目组还对与本项目研究内容相关的离散事件系统模型诊断、结合结构特征的规划方法和本体调试等领域进行了研究。本项目取得的成果进一步丰富了形式化验证和不一致诊断的理论与方法，显著提高其实用性， 对集成电路产业发展具有重要推动作用。. 在本项目的支持下，项目组提出的方法在国内外核心以上期刊和学术会议上发表和接受论文50多篇，其中被SCI/EI检索论文40多篇。主要发表在《SCIENCE CHINA Information Sciences》、《Expert Systems with Applications》、《Engineering Applications of Artificial Intelligence》、《Neural Computing and Applications》、《软件学报》、《计算机学报》、《计算机研究与发展》和《电子学报》等国内外权威期刊上。