2. The apparatus of claim 1 , wherein the extractor includes a bounded model checker, capable of generating a set of formulas or constraints which is satisfiable if and only if the one or more given properties are guaranteed to hold within a bounded execution sequence.
1. An apparatus for verifying a property of a design for a system, the apparatus comprising: instructions that when executed by a processor provide, a design description interface to receive a design description of the system, including a description of properties to be verified, either as part of the design description or separate from the design description, an extractor in communication with the design description interface, the extractor to extract a plurality of formulas or constraints in response to the design description of the system, a satisfiability solver in communication with the extractor, the satisfiability solver to determine a satisfiability of the plurality of formulas or constraints using a general numeric backtracking algorithm, wherein the satisfiability solver searches in a space of non-Boolean structures for the satisfiability of the plurality of formulas or constraints, an output interface in communication with the satisfiability solver, the output interface to determine whether or not one or more of the given properties are violated, and to put the result of the satisfiability solver in a form of a counterexample suitable to aid in the diagnosis of failures.