Patent ID: 7516109

Claim:
A computer-implemented method for verifying the behavior of a digital system, said method comprising, receiving a constraint graph with directed arcs, each said directed arc being labeled with a Boolean formula, said constraint graph having at least one accepted path, each accepted path in said constraint graph being labeled with a sequence of Boolean formulas describing a disallowed pattern of behavior of said digital system; receiving a list of non-visible signals; starting with said constraint graph, performing for each non-visible signal in the list of non-visible signals: (a) performing either (a1) all possible resolutions of equal-length directed paths within the constraint graph of said non-visible signal or (a2) selected resolutions of equal-length directed paths within the constraint graph of said non-visible signal; (b) deleting all arcs in a resulting constraint graph that are labeled with a Boolean formula that mentions said non-visible signal; (c) deleting all arcs in the resulting constraint graph that are no longer on a directed path from an original initial node of the constraint graph to an original terminal node of the constraint graph; supplying the resulting constraint graph to a constraint-based simulator; supplying input values to said constraint-based simulator; using said input values and constraints accepted by said constraint graph to calculate output values; responding to a user query about a particular output value by determining the input values and the constraint, or constraints, used to calculate said output value; and supplying to the user said input values and said constraint, or constraints.