Here At Last! Automated Verification Of Heterogeneous 2D/3D Package Connectivity

By Michael Walsh and Jin Hou with Todd Burkholder

The heterogeneous integration of multiple ICs in a single package along with high-performance, high-bandwidth memory is critical for many high-performance computing applications. After everything has been heterogeneously integrated and packaged, such designs feature complex connectivity with many hundreds of thousands of connections, making it extremely challenging to verify the correctness of the connections. The traditional way to verify these connections requires a lot of manpower and time and is either not exhaustive or too late in the process, as it is typically done after implementation is complete.

This article introduces a new way to functionally verify packaging connectivity using formal verification that can exhaustively verify all interconnections between IC blocks. The flow is automatic for all steps, from creating connectivity specifications to verifying packaging output connectivity. The automatic parallel algorithms on the compute grid can verify huge numbers of connections in minutes or even seconds. The script for the flow is simple and only takes a few minutes to set up. Once the script is ready, it can be reused for different packaging projects.

Automatic formal-based approach

With rapid advances in package technology and the explosion of AI and high-performance computing applications, substrate designers face design challenges that are breaking their existing methodologies. Designs with 500,000 bumps and several hundred thousand connections are becoming commonplace. With hybrid bonding technology promising millions of bump connections, functional verification engineers need a new way to handle the explosion of die-to-die connections.

The formal verification tools specializing in connectivity check are a good fit for verifying package connections early in the process. The formal connectivity solutions do not require package designers to write lengthy testbenches and assertions for possibly millions of connections, as would be required when using simulation. Formal connectivity solutions do not require package designers to understand the function of the design or know how to run a simulation. For verifying the connections between multiple dies, formal tools do not need the functional models of the dies.

They need only two things:

• The system top module that instantiates the multiple dies and has the connectivity information of the dies
• The module port definitions of the dies, normally the “black box” modules received by a package team

Formal verification is powerful for verifying package connections in chiplets. There are several ways that formal methods can help in this context.

1. Detecting connection errors: A formal connectivity solution can detect errors related to package connections. It can mathematically analyze the package output module against the connectivity spec and identify inconsistencies or violations of intended connections that may lead to electrical faults. When it finds broken connections, it provides waveforms to show the issue and has all other necessary features for debugging the issue.
2. Ensuring correctness of connections: Since formal is doing exhaustive mathematical analysis, considering all possible stimulus, it can verify that signals are routed as intended by proving connections adhere to the specified requirements. When it proves a connection, there is no scenario that can break the connection; i.e., no overlooked scenarios.
3. Avoiding short circuits: Formal verification can identify potential short circuits or other connectivity issues in the package by finding unintended connection paths.
4. Complex systems with millions of connections: The formal flow generates a golden connection spec automatically – without the need to manually create CSV files of connections – and can verify large numbers of connections using parallel algorithms.
5. Early detection: Formal verification can be applied right after package prototyping before package physical implementation. Any mistakes in the planning and prototyping stage can be caught early, which can save lots of time and money.
6. Safety and reliability: Only formal verification can do exhaustive analysis. It is crucial to use formal verification to verify the correctness of package connections of ICs for industries like aerospace, automotive, and medical.
7. Compliance: Formal tools should be ISO 26262 certified, which is essential for audits and quality control for industries with strict regulatory standards.

When using formal tools to verify the correctness of the package connections after package prototyping is done, we need the specification of the connections. Some companies manually create the connection spec in CSV files and write scripts to generate the system top to instantiate the multiple dies in accordance with the connection spec. In this situation, the existing CSV file can be used as the spec for verifying package output files. When there is no existing CSV spec of the connections, either the user manually creates the connection spec in a format accepted by the formal tool or uses a connectivity extraction tool to generate the specification if the design or verification team has already created the system top module and has done functional verification. We can use the system top module and the black boxes of the dies as the golden reference model, and its connections as the specification.

When we have the spec of the connections and the output netlist file from the package tool, we can run the formal connectivity tool to verify if the package output design satisfies the connection specifications. The two flows for using formal verification tools to verify package connectivity are shown in figures 1 and 2.

Fig. 1: Using existing connection spec in CSV.

Fig. 2: Using reference model to extract connection spec.

Two testcases

In our two testcases, we used the flow shown in figure 2. First, we used golden reference models and the Siemens EDA tool Connectivity Explorer to extract connections automatically from the reference model and export them into a CSV file. Then we used the Xpedition Substrate Integrator (xSI) package tool to generate Verilog netlists. Finally, we used the Check Connect formal tool to automatically generate checks for the connections in the CSV file and formally verify if the package output file satisfies the connections in the CSV spec file; i.e., to see if the packaging process broke any connections in the golden reference model.

When using formal connectivity solutions, the script is very simple and requires only a few minutes to create. After the script is ready, the run is automatic. Here is an example of the Makefile to run all the steps. The config.txt has the simple definition “-inst *” that tells Connectivity Explorer to extract all connections for all instances.

#### Compile designs 
   Compile_vl:
      vlog -sv -f flist_golden.txt -work lib_golden 
      vlog -sv -f flist_package.txt -work 
      lib_package
#### Generate Connectivity Spec 
   Generate_conn_csv:
      qconnect_check -explore -od log_csv \
      -infile config.txt \
      -dut F1760_Crete -work ./lib_golden 
#### Run Formal Analysis
   Check_connect:
      qverify -od log_cc -do "\
      connectcheck compile -d F1760_Crete -work lib_package;\ 
      connectcheck load csv log_csv/qconnect_explore_F1760_Crete.csv;\
      connectcheck verify "

When using the formal tool to verify package connections, we care about only the connections between the blocks. We do not need to know about the functionality inside each block. The package tool can export modules without internal logic and keeps only the ports and connections between blocks.

Package teams often get only the system top module and the black box of dies from system verification teams. Even when package teams get the full functional modules from the system verification team for the golden reference model, Connectivity Explorer can treat the die modules as black boxes and extract the connections between the dies. Through black boxing the modules of dies, the formal tool can run very fast with any size of system. When verifying the package design against the connection spec CSV, Check Connect also runs fast and can handle big systems with many dies since there are not many sequential logics to analyze.

When running Check Connect on the package design with the connection spec CSV, if the tool exhaustively proves all the connections, we are assured that the package design satisfies the connectivity spec. If the tool finds any violations, we know that the package design has broken some connections and routed signals in wrong paths.

When the tool finds a violation, it provides a short counterexample in the wave tab to show the violation of the connection. With the waveforms and rich debug features, such as source tracing and schematic view, provided by the formal tool, we can easily find the root cause of the issue.

Is there any possibility that the reference model or the connection specification missed some connections? It is possible since system functional verification may not be exhaustive, or package planning may be started before system functional verification is completed. Is there any possibility that the package design accidentally adds extra pins or connections? This situation is rare, but not entirely error-free due to such things as pin typos that add new pins.

One way to help on this issue is using a unique feature of Check Connect to generate a missing-port report that lists the ports of the top module and the dies not covered by any connections. If there is a port uncovered by the connection specification, first we will check if the port definition in the package design is correct and not a mistake. If the port definition is correct, the problem may lie either in the reference model from which the CSV file is extracted or in the original manually created connection specification. For missing connection definitions, we can manually add them, and rerun Check Connect on the package design.

Testcase results

We ran two designs using the second flow described above and shown in more detail in figure 3. The wall time, including compile and extracting the connections of the reference model for the two test cases, is 15 seconds and 35 seconds, respectively. The wall time, including compile and checking the connections of the package design for the two test cases, is 30 seconds and 56 seconds, respectively.

Fig. 3: Detailed testcase flow using formal verification.

When using Check Connect to generate the missing-port report for Design 1, the tool identified that two ports “U12.DFX_THERMO0” and “U12.DFX_ THERMO1” are not covered by the connection specification. Checking the source files of both the reference model and the package design reveals that neither have connections for these two ports, as shown in figure 4. The root cause of the missing connections for the two ports in the package design is caused by the missing connections in the reference model. Therefore, not only can Check Connect verify package designs, it can also find possible missing connections in the reference models (figure 4).

Fig. 4: Missing two connections.

In this case, the designer had purposely left two thermal sensor pins unconnected. Check Connect identified these two as suspicious, leaving the designer to decide how to disposition them. It is not uncommon to leave unused pins floating. The designer later confirmed that leaving these two pins floating was intentional but was still impressed it was identified. The results for the two testcases are shown in table 1.

Table 1: Testcase results.

Conclusion

When using formal to start connectivity verification early, right after package planning and prototyping, the quality of the physical implementation can be improved dramatically and the time to market can be shortened significantly. The ease of use of the methodology makes its adoption painless with immediate rewards.

For a fuller explanation of the challenges of verifying package connectivity and why other approaches fall short, and to gain a deeper understanding of how to use formal tools to verify connectivity for package designs, please download the whitepaper from Siemens, New innovative way to functionally verify heterogeneous 2D/3D package connectivity.

Jin Hou is a product engineer for Questa Formal in the IC Verification Systems division of Siemens EDA. Houhas more than 12 years in formal and assertion-based verification. She has worked as a CAE and PE, with experience in product definition, customer support, tool testing, customer training, technical marketing, and, currently, as a PE for the Questa Formal Apps. Houearned her Ph.D. at Université de Montréal, Montreal, Canada.

Todd Burkholder is a senior writer for Siemens EDA.