Equivalence Checking in C-based System-Level Design by Sequentializing Concurrent Behaviors

T. Sakunkonchak, T. Matsumoto, H. Saito, S. Komatsu, and M. Fujita (Japan)


VLSI design and CAD, system-level design, equivalence checking, sequentialization, concurrent behaviors, syn chronization verification


In system-level designs, since many incremental refine ments are applied to the designs, equivalence checking be tween each refinement should be applied. However, prov ing whether two concurrent designs are equivalent is a dif ficult task, not to mention that the concurrent design itself can be error-prone. In this paper, we propose an equiva lence checking method for C-based descriptions of system level designs by sequentializing the concurrent behaviors. Before sequentializing concurrent behaviors, we need to check that the design must not contain neither deadlock nor race condition. After the sequentialization, equiva lence checking is performed by symbolic simulation. To show that our methodology can be applied to practical de signs, we experiment with some SpecC designs developed by University of California Irvine (UCI). The results show that the proposed method is promising. Although the size of some designs are large, with heuristic search for concur rency and synchronization, the size of designs are reduced accordingly and hence we can perform equivalence check ing with the sequentialized ones.

Important Links:

Go Back