A common approach to test generation and hardware verification based on temporal logic

Abstract

Hardware verification and sequential test generation are aspects of the same problem, namely to prove the equal behavior determined by two circuit descriptions. During test generation, this attempt succeeds for the faulty and fault free circuit if redundancy exists, and during verification it succeeds, if the implementation is correct with regard to its specification. This observation can be used to cross-fertilize both areas, which been treated separately up to now. In this paper, a common formal framework for hardware verification and sequential test pattern generation is presented, which is based on modeling the circuit behavior with temporal logic. In addition, a new approach to cope with non resetable flipflops in sequential test generation is proposed, which is not restricted to stuck-at faults. Based on this verification view, it is possible to provide the designer with one tool for checking circuit correctness and generating test patterns. Its first implementation and application is also described.