Hybrid Satisfiability Solving for RTL Verification

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.