Using formal to exhaustively verify all interconnections between IC blocks right after package planning and prototyping.
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.
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:
Formal verification is powerful for verifying package connections in chiplets. There are several ways that formal methods can help in this context.
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.
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.
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.
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.
 |
 |
 |
 |
 |
 |
 |
 |
 |  |
Leave a Reply