Patent ID: 8166430

Claim:
A computer-implemented method of functional verification of a digital circuit, wherein the digital circuit is checked with a set of properties representing a functioning of the digital circuit, wherein a quality factor of the set of properties has a predetermined value and wherein the properties determine a value series of internal values and output values for an input pattern, the input pattern comprising a temporal sequence of values of input values and an initial value of its internal values, the method comprising: a) Determining an existence of at least one subset of interrelated properties (P 0 , P 1 , . . . P n ); b) Checking by a computer whether a value of a predetermined expression Q(t) is uniquely determined for at least one input pattern at at least one time point by means of an interaction of the least one subset of interrelated properties, whereby at said time point the value of the predetermined expression Q(t) is not uniquely determined by individual ones of the properties and wherein the predetermined expression is only dependent on values of the input values and the output values and the output values at time points; and c) Outputting by a computer the quality factor based on said Q(t).