Symbolic variable reduction
US6591400B1 · kind B1 · utility
Assignee
Inventor
Key dates
| Filing date | Sep 29, 2000 |
| Grant date | Jul 8, 2003 |
| Priority date | — |
| Expiry date | Nov 4, 2020 |
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 herein, providing for improved efficiency and capacity of popular binary decision diagram (BDD) based algorithms. A lazy pre-image computation method is disclosed that builds new transition relation partitions on-demand only for relevant next internal variables of a state predicate. A symbolic variable reduction method is disclosed to eliminate variables in a state predicate under “don't care” conditions. Symbolic variable reduction improves the efficiency for symbolic model checking computations especially lazy pre-image based computations providing means to handle very large-scale integrated circuits and other finite state systems of problematic complexity for prior methods. The teachings of these disclosed methods provide for automated 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.