Abstract:A gate-level software-based self-testing method based on bounded model checking is proposed in this paper. The module in processor is abstracted and simplified into a constrained module to alleviate the state explosion problem. Then, the trigger conditions for unpredictable faults are transformed into properties one by one, and the bounded model checking is used to search violations which trigger these properties. Finally, the violation is mapped into the sequence of test instructions, and a sequence of observation instructions is added to form a self-test program. The experimental results show that the method can effectively test the faults which are difficult to be tested in the controller but without causing the state explosion problem, and improve the test quality of online test.