Alignability equivalence of synchronous sequential circuits

Sequential verification is a well known research framework that has attracted many researchers in the aca demic and industrial worlds during the last few decades. In this framework, initialization of synchronous models is one of the fundamental and challenging research topics that is difficult to solve, especially when talking about large industrial strengths hardware models. Many researchers in this domain such as Pomeranz and Reddy (1994), Pixley and Beihl (1991), and Pixley, Jeong and Hachtel (1994), and others tried to analyze and propose solutions to this problem, however the majority of the approaches used were based on BDDs and classical reachability analysis methods, which by nature suffer from capacity and complexity limits. When talking about hardware formal equivalence verification, the Initialization issue becomes even more complex especially when trying to verify the logic equivalence of two large industrial circuits. In this note we propose a new adaptive and iterative approach that combines various symbolic simulation techniques and bounded model checking algorithms to initialize sequential circuits for the alignability equivalence verification. The novelty of our method has been employed on complex real life sequential models from Intel lead Pentium processor designs. These methods are already implemented in Intel´s sequential verification engine, Insight.