SAT-based techniques for determining backbones for post-silicon fault localisation

The localisation of faults in integrated circuits is a dominating factor in the overall verification effort. The limited observability of internal signals of chips complicates the spatial and temporal localisation of bugs in post-silicon validation. We address the problem of recovering the values of unobservable signals of a chip prototype from state bits recorded in a trace-buffer of limited size using a SAT-based analysis. Our technique is a novel application of backbones. This term refers to the set of parameters of a Boolean function that need to be fixed to a constant value for that function to evaluate to true. There is a range of known SAT-based techniques targeting this problem. We discuss a number of existing techniques and gradually extend these techniques with novel ideas, leading to novel and previously unstudied algorithms. We evaluate the performance of these algorithms using the aforementioned application in post-silicon validation. Our results show that these SAT-based techniques are suitable for large-scale applications with even millions of variables. Moreover, we evaluate the utility of backbones by quantifying the restored state bits in a number of case studies, including two processor cores.