Formal Verification Aware Redundant Sequential Logic Optimization to Improve Design Utilization

With continuous advancement in technology, semiconductor industry is moving towards lower process nodes to improve transistor density, performance, and power optimization. For lower nodes, fabrication gets costlier and area reduction is of prime importance. To align with this goal, while doing physical implementation one of the key targets is to synthesize design with most optimal logic and less redundant functional logic. Even though synthesis tools are optimized to align with customers target, there are limitations. Identification of such redundant logic is possible both in synthesis and formal verification tools. This paper presents novel algorithm and process to identify redundant logic using Formal Verification tool and use this data to generate ECO such that synthesis tool can optimize logic better than current known methods. Using proposed solution, 1K to 38K reduction in sequential cell count and 4K to 85K overall cell count reduction has been observed for various design cases. This solution provides logic area and power saving without compromising on design testability and formal verification at the cost of runtime increase.