An emulation model for sequential ATPG-based bounded model checking

Bounded model checking based on sequential ATPG (automatic test pattern generation) is virtually the sequential ATPG state-justification phase. The state-justification phase is a very complicated and expensive process in term of CPU time. Previous work to speed the search concentrated on developing heuristics to achieve speed-up. In this paper we develop a novel architecture to emulate the state-justification on reconfigurable hardware. The feature of fine-grain massive parallelism of reconfigurable hardware is exploited to achieve speed-up.