Method for validating simulation results of a system as well as equivalence comparison of digital circuits based on said method

Method for equivalence comparison of digital circuits, whereby each digital circuit is described by a plurality of state variables as well as input variables and output variables initially assumed as freely assignable and whenever a difference is found, a counter-example is generated, which is validated for proving inequivalence, by attempt being made,

• to prove initially on the basis of simulations, reachability of the counter-example, by searching for a sequence of samples, which stops the assignment necessary for this sample based on completely unspecified state variables, and
• if this does not succeed in proving non-reachability of this counter-example by an over approximation, by iteratively determining on the basis of the possible target states of the counter-example previous states, from which the target states can be reached, and adding to a quantity of states for such time until no further new states can be added, whereby non-reachability is the case, if not all the states in the quantity of states were reached and therefore the target states of the counter-example cannot be reached by each starting state.