Using Formal Methods to Support the Development of STLs for GPUs

Graphics Processing Units (GPUs) boost the development of high-performance safety-critical applications. The reliability of such systems is of utmost importance since faults affecting the hardware may occur at any time during the systems' operational life. Thus, methods to effectively test these devices during their in-field operation are necessary. One popular solution relies on Software Test Libraries (STLs), which recently have been started being used for GPUs as well, since they are effective in terms of fault detection capabilities, intrusiveness, flexibility, and test duration. A drawback of the STL approach for GPUs is the extensive effort used to develop effective test routines for complex structures, e.g., controllers, due to the complicated constraints stemming from the ISA, the available compilation flows and parallelism constraints. We propose a novel technique based on formal methods to support the generation of stimuli and enhance the quality of pre-existing STLs for GPUs. To validate the proposed method, we resort to an open-source GPU model (FlexGripPlus). Experimental results show that the method can effectively generate complementary code fragments to be added to existing STLs and increase their fault coverage. In the case of the GPU's decoding unit, the stuck-at fault coverage was increased by nearly 10%.