Enhancing the Effectiveness of STLs for GPUs via Bounded Model Checking

Graphics Processing Units (GPUs) are becoming widespread, even in safety-critical applications. In that case, it is imperative to guarantee that the probability of producing critical failures due to hardware faults is lower than a given threshold. To detect possible permanent hardware faults as soon as they appear during the operational phase (e.g., due to aging), Software Test Libraries (STLs) have gained significant traction as a widely adopted test solution due to their effectiveness in terms of fault detection capabilities, test application time, and flexibility. However, a major drawback of this solution is the lack of automation in the STL generation phase. As a result, high manual labor is required for their generation. This becomes even more arduous in complex architectures that require in-depth knowledge to cover hard-to-test faults. In this paper, we introduce a methodology based on Bounded Model Checking to support the generation and improvement of stuck-at-oriented STLs for hard-to-test units in GPUs, showing that we can enhance the test coverage achieved by pre-existing STLs while also identifying a set of functionally untestable faults. To experimentally validate the proposed method’s effectiveness, we use the FlexGripPlus GPU model to target two hard-to-test units, one medium to low complexity sub-unit and one high complexity sub-unit, as study cases. For both units, we had pre-existing STLs written for the stuck-at model. Resorting to the proposed method, the STLs’ test coverage was increased by 9.57% and 2.19%, respectively. In addition, the method also identified a significant number of functionally untestable faults.