| ［1］Lu F, Cheng K. Sequential Equivalence Checking Based on K-th Invariants and Circuits SAT Solving［C］// Proceedings of the High-Level Design Validation and Test Workshop'05. New York: IEEE, 2005: 45-52.
［2］Kuehlmann A. Dynamic Transition Relation Simplification for Bounded Property Checking［C］// Proceedings of the 2004 IEEE/ACM International Conference on Computer Aided Design. New York: IEEE, 2004: 50-57.
［3］张海宾, 段振华. 多速率混合系统的模型检查［J］. 西安电子科技大学学报, 2008, 35(1)：60-64.
Zhang Haibin, Duan Zhenhua. Model Checking Multirate Hybrid Systems ［J］. Journal of Xidian University, 2008, 35(1)：60-64.
［4］郭建，金乃咏. 模型检验中对CTL公式的空属性探测［J］. 西安电子科技大学学报, 2007, 34(5): 794-799.
Guo Jian, Jin Naiyong. Vacuity Detection in Computation Temperal Logic ［J］. Journal of Xidian University, 2007, 34(5): 794-799.
［5］Cook S. The Complexity of Theorem Proving Procedures［C］//ACM SIGACT Symposium on the Theory of Computing. New York: ACM, 1971: 151-158.
［6］Kuehlmann A, Ganai M K, Paruthi V. Circuit Based Boolean Reasoning［C］//Proceedings of the 38th annual Design Automation Conference. New York: ACM, 2001: 232-237.
［7］Kuehlmann A, Paruthi V, Krohm F, et al. Robust Boolean Reasoning for Equivalence Checking and functional Property Verification［J］. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 2002, 21(12): 1377-1394.
［8］Lu F, Wang L, Cheng K, et al. A Circuit SAT Solver with Signal Correlation Guided Learning［C］//Proceedings of the Conference on Design, Automation and Test in Europe. Washington: IEEE Computer Society, 2003: 892 - 897.
［9］Lu F, Wang L, Cheng K, et al. A Signal Correlation Guided ATPG Solver and Its Applications for Solving Difficult Industrial Cases［C］//Proceedings of the 40th annual Design Automation Conference. New York: ACM, 2003: 436-441.
［10］Biere A. AIGER (AIGER is a format, library and set of utilities for And-inverter Graphs (AIGs)) ［CP/OL］.［2008-09-30］. http://fmv.jku.at/aiger/.
［11］Altera Corp. Quartus II University Interface Program ［CP/OL］.［2008-09-10］. http://www.altera.com/education/univ/research/unv-quip.html.
［12］Pistorius J, Hutton M, Mishchenko A, et al. Benchmarking Method and Designs Targeting Logic Synthesis for FPGAs［C］// Proceedings of the ACM/IEEE International Workshop on Logic and Synthesis. New York: IEEE, 2007: 230-237.
［13］Berkeley Logic Synthesis and Verification Group. ABC: a System for Sequential Synthesis and Verification. Release 70930［CP/OL］.［2008-10-22］. http://www.eecs.berkeley.edu/ alanmi/abc.
［14］Eén N, Srensson N. An Extensible Sat-solver［C］//SAT 2003, LNCS: 2919. Berlin: Springer, 2004: 333-336.
［15］PicoSAT［CP/OL］.［2008-10-22］. http://fmv.jku.at/picosat/. |
