6. The method of claim 1 wherein the property checking schema for the said LTL operator F(p) for a given time frame bound comprises: a) starting search from a given start state at time frame i, with a given constraint database, wherein i=0 corresponds to an initial state of the circuit; b) checking for satisfiability of p in the i th state of a path, c) if satisfiable, terminating the search with success; d) if unsatisfiable, learning that p is always false in the i th state and adding this learnt knowledge to a constraint database; e) continuing the search by increasing i until the said time frame bound is reached, and repeating steps b-d; and f) terminating the search inconclusively if the said time frame bound is reached.
1. A method for bounded model checking of arbitrary Linear Temporal Logic (LTL) properties in a verification engine for verification circuits which is capable of bounded model checking the method comprising: in a verification engine, translating by a computer configured by said verification engine LTL properties expressed with one or more LTL operators F(p), G(p), U(p,q) and X(p) into property checking schemas for performing Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator, X represents a next-time operator, p represents either an atomic proposition or a Boolean combination of LTL operators, and q represents either an atomic proposition or a Boolean combination of LTL operators, checking by the said computer the said properties by invoking repeatedly one or more property checking schemas for F(p), G(p), U(p,q) and X(p) operators, and using the results of the checking to indicate if a circuit performs according to the said properties, wherein a subset of the property checking schemas is customized to perform a partitioning of a k th instance of a corresponding bounded model checking problem into multiple smaller Boolean satisfiability sub-problems, wherein the partitioning is performed across said LTL operators, and for each said operator both across time frames and within time frames, wherein when a choice exists about which said operator to check next, the choice is made according to priority determined by degree of difficulty of search estimated to be increasing in the following order: atomic propositions, X operator, F operator, U operator, G operator.