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). Experimental results using a VLIW processor as a case study clearly demonstrate our capability of providing simplified counterexamples.