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

fYear

2001

fDate

2001

Firstpage

190

Lastpage

193

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;

fLanguage

English

Publisher

ieee

Conference_Titel

ASIC, 2001. Proceedings. 4th International Conference on

Conference_Location

Shanghai

Print_ISBN

0-7803-6677-8

Type

conf

DOI

10.1109/ICASIC.2001.982529

Filename

982529