Methods for performing generalized trajectory evaluation
US7031896B1 · kind B1 · utility
Assignee
Inventor
Key dates
| Filing date | Jun 30, 2000 |
| Grant date | Apr 18, 2006 |
| Priority date | — |
| Expiry date | Oct 21, 2022 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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 com…
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.