Counterexample Generation for Incomplete Designs.
Tobias Nopper, Christoph Scholl · 2007
Counterexample generation is a crucial task for error diagnosis and debugging of sequential circuits. The simpler a counterexample is – i.e. more general and fewer assigned input values – the better it can be understood by humans. We will use the concept of Black Boxes – parts of the design with unknown behavior – to mask out components for counterexample computation. By doing this, the resulting counterexample will argue about a reduced number of components in the system in order to facilitate the task of understanding and correcting the error effect.