Sequential circuits test generation using GTL

The algorithm, which avoids drawbacks of conventional approaches, has been presented for not resetable lines using GTL(Global Temporal Logic). This model checking algorithm are subject to constant improvement so that the size of manageable circuits will future increased. In this paper, based on the global temporal logic that defined by forward and reverse operator, a common formal framework for test generation is presented. In addition, heuristic for accelerating the testing process and implementation are given.