Title :
EVBCS: new equivalence verification algorithm based on OBDD and circuit structure
Author :
Feng, Lu ; Jinian, Bian ; Hongxi, Xue
Author_Institution :
Comput. Sci. Dept., Tsinghua Univ., Beijing, China
Abstract :
In this paper, an algorithm, EVBCS, for formal verification of combinational logic circuits, is proposed. It combines BDD and structure isomorphism techniques. It also uses a heuristic method to select a set of internal signals (cutline) to reduce the size of BDDs to be created. The algorithm is demonstrated on ISCAS´85 benchmarks using synthesis and optimization tools. The experiment results show that the algorithm is very effective for circuits with structure similarities which are often created by using local synthesis tools and local optimization tools
Keywords :
binary decision diagrams; circuit optimisation; combinational circuits; formal verification; high level synthesis; EVBCS; ISCAS´85 benchmarks; OBDD; circuit structure; combinational logic circuits; equivalence verification algorithm; formal verification; heuristic method; internal signals; local optimization tools; local synthesis tools; optimization tools; structure isomorphism; structure similarities; synthesis tools; Automatic test pattern generation; Binary decision diagrams; Boolean functions; Circuit synthesis; Combinational circuits; Computer science; Data structures; Formal verification; Heuristic algorithms; Signal synthesis;
Conference_Titel :
ASIC, 2001. Proceedings. 4th International Conference on
Conference_Location :
Shanghai
Print_ISBN :
0-7803-6677-8
DOI :
10.1109/ICASIC.2001.982529
