Post-silicon fault localisation using maximum satisfiability and backbones

Charlie Shucheng Zhu, Georg Weissenbacher, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

52 Scopus citations


The localisation of faults in integrated circuits is a challenging problem and a dominating factor in the overall verification effort. Electrical bugs, in particular, surface only in the fabricated prototypes, leading to behaviour deviating from the golden model. Limited observability complicates their localisation: Logging mechanisms such as trace buffers allow us to retain only a limited execution history. A symbolic analysis of the RTL design can find discrepancies between the values recorded in the trace buffer and the intended behaviour. Contemporary MAX-SAT solvers are then able to identify a maximal subset of the RTL design that is consistent with the observed behaviour. The elements in the complement of this subset represent potential locations of the fault. The scalability of contemporary decision procedures dictates the size of a window of execution cycles which we can analyse using symbolic techniques. Current MAX-SAT-based fault localisation techniques require this window to span the fault as well as the error it causes. To address the scalability issues resulting from large window sizes, we propose to slide a smaller window along the temporal axis, constraining it with the information recorded in the trace buffer for the respective execution cycles. In this scenario, the localisation attempt may fail: The limited information provided by the trace buffer may be insufficient to pin down the exact temporal and spatial location of the fault. We propose to use backbones to identify information that can be propagated across sliding windows. The backbone of a symbolic representation of a circuit is the set of signals that are immutable under the given constraints (e.g., the output and trace buffer values). This additional information has several benefits: Firstly, it may be instrumental in locating the fault. Secondly, it may enable a reduction of the size of the of trace buffers and the sliding window. Our preliminary experimental results demonstrate that the use of backbones allows us to reduce the size of the sliding windows or the trace buffer.

Original languageEnglish (US)
Title of host publication2011 Formal Methods in Computer-Aided Design, FMCAD 2011
Number of pages4
StatePublished - 2011
Event2011 Formal Methods in Computer-Aided Design, FMCAD 2011 - Austin, TX, United States
Duration: Oct 30 2011Nov 2 2011

Publication series

Name2011 Formal Methods in Computer-Aided Design, FMCAD 2011


Other2011 Formal Methods in Computer-Aided Design, FMCAD 2011
Country/TerritoryUnited States
CityAustin, TX

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'Post-silicon fault localisation using maximum satisfiability and backbones'. Together they form a unique fingerprint.

Cite this