Utilizing an unsat proof for model checking

Abstract

A proof of unsatisfiability associated with a bounded model may be extended to apply to another bounded model having a larger bound. In some exemplary embodiments, an unbounded model may be proved using one or more such extensions. A proof may be reordered in order to decrease its size and increase the productivity of systems that utilize it. The proof may be reorder by a natural temporal order of cycles.

Description

BACKGROUND[0001]The present disclosure relates to model checking, in general, and to SAT-based model checking, in particular.[0002]State of the art computerized components are very complex and require extensive quality assurance checks. One of the commonly used techniques is formal verification in which the computerized component is modeled and is examined by a model checker. The model describes all possible behaviors of the computerized component based on inputs from the environment and calculations performed by the computerized component itself. Most components are represented by cycled models in which the state of the component may differ from one cycle to the other. It will be noted that the computerized component may be a software component, firmware component, hardware component or the like. It will be further noted that in some cases the component to be verified may be a business method, user interaction, communication protocol or any other form of activity or computation tha...

AI Technical Summary

Benefits of technology

[0015]In some exemplary embodiments, the method further comprises eliminating double pivot variables from the comb.

Problems solved by technology

State of the art computerized components are very complex and require extensive quality assurance checks.

While the BMC may falsify the specification property by determining that in a given one or more cycles the specification property is not held, it cannot prove that the specification is held for the model, as the number of cycles is bounded.

Although BMC engines are usually faster and more efficient than other types of model checking engines, they are unable to provide a proof that the model holds the specification property in each and every possible behavior.

Images