Invariant checking method and apparatus using binary decision diagrams in combination with constraint solvers

In a computer system comprising a processor, I/O control circuitry, an input unit, an output unit, a memory coupled to the processor, and a computer readable medium containing instructions which when executed by the processor causes the computer system to implement an invariant checking method, said computer system performs 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 path, 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.

An invariant checking apparatus for determining whether a system property is an invariant of a system based on system input descriptions, said invariant checking apparatus comprising:

• an input section for receiving a system description and a system property;
• a processor for performing the steps of:
• 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 path, 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;
• and
• an output unit showing a counterexample when said system property is not an invariant of said system description.