【摘要】 RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.更多还原

【Abstract】 RTL hybrid satisfiability solving methods are classified into two categories:One is based on SMT(Satisfiability Modulo Theories),and the other is based on circuit structure searching.The methods of the former category mainly use logic reasoning,and are widely applied in processor verification because SMT supports the fundamental theories used to express the verification conditions.The methods of the latter category are efficient because they can take full advantage of constraint information in circuits.Representative works and their key strategies are introduced for each category.Research progress of RTL hybrid satisfiability solving for our Formal Verification Research Group is also introduced.更多还原