Mining global constraints for improving bounded sequential equivalence checking

In this paper, we propose a novel technique on mining relationships in a sequential circuit to discover global constraints. In contrast to the traditional learning methods, our mining algorithm can find important relationships among several nodes efficiently. The nodes involved may often span several timeframes, thus improving the deductibility of the problem instance. Experimental results demonstrate that the application of these global constraints to SAT-based bounded sequential equivalence checking can achieve one to two orders of magnitude speedup. In addition, because it is orthogonal to the underlying SAT solver, it can help to enhance the efficacy of typical SAT based verification flows. Categories and Subject Descriptors: B.6.3 [Design Aids]: Verification General Terms: Verification, Algorithms

• Type: Conference
• Year: 2006
• Where: DAC
• Authors: Weixin Wu, Michael S. Hsiao
• Keywords: Computer Architecture, DAC 2006, Global Constraints, Sequential Circuit, Sequential Equivalence Checking