Methods for performing generalized trajectory evaluation

摘要

Methods for formal verification of circuits and other finite-state systems are disclosed. Formal definitions and semantics are disclosed for a model of a finite-state system, an assertion graph to express properties for verification, and satisfiability criteria for specification and automated verification of forward implication properties and backward justification properties. A method is disclosed to perform antecedent strengthening on antecedent labels of an assertion graph.;A method is also disclosed to compute a simulation relation sequence ending with a simulation relation fixpoint, which can be compared to a consequence labeling for each edge of an assertion graph to verify implication properties properties according to the formal semantics. An alternative method is disclosed to compute the simulation relation sequence from the strengthened antecedent labels of an assertion graph, thereby permitting automated formal verification of justification properties.;Finally methods are disclosed to significantly reduce computation through abstraction of models and assertion graphs and to compute an implicit satisfiability of an assertion graph by a model from the simulation relation computed for the model and assertion graph abstractions. Other methods and techniques are also disclosed herein, which provide for fuller utilization of the claimed subject matter.