Much effort is spent by programmers everyday in trying to reduce long, failing execution traces to the cause of the error. We present an algorithm for error cause localization based on a reduction to the maximal satisfiability problem (MAX-SAT), which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisfied by an assignment. At an intuitive level, our algorithm takes as input a program and a failing test, and comprises the following three steps. First, using bounded model checking, and a bound obtained from the execution of the test, we encode the semantics of a bounded unrolling of the program as a Boolean trace formula. Second, for a failing program execution (e.g., one that violates an assertion or a post-condition), we construct an unsatisfiable formula by taking the formula and additionally asserting that the input is the failing test and that the assertion condition does hold at the end. Third, using MAX-SAT, we find a maximal set of clauses in this formula that can be satisfied together, and output the complement set as a potential cause of the error.

Logic synthesis for soft error mitigation is increasingly important in a wide range of applications of FPGAs. We present R2, an algorithm for rewiring a post-layout LUT-based circuit that reduces the overall criticality of the circuit, where criticality is the fraction of primary inputs that lead to observable errors at the primary outputs if an single event upset inverts a configuration bit. Our algorithm explicitly optimizes the robustness of the interconnect, the dominant component of FPGAs. The key idea of R2 is to exploit Boolean flexibilities in the circuit implementation to replace wires with high criticality with those with lower criticality while preserving the circuit functionality. We estimate criticalities using a Monte Carlo fault simulation. We represent flexibilities using SPFDs (Set of Pairs of Functions to be Distinguished), and use criticality information to choose candidates for rewiring, assigning the maximum flexibility to high criticality wires. Compared to IPR, a recent robust logic optimization, our implementation increases MTTF (Mean Time to Failure) by 24%, showing for the first time, the advantages of exploiting Boolean flexibilities in optimizing for robustness. In addition, R2 achieves 5% and 2% more reduction on the number of wires and LUTs in an FPGA than that obtained by the existing rewiring algorithm for area minimization.

Power and fault tolerance are deemed to be two orthogonal optimization objectives in FPGA synthesis, with independent attempts to develop algorithms and CAD tools to optimize each objective. In this paper, we study the relationship between these two optimizations and show empirically that there are strong ties between them. Specifically, we analyze the power and reliability optimization problems in FPGA physical synthesis (i.e., packing, placement, and routing), and show that the intrinsic structures of these two problems are very similar. Supported by the post routing results with detailed power and reliability analysis for a wide selection of benchmark circuits, we show that with minimal changes - fewer than one hundred lines of C code - an existing power-aware physical synthesis tool can be used to minimize the fault rate of a circuit under SEU faults. As a by-product of this study, we also show that one can improve the mean-time-to-failure by 100% with negligible area and delay overhead by performing fault-tolerant physical synthesis for FPGAs. The results from this study show a great potential to develop CAD systems co-optimized for power and fault-tolerance.