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

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.