Symbolic model checking with dynamic model pruning
US6643827B1 · kind B1 · utility
Assignee
Inventor
Key dates
| Filing date | Sep 30, 2000 |
| Grant date | Nov 4, 2003 |
| Priority date | — |
| Expiry date | Feb 9, 2022 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Formal verification methods provide for improved efficiency of popular binary decision diagram (BDD) based algorithms. A lazy pre-image computation method builds new transition relation partitions on-demand for relevant internal variables of a state predicate, and conjoins only next state relations for relevant internal variables to a pre-image including the state predicate. A lazy fixpoint computation method makes iterative use of lazy pre-image computation to compute conditions that must be satisfied to produce a given set of states. A forward assumption propagation method generates assumptions to characterize a set of interesting states for a property being evaluated at one or more evaluation stages. A dynamic transition relation reduction improves the efficiency for symbolic model checking by reducing transition relations under assumptions dynamically generated from properties being evaluated. These methods provide symbolic model checking of circuits and other finite state systems previously too large to be completed successfully using BDD based algorithms.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.