ConnChecker: Automated Root-Cause Analysis for Formal Connectivity Check via Graph

ConnChecker is a novel graph-based automated tool that accelerates formal connectivity verification in complex SoC designs by categorizing counterexamples and localizing root causes, achieving up to an 80% reduction in debugging time.

The Gist

Imagine you are the chief engineer of a massive, futuristic city (a Chip or SoC). This city is made of billions of tiny roads, bridges, and traffic lights (the signals and wires) that connect different districts (the components).

Your job is to make sure that when a message is sent from the "Power Plant" (the Source) to the "Hospital" (the Destination), it actually gets there without getting lost or blocked.

The Problem: The "Lost in the Maze" Scenario

In the past, when a message failed to arrive, engineers had to act like detectives with a magnifying glass. They would manually trace every single road on a giant map, looking for a broken bridge or a red light that was stuck.

• The Issue: The city is so huge and complex that this manual tracing takes forever. It's like trying to find a specific typo in a library of a million books by reading every page.
• The Result: Engineers spent nearly half their time just fixing these "lost messages" instead of building new features.

The Solution: ConnChecker (The Smart GPS)

The authors of this paper created a tool called ConnChecker. Think of it as a Smart GPS and Traffic Control System that doesn't just tell you that a message failed, but instantly tells you why and where to fix it.

Instead of manually walking the streets, ConnChecker looks at the city as a Graph (a web of dots and lines) and automatically sorts the problems into three buckets:

Bucket 1: "The Road Exists, But Traffic is Stopped"

• The Metaphor: The bridge is built, but a construction crew (a bug or wrong setting) has put up a "Do Not Enter" sign.
• What ConnChecker Does: It zooms in on the specific bridge and says, "Hey, the sign is wrong here!" It breaks the long journey into small segments and checks each one individually, pinpointing the exact spot where the traffic jam started.
• Result: Instead of checking the whole highway, you only fix one small section.

Bucket 2: "The Road Doesn't Exist"

• The Metaphor: You are trying to drive from the Power Plant to the Hospital, but the map shows a cliff where the bridge should be. The road was never built.
• What ConnChecker Does: It works backward from the Hospital. It asks, "Who should be sending power here?" It traces back to the source and finds the missing link. It's like a detective saying, "The Hospital has no power because the main generator wasn't connected to the substation."
• Result: It highlights the missing wire so you can build it immediately.

Bucket 3: "The Road Exists, But It's a Dead End"

• The Metaphor: The road is there, but a giant wall (a logic constraint) blocks the car from moving forward. The car can see the road, but it can't drive on it.
• What ConnChecker Does: It analyzes the rules of the road. It finds the specific rule (like "This gate only opens if it's raining") that is preventing the signal from passing.
• Result: It tells you exactly which rule is too strict and needs to be loosened.

The Results: From Hours to Minutes

The team tested this tool on two real-world "cities" (a Radar Sensor and a Car Computer).

• Before: Fixing a complex connection problem took engineers nearly 30 minutes of intense, manual tracing.
• After: ConnChecker solved the same problems in about 5 minutes.
• The Magic: For the hardest, most complicated problems, it saved up to 80% of the time.

Why This Matters

Imagine if your GPS didn't just say "You are lost," but instead said: "You are lost because you missed a turn 2 miles ago. Here is the exact street name, and here is a picture of the missing sign."

That is what ConnChecker does for chip designers. It turns a frustrating, hours-long mystery into a quick, automated fix, allowing engineers to spend less time debugging and more time innovating.

In short: ConnChecker is the ultimate auto-pilot for fixing broken connections in computer chips, turning a manual nightmare into a fast, automated process.

Technical Summary

Here is a detailed technical summary of the paper "ConnChecker: Automated Root-Cause Analysis for Formal Connectivity Check via Graph."

1. Problem Statement

Formal connectivity verification is a critical step in System-on-Chip (SoC) design to ensure signal paths and interconnections function correctly. While tools like the Cadence JasperGold Connectivity App can verify these paths, the debugging process remains a major bottleneck:

• Manual Intensive: When a connectivity check fails, the tool generates a counterexample (CEX). Engineers must manually analyze these CEXs to find the root cause, a process that consumes approximately 47% of verification time according to industry reports.
• Complexity: As designs grow (e.g., mixed-signal, multi-clock domains, deep hierarchies), manual tracing of signal paths becomes error-prone and time-consuming.
• Lack of Automation: Existing solutions focus on verification execution but lack automated frameworks for Root-Cause Analysis (RCA) and debugging acceleration.

2. Methodology: ConnChecker Framework

ConnChecker is a graph-based framework designed to automate RCA by integrating formal tool outputs (structural/functional dependency graphs and CEX reports) into a structured workflow. It models the Design Under Test (DUT) as a directed dependency graph $G = (V, E)$, where nodes are signals/pins and edges represent dependencies.

The solution operates in two main stages:

A. Automatic Failure Categorization

Upon receiving a failure report, ConnChecker automatically classifies the failure into one of three distinct categories to route it to a specific analysis flow:

1. Functional & Structural Connection Exists: The path exists structurally and functionally, but the check fails due to RTL bugs, incorrect connectivity maps, or missing constraints.
2. No Structural Connection: The path is physically broken (missing edges), making the destination unreachable from the source.
3. Only Structural Connection Exists: A structural path exists, but signal propagation is blocked by over-constraints, disabled logic, or incomplete formal setup (functional disconnect).

B. Core Debug Engine (Three Analysis Flows)

Once categorized, the tool executes a targeted workflow:

• Flow 1 (Functional/Structural Failure):

  • Strategy: Decomposes the functional dependency graph into smaller segments.
  • Action: Generates atomic assertions for each edge to isolate the specific broken segment. It utilizes reverse connectivity checks on failed segments to extract connections directly from RTL, comparing them against specifications.
  • Benefit: Segment-level analysis is more efficient than full-path reverse checks and provides precise localization of the error.

• Flow 2 (No Structural Connection):

  • Strategy: Uses Fan-in Analysis (backward tracing) starting from the destination signal.
  • Action: Constructs a fan-in graph to identify the "cone of influence." It filters out irrelevant signals (clocks, resets, top-level inputs) to isolate root drivers (signals not driven by any other signal).
  • Benefit: Identifies missing drivers or disconnected segments without exhaustive manual inspection.

• Flow 3 (Only Structural Connection):

  • Strategy: Applies a divide-and-conquer approach to the structural path.
  • Action: Leverages JasperGold's over-constraint analysis to pinpoint why signal propagation is blocked (e.g., inputs tied to 0, logic gating).
  • Benefit: Explains functional disconnects caused by environmental constraints rather than missing wires.

3. Key Contributions

1. Structured Failure Categorization: Transforms manual debugging into an automated, graph-driven process by routing failures to specific, optimized analysis flows.
2. Automated Atomic Connectivity Checks: Generates targeted assertions for individual graph edges to isolate broken connections with minimal manual intervention.
3. Fan-in Cone Analysis: Automates the tracing of upstream dependencies to identify missing drivers in cases where no connectivity exists.
4. Scalable Architecture: Supports both single-mode (individual failure) and multi-mode (concurrent processing) debugging, validated on production-grade industrial SoCs.

4. Experimental Results

The tool was evaluated on two industrial SoCs:

• Radar Sensor: Medium-sized, multi-hierarchical.
• Automotive Microcontroller (AURIX): Large-scale, deep hierarchy, complex peripheral coverage.

Performance Metrics:

• Time Reduction: ConnChecker achieved up to an 80% reduction in debugging time for complex cases.
• Speedup Factors:
  • Simple Connections: Comparable to manual methods (2x speedup).
  • Complex Connections (Mixed-signal, Multi-clock, 40+ edges): Speedups ranged from 2x to 5x.
  • Specific Example: A complex microcontroller case (47 edges, multi-clock domain) took ~29 minutes manually but only ~5 minutes with ConnChecker.
• Scalability: Runtime remained nearly constant as connection complexity increased, demonstrating the framework's ability to handle large-scale designs efficiently.

5. Significance and Impact

• Bridging the Automation Gap: ConnChecker addresses a critical void in the verification ecosystem where debugging remains largely manual despite advanced verification tools.
• Handling Complexity: It specifically tackles difficult scenarios like mixed-signal connectivity, multi-clock domain crossings, and multiple failure points, which traditionally require deep domain expertise and iterative manual tracing.
• Practical Applicability: Validated on real-world, tape-out chips, proving its viability for industrial use.
• Future Outlook: The authors identify limitations in handling multi-path scenarios (requiring heuristic path selection) and bus-level connections (requiring bitwise optimization), setting the stage for future enhancements in automation heuristics.

In conclusion, ConnChecker significantly accelerates the formal connectivity debugging lifecycle, reducing time-to-market and engineering effort by transforming unstructured tool outputs into actionable, automated root-cause analysis.