Sciweavers

Share
ICCAD
2007
IEEE

Computation of minimal counterexamples by using black box techniques and symbolic methods

9 years 11 months ago
Computation of minimal counterexamples by using black box techniques and symbolic methods
— Computing counterexamples is a crucial task for error diagnosis and debugging of sequential systems. If an implementation does not fulfill its specification, counterexamples are used to explain the error effect to the designer. In order to be understood by the designer, counterexamples should be simple, i.e. they should be as general as possible and assign values to a minimal number of input signals. Here we use the concept of Black Boxes — parts of the design with unknown behavior — to mask out components for counterexample computation. By doing so, the resulting counterexample will argue about a reduced number of components in the system to facilitate the task of understanding and correcting the error. We introduce the notion of ‘uniform counterexamples’ to provide an exact formalization of simplified counterexamples arguing only about components which were not masked out. Our computation of counterexamples is based on symbolic methods using AIGs (And-Inverter-Graphs)....
Tobias Nopper, Christoph Scholl, Bernd Becker
Added 16 Mar 2010
Updated 16 Mar 2010
Type Conference
Year 2007
Where ICCAD
Authors Tobias Nopper, Christoph Scholl, Bernd Becker
Comments (0)
books