Efficient Generation of Stimuli for Functional Verification by Backjumping Across Extended FSMs

Extended finite state machines (EFSMs) can be efficiently adopted to model the functionality of complex designs without incurring the state explosion problem typical of the more traditional FSMs. However, traversing an EFSM can be more difficult than an FSM because the guards of EFSM transitions involve both primary inputs and registers. This paper first analyzes the hardness of traversing an EFSM according to the characteristics of its transitions. Then, it presents a methodology to generate an EFSM which is easy to be traversed. Finally, it proposes a functional deterministic automatic test pattern generation (ATPG) approach that exploits such EFSMs for functional verification. In particular, the ATPG approach joins backjumping, learning, and constraint solving to (i) early identify possible symptoms of design errors by efficiently exploring the whole state space of the design under verification (DUV), and (ii) generate effective input sequences to be used in further verification steps which require to stimulate the DUV. The effectiveness of the proposed approach is confirmed in the experimental result section, where it is compared with both genetic and pseudo-deterministic techniques.