Mining Global Constraints With Domain Knowledge for Improving Bounded Sequential Equivalence Checking
Weixin Wu, Michael S. Hsiao · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2007
We present a novel technique on mining relationships in a sequential circuit to discover global constraints. We utilize domain knowledge to prune the search space for our mining process, via which the mined relations may often span several time frames, thus improving the deductibility of the problem instance. Experimental results demonstrate that the application of these global constraints to satisfiability (SAT)-based bounded sequential equivalence checking can achieve a one to two orders-of-magnitude speedup.