SYSTEM AND METHOD FOR REACTIVE INITIALIZATION BASED FORMAL VERIFICATION OF ELECTRONIC LOGIC DESIGN

摘要

A system and method use reactive initialization to facilitate formal verification of an electronic logic design. The system verifies that a part of the logic design correctly transitions through a sequence of states by automatically assigning an initial state value. The system interacts with a correction-unit to provide meaningful feedback of verification failures, making it possible for the correction-unit to correct the failures or add new constraints that allow the verification to complete. Assigning an initial state simplifies the verification of the validity of the remaining states in the sequence, thus making it more likely to reach a conclusive result and consuming less computing resources.

主权项

1. An automated method, implemented as design verification software running on a computer system, of formally verifying a set of properties expressing intended logic behavior of an integrated circuit, the verification software including a correction unit for reactive initialization, comprising:
receiving, by a data storage accessible to a processor, a description of at least a portion of an integrated circuit design to be formally verified, a set of properties of the design to be verified, and a set of constraints, wherein the properties are restricted to any sequence of events that would indicate a failure; analyzing the description by the processor with respect to each property determining reachability of a specific state from a given initial state under conditions specified by the constraints, the analysis being conducted locally over a set of sub-designs from the received description, such thata) reaching the specified state through the sequence dictated by the property being reported as a failure for the sub-design and the given initial state, andb) failing to reach the specified state through the sequence dictated by the property being reported as a pass of the analysis for the sub-design and the given initial state;
identifying invariant signals, whenever a failure of the analysis is reported, from the set of conditions leading to the failure; adding a constraint corresponding to the identified invariant signals, and re-analyzing with the added constraint until reachability is determined.