Verifying your 2.5/3D IC device assembly level netlist
The heterogeneous integration of multiple chiplets in a single packaging platform is critical for many high-performance compute segments such as AI, Hyperscalers, HPC, Cloud datacenters, neural processors and even autonomous vehicles. With the quantity of chiplets commonly exceeding double-digit numbers. Add to that the increasing usage of high-speed, low power and low latency high-bandwidth-memory (HBM) stacks the resultant designs often exceed 1M+ total pins. With that many device pins the resultant connectivity is massive making the task of verifying the connectivity’s correctness exceptionally challenging and time consuming.
The traditional way to verify the connections requires a lot of manpower and time and is either not exhaustive or too late in the process. In this blog we will introduce a new way to verify the package connectivity using formal verification that can exhaustively verify all interconnections between the chiplet blocks. The flow is automatic for all steps from creating the connectivity specification to verifying the package assemblies output connectivity. The automatic parallel algorithms execute on a compute grid and verify huge numbers of connections in minutes even seconds. The script for executing the flow is simple and only takes a few minutes to setup. Once the script is ready, it can be reused for different package projects.
How was this typically done?
Historically semiconductor package design has been a relatively simple task as it involved a single IC/die with a relatively low number of external bumps (100’s). The IC/die bumps are fanout connected to the package ball-grid-array (BGA) geometry suitable for connecting to a printed circuit board. The package netlist connecting the IC/die bumps to BGA was often captured by the package designer, typically using Excel to manually assign net names to the desired die bumps and BGA balls to achieve the intended connection.
We are going to need a new approach!
Today’s multi IC/chiplet heterogeneously integrated packages often include interposers and is now a system integration task: The designer has the responsibility to take input from various stakeholders, who are often designing their content at the same time the package and/or interposer is being designed and create a design which is both electrically and physically correct, but functions as designed too.
Heterogeneous integration has brought with it some challenges for the package designer. The source data is being supplied in a myriad of data formats such as Ball map CSV files, LEF/DEF from IC place and route tools, GDSII/OASIS, Verilog RTL, spreadsheet/csv data and of course plain text files.
As each component of the design is introduced, it must be connected to the other components in the system. Spreadsheet based design requires every connection be defined as a scalar. High Bandwidth Memory (HBM) based designs with their 1024 bit width would be extremely tedious and error prone defining the connectivity one bit at a time.
To handle the explosion of die-to-die connections, designers are embracing language-based design to define the connectivity of the system. It is far more efficient and less error prone to write Verilog RTL using proper bus notation to connect the various components of a system together than it is to define the connectivity one bit at a time in a spreadsheet or develop specialized Excel macros to populate a connectivity table. Spreadsheet based solutions, even with custom macro development, do not scale for hundreds of thousands or millions of bumps. Through the use of Siemens Innovator3D IC Integrator the challenge of source data aggregation/integration is quickly overcome, creating a 3D Digital Twin model of the entire design. The design connectivity can then be exported for verification, this aggregated netlist can then be validated against the reference netlist the design was assembled from by using a functional verification process and technology.
The formal verification tool, Questa OneSpin Formal Verification specializes in connectivity checking and is a perfect fit for verifying package connection early in the process. It does not require package designers to write lengthy testbenches and assertions. For verifying the connections between multiple dies, formal tools only need the system top module that instantiates the multiple dies and has the connectivity information of the dies, and the module port definitions of the dies, normally the “black box” modules received by a package team. Formal verification is a powerful way of detecting connectivity errors, ensuring correctness of connections, avoiding short circuits and easily manages millions of connections. Formal verification can be applied right after package pathfinding/prototyping, before package physical implementation is started. Any mistakes in the planning and prototyping stage can be caught early, which can save lots of time and money if allowed to enter the implementation process.
This entire process was presented in detail at the 2024 DVcon conference. The paper describing the process and workflow can be found here:
