FWF - QUAINT - Quantified Decision Procedures and Interpolation for Error Correction

  • Hofferek, Georg, (Co-Investigator (CoI))
  • Könighofer, Robert, (Co-Investigator (CoI))
  • Bloem, Roderick (Principal Investigator (PI))

Project: Research project

Project Details

Description

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.
StatusFinished
Effective start/end date1/01/1230/09/15

Research Output

  • 7 Conference contribution
  • 1 Doctoral Thesis

Controller Synthesis with Uninterpreted Functions

Hofferek, G., 2014

Research output: ThesisDoctoral Thesis

Open Access
File

How to Handle Assumptions in Synthesis

Bloem, R. P., Ehlers, R., Jacobs, S. & Könighofer, R., 2014, Proceedings 3rd Workshop on Synthesis. Electronic Proceedings in Theoretical Computer Science, Vol. 157. p. 34-50 (EPTCS).

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

Open Access
File

SAT-based methods for circuit synthesis

Bloem, R. P., Egly, U., Klampfl, P., Könighofer, R. & Lonsing, F., 2014, Formal Methods in Computer-Aided Design. Institute of Electrical and Electronics Engineers, p. 31-34

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

Open Access
File