Patent ID: 6131078
Filing Date: 2000-10-10
Classification: G06F

Abstract:
In a computer system, a method of verifying that a system S satisfies certain predetermined constraints representing specifications of said system S, wherein said system S comprises a collection of interconnected objects such as found in an electric circuit, and wherein satisfying said constraints signifies proper functioning of said system S, said method comprising the steps of:a. providing a representation of the system S and said constraints in a form sufficient to reveal their structure;b. creating a quantified Boolean formula identified as G representative of said system S and its constraints;c. storing said formula G in a storage medium of said computer system;d. making reference to said representation of said system S and its constraints, creating therefrom a collection of quantified Boolean formulae Q.sub.S, said collection having at least G contained therein, wherein each subsequent Boolean formula is created from a previously created Boolean formula in said collection Q.sub.2 and wherein the additional quantified Boolean formulae in addition to said quantified Boolean formula G are created without selected variables and quantifiers that were contained in the previously created quantified Boolean formula in said collection Q.sub.S, said selected variables and quantifiers corresponding to one or more objects and constraints of said system S;e. storing the last created formula in said collection of quantified Boolean formulae Q.sub.s in a storage medium of said computer system for further processing;f. processing said collection of quantified Boolean formulae Q.sub.S to obtain a result; andg. evaluating said result to determine whether said system S satisfies said constraints and signifying thereby whether said system S is capable of functioning according to said specifications.