Patent ID: 7058910

Claim:
An invariant checking method for determining whether a system property is an invariant of a system description, said method comprising the steps of: receiving a system description and a system property; transforming said system description and said system property into a model formula comprising variables; eliminating enumerated variables from said model formula and providing a corresponding output formula comprising zero or more integer constraints and residual variables remaining after eliminating said enumerated variables; partitioning said output formula into zero or more integer constraint subsets and into a logic formula by assigning a new logic variable for each of said zero or more integer constraints in said output formula; using a constrained binary decision diagram which is constructed from said logic formula using a heuristic algorithm to provide ordering of said logic variables, said constrained binary decision diagram having at least a true path or a false paths each path comprising said ordering of said logic variables; applying a constraint solver to at least one of said integer constraint subsets corresponding to said ordering of said logic variables within said true path; and determining said system property is not an invariant of the system when said at least one of said integer constraint subsets is satisfiable.