In spite of all the effort that goes into verification, the design of integrated circuits has become so complex that critical bugs often make their way into in silicon. Since respins are prohibitively expensive for all but show-stopping bugs, there is often a need for software workarounds for hardware bugs in systems involving both hardware and software components. In QUAINT, we propose to develop automatic methods to construct such workarounds.
We will study the repair problem from two sides. On the one hand, we will develop methods to model hardware bugs in such a way that the search for a software workaround is feasible. The tasks include fault localization and solving formulas for a valid repair. Following previous work, we view the repair problem as a game played by two players (the environment and the system) with opposite interests (to violate and to fulfill the specification, resp.). Thus, the repair problem will naturally result in formulas with quantifier alternations. However, modifications are needed to consider available hardware constraints.
The second goal is to develop novel methods to evaluate such formulas efficiently and to extract repairs from them. Here, we will use our existing expertise in interpolation for function extraction and quantifier elimination to speed up QBF solving and to generate certificates that allow for efficient repairs. We will also study ways to move beyond the bit level, studying quantified formulas in other logics, in particular using equality logic and uninterpreted functions.