Formal Verification for RTL and TLM Designs

Speaker:  JiNian Bian - Dept of Computer Science and Technology, Tsinghua University, Beijing, P. R. China
  Friday, September 12, 2008 at 2:15 PM Inizio alle 14:30, Caffè e biscotti alle 14:15.

 

         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.

 


Place
Ca' Vignal 3 - Piramide, Floor 0, Hall Verde

Contact person
Maria Paola Bonacina

Publication date
April 18, 2008

Studying