The verification of circuit design is to check its correctness and safety, which is vital in the circuit design process and occupies almost half of the cost and time. Formal verification is one of the important ways to guarantee the correctness and safety of software and hardware systems of computers and has been applied to circuit design verification. The electronic design automation (EDA) software from three global EDA giants, i.e., Cadence, Synopsis, and Siemens, all includes mature formal verification tools for circuit design. This paper summarizes the current status of the formal verification of circuit design, analyzes its challenges, discusses its perspectives and trends, and proposes suggestions on its development in China.