形式验证提供了一种快速、详尽且支持高效调试的解决方案。传统上，芯片级形式验证确实不可行。该方法通常以模块级别为目标，使状态空间的规模保持在适当水平。但是，鉴于连通性检查仅集中在布线上（与模块级别的复杂度相比，布线一般是器件的简单部分），借助一些假设，状态空间可以减小到可管理的规模。这种简化的性质取决于所需检查的类型。本文首先会概述几种类型的连通性检查，然后详细介绍一种新型半自动验证流程（包括代码）。已有一些 Mentor Graphics 使用该流程来简化连通性检查。该流程基于一个脚本环境，围绕该环境提供了充足的信息以方便用户开始实施新的验证方法。
来源：Mentor
