Formal connectivity checking offers scalable verification of signal paths in complex SoC designs, but debugging counterexamples remains a manual and time-consuming process. ConnChecker introduces a new graph-based perspective for automating root-cause analysis by integrating formal tool outputs such as structural/functional dependency graphs and counterexamples report. It begins with automatic failure categorization, routing each counterexample to one of three targeted analysis flows. These flows localize failure points and suggest corrective actions or hints for manual inspection. Evaluated on two industrial SoCs, ConnChecker achieved up to 80\% reduction in debugging time, especially for complex cases, demonstrating its scalability and effectiveness across diverse connectivity scenarios.

翻译：形式化连通性检查为复杂SoC设计中的信号路径提供了可扩展的验证手段，但反例调试仍是一个依赖人工且耗时的过程。ConnChecker提出了一种新的基于图的视角，通过整合形式化工具输出的结构/功能依赖图及反例报告，实现根因分析的自动化。该方法首先进行自动故障分类，将每个反例路由至三个针对性分析流程之一。这些流程能够定位故障点，并提供修正建议或人工检查线索。在两个工业级SoC上的评估表明，ConnChecker可减少高达80%的调试时间，尤其在复杂场景中效果显著，验证了其在多样化连通性场景下的可扩展性与有效性。