Sequential equivalence checking using a hybrid boolean-word level decision diagram

Abstract

By increasing the complexity of system on a chip (SoC) formal equivalence checking has become more and more important and a major economical issue to detect design faults at early stages of the design cycle in order to reduce time-to-market as much as possible. However, lower level methods such as BDDs and SAT solvers suffer from memory and computational explosion problems to match sizes of industrial designs in formal equivalence verification. In this paper, we describe a hybrid bit- and word-level canonical representation called Linear Taylor Expansion Diagram (LTED) [1] which can be used to check the equivalence between two descriptions in different levels of abstractions. To prove the validity of our approach, it is run on some industrial circuits with application to communication systems and experimental results are compared to those of Taylor Expansion Diagram (TED) which is also a word level canonical representation [2]. © 2008 Springer-Verlag.