Sciweavers

Share
DAC
2006
ACM

Mining global constraints for improving bounded sequential equivalence checking

9 years 6 months ago
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
Weixin Wu, Michael S. Hsiao
Added 13 Jun 2010
Updated 13 Jun 2010
Type Conference
Year 2006
Where DAC
Authors Weixin Wu, Michael S. Hsiao
Comments (0)
books