Using Formal Methods to Support the Development of STLs for GPUs

• Main Authors: Deligiannis, Nikolaos I., Faller, Tobias, Rodriguez Condia, Josie E., Cantoro, Riccardo, Becker, Bernd, Reorda, Matteo Sonza
• Format: Conference Proceeding
• Language: English
• Subjects: Computer architecture; Flexible printed circuits; Formal Methods; Graphics processing units; Graphics Processing Units (GPUs); Libraries; Parallel processing; Parallel programming; Software; Software Test Libraries; Test Quality
• ISSN: 2377-5386
• DOI: 10.1109/ATS56056.2022.00027

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 G PU s as well, since they are effective in terms of fault detection capabilities, intrusiveness, flexibility, and test duration. A drawback of the STL approach for G PU s 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 (Flex GripPlu s). 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%.