Formal Verification for RTL and TLM Designs
- JiNian Bian - Dept of Computer Science and Technology, Tsinghua University, Beijing, P. R. China
- Data e ora
- venerdì 12 settembre 2008 alle ore 14.15 - Inizio alle 14:30, Caffè e biscotti alle 14:15.
- Ca' Vignal 3 - Piramide, Piano 0, Sala Verde
- Maria Paola Bonacina
- Referente esterno
- Data pubblicazione
- 18 aprile 2008
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.