Testing a processor in native mode by executing instructions from cache has been shown to be very effective in discovering defective chips. In previous work, we showed an efficient technique for generating instruction sequences targeting specific faults. We generated tests using traditional techniques at the module level and then mapped them to instruction sequences using novel methods. However, in that technique, the propagation of module test responses to primary outputs was not automated. In this paper, we present the algorithm and experimental results for a technique which automates the functional propagation of module level test responses. This technique models the propagation requirement as a Boolean difference problem and uses a bounded model checking engine to perform the instruction mapping. We use a register transfer level (RT-Level) abstraction which makes it possible to express Boolean difference as a succinct linear time logic (LTL) formula that can be passed to a bounded model checking engine. This technique fully automates the process of mapping module level test sequences to instruction sequences.
展开▼
