Formal Verification for RTL and TLM Designs

         SAT is widely applied in electronic design automation (EDA), especially formal verification, and other fields. SAT solving techniques have been improved rapidly in the last decade. Boolean SAT has been applied in gate-level formal verification successfully. They performed well in model checking. Almost all the SAT solvers used in formal verification are complete, which can find at least one solution if there are solutions). Do incomplete SAT solvers fit for formal verification? Constraint propagation can be adapted to reduce the epistasis in SAT solving using genetic algorithm.

Recently, for the formal verification in Register Transfer Level (RTL), the hybrid SAT problem, which contains not only Boolean but also word variables, has received more and more attention. Some efficient algorithms to solve the hybrid SAT problem are presented, which use complete hybrid branch-and-bound strategy with conflict-driven learning. Furthermore, hybrid three-valued SAT solving and symbolic simulation are combined for incomplete verification to improve the efficiency.

Satisfiability Modulo Theories (SMT) is considered as the second generation of verification engines comparing to the first generation with BDD and SAT. It is applied in high level circuit verification combining with hypergraph partitioning to improve the solving efficiency.

Now Transaction Level Modeling (TLM) is a new trend in EDA. TLM 2.0 was released on DAC 2008. Can SAT be extended to TLM? Some possible solutions will be shown in the talk.