Formal verification of ‘full chip’ containing ‘shell’ partitions with and without feed-thrus

The `Full Chip´ module of an ASIC is made up of various partitions and similar to individual partitions, it also goes through various stages of the physical design. The initial design-planning works on the existing pins of a partition, adds feed-thru pins and performs custom placement and routing on signal and clock nets. Near tape-in, ECO (Engineering Change Order) forces manual changes to design as opposed to taking it through full implementation cycle. At the final stages, when layout database of each partition meets the requirements, a bottom up integration is carried out to create full chip layout. All these stages can create logical differences between layout and RTL of the top level interface. In order to verify that no unintentional logical change has happened to full chip, a robust formal verification strategy with numerous practical considerations is necessary. Designers also make use of 100% or partial shell models at the floor-planning phase which does bring advantages but also creates challenges for the formal verification flow. This article documents these challenges by explaining the formal verification approach taken on Intel´s next generation network processing chip.