Ravi Surepeddi, Architect, Magma Design Automation, Inc.

ESL to GDSII net-list transformations need validation for its logic correctness at each stage of chip design flow for QOR to be valid and improved and for chip design goals to be met. There are some intricacies in formal equivalence verification, as the verification is compare point (CP)-based and the net-list optimization can be very significant to partition the logic for CP establishment and verify the CP. This paper addresses the important aspects of formal verification for signoff of chip design when complex net-list optimizations such as signed data path operations, don't care logic/states, finite state machine register inference style, timing feedback loops, clock gating, and register retiming exist.