Automatic symbolic indexing methods for formal verification on a symbolic lattice domain

摘要

Processes for formal verification of circuits and other finite-state systems are disclosed. For one embodiment, a process is disclosed to provide for significantly reduced computation through automated symbolic indexing of a property assertion and to compute the satisfiability of the property assertion directly from a symbolic simulation of the indexed property assertion. For an alternative embodiment a process using indexed property assertions on a symbolic lattice domain to represent and verify properties, provides an efficient symbolic manipulation technique using binary decision diagrams (BDDs). Methods for computing symbolic simulations, and verifying satisfiability may be applicable with respect to property assertions that are symbolically indexed under specific disclosed conditions. A process is also disclosed to compute a constraint abstraction for a property assertion, thereby permitting automated formal verification of symbolically indexed properties under constraints and under specific conditions, which may be automatically checked.