Synopsys, Inc.
Automated Debug of Falsified Power-Aware Formal Properties using Static Checker Results

Abstract:

A power intent specification specifies the desired power intent for a design of an integrated circuit, for example the states of the power domains under different conditions. Power-aware formal properties describe desired behaviors specified by the power intent specification. Falsified power-aware formal properties indicate that the design does not exhibit the desired behavior. In addition, a debug context database contains debug contexts for static-check violations resulting from power-aware static checking of the design. Static checking checks for compliance with the power intent specification based on a static structure of the design. Falsified power-aware formal properties ae matched against the static-check violations. A data structure is generated, associating debug contexts for the matching static-check violations as possible causes of the falsified power-aware formal properties.