欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
RTL混合可满足性求解方法分为基于可满足性模理论（SMT）和基于电路结构搜索两大类．前者主要使用逻辑推理的方法，目前已在处理器验证中得到了广泛的应用，主要得益于SMT支持用于描述验证条件的基础理论；后者能够充分地利用电路中的约束信息，因而求解效率较高．介绍了每一大类中的典型研究及其所采用的重要策略，以及RTL可满足性求解方面的研究进展．
英文摘要：
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 sa＇tisfiability solving for our Formal Verification Research Group is also introduced.
同期刊论文项目
同项目期刊论文
Stochastic local operations and classical communication properties of the n-qubit symmetric Dicke st
Classification of four-qubit states by means of a stochastic operation and the classical communicati
期刊信息
位置：