[1] [1] BRAND D. Verification of large synthesized designs ［C］ // Proceed Int Conf Comput Aided Design (ICCAD). Santa Clara, CA, USA. 1993: 534-537.

[3] [3] DAVIS M, PUTNAM H. A computing procedure for quantification theory ［J］. J ACM (JACM), 1960, 7(3): 201-215.

[4] [4] MARQUES-SILVA J, LYNCE I, MALIK S, et al. Handbook of satisfiability ［M］. Amsterdam: IOS Press, 2021: 133-182.

[5] [5] BRAYTON R, MISHCHENKO A. ABC: an academic industrial-strength verification tool ［C］ // Int Conf Comput Aided Verific. Edinburgh, Uk. 2010: 24-40.

[9] [9] GOERING R. Synopsys pushes formal tools into mainstream ［Z］. Electronic Engineering Times, 1998.

[10] [10] KURSHAN B. FormalCcheck user's manual ［Z］. San Jose: Cadence Design, 1998.

[11] [11] Mentor FormalPro training is designed to help you dramatically reduce the time required to verify ASICS and Ics ［Z］. Wilsonville: Mentor Graphics, 2017.

[13] [13] KUEHLMANN A. The best of ICCAD: 20 years of excellence in computer-aided design ［M］. Boston: Springer, 2003: 65-72.

[15] [15] MOSKEWICZ M W, MADIGAN C F, ZHAO Y, et al. Chaff: engineering an efficient SAT solver ［C］ // Proceed 38th Annual Design Autom Conf. Las Vegas, NV, USA. 2001: 530-535.

[16] [16] ZHANG H, STICKEL M. Implementing the Davis-Putnam method ［J］. J Automated Reasoning, 2000, 24(1): 277-296.

[17] [17] BROWNE C B, POWLEY E, WHITEHOUSE D, et al. A survey of Monte Carlo tree search methods ［J］. IEEE Trans Comput Intellig & AI in Games, 2012, 4(1):1-43.

[18] [18] EéN N, SRENSSON N. An extensible SAT-solver ［C］ // Int Conf Theory Applic Satisfiability Testing. Berlin, Germany. 2003: 502-518.