Patent Document ID: 8862439
Application ID: 12824081
Patent Flag: 1

Claim One:
1. A method for verifying a design of a system, the method comprising: receiving a high level design description of a design for a system; extracting a set of logical formulas from the high level design description of the design, wherein the logical formulas are clauses of quantifier-free linear arithmetic; and determining satisfiability of the set of logical formulas including searching in a space of non-Boolean structures for a satisfying assignment to the logical formulas, including generating a sequence of mutations to a structure according to a prescribed rule, wherein the structure is an assignment of numeric values to variables occurring in the logical formulas; and deducing one or more new logical formulas in response to one or more conflicts in the searching in the space of non-Boolean structures for the satisfying assignment, including applying a shadow rule, wherein the shadow rule is a deduction rule that resolves conflicts in the assignment of numeric vales to variables by generating a new clause defining a feasible set of values for a variable from the intersection of feasible sets of values for the variable from a pair of compatible clauses; wherein one or more of the receiving, extracting, or determining are performed with a processor.