大规模集成电路形式化等价性验证研究进展

In integrated circuit design, the verification time for the correctness can take up to 80 percent of the overall design process. Therefore, investigation into the equivalence checking method between different abstraction layers is indispensable, which can improve the efficiency of equivalence checking and reduce the overall time. This paper first presents a brief introduction on the background and development of formal equivalence checking. Then an analysis of formal equivalence checking methods is given, which including the equivalence between RTL(Register Transfer Level) and its variants and the equivalence between SLM (System Level Model) and RTL. Consequently, the typical formal equivalence checking tools developed by the electronic design company is introduced. Finally, we discuss the challenges that formal equivalence checking now facing, and the directions for future research.