Back to results
US 7,031,896 B1Granted
Methods for performing generalized trajectory evaluation
AssigneeIntel Corporation
InventorJin Yang
Life of this patent
Estimating the term…
Loading patent…
Loading patent…
AssigneeIntel Corporation
InventorJin Yang
Estimating the term…
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.
A computer software product including one or more recordable media having executable instructions stored thereon which, when executed by a processing device, causes the processing device to strengthen a first antecedent label for an edge in an assertion graph, wherein strengthening the antecedent label comprises causing the processing device to:
A computer-implemented method comprising strengthening a first antecedent label for an edge in an assertion graph, wherein strengthening the antecedent label comprises:
A verification system comprising means for strengthening a first antecedent label for an edge in an assertion graph, wherein the means for strengthening the antecedent label comprises:
A verification system comprising:
A verification system comprising:
A computer-implemented method comprising:
Dependencies are inferred from the claim text.