形式验证工具创业公司的jasper design automation公司正在提供一款用于帮助ic验证团队生成并跟踪验证计划的免费工具。jasper公司主管市场的副总裁craig cochran先生说：该公司提供了“浅形式工具”和“深形式工具”。浅形式工具（例如，jasper gold express）通常用于证明形式断言，而深形式工具（例如，jasper gold）则负责运行一个系统形式测试计划，用于描述设计中需要进行形式验证的最为关键的特征。这些工具随后将对上述特征进行系统验证。

　　大多数验证小组都混合运用了仿真、形式、代码覆盖和其它技术。验证小组必须区分这些功能的优先次序，并估计适合每种功能的最佳验证方法。因此，验证小组通常会制订一项验证计划。cochran先生说：“客户编写这些测试计划已经有一段时间了，但是，他们常常是采用一种字处理程序来编写计划。验证小组确实需要一种能够帮助人们轻松完成测试计划的设计和生成的工具。该产品可为人们提供众多的用途——不仅可用于形式验证，而且还可应用于仿 真。”

　　jasper公司计划于8月中旬向所有那些有兴趣下载其gameplan verification planner工具的用户分发拷贝。该产品有助于用户捕获其设计的主要特征、期望功能、验证方法、测试优先级、技术和测试状态。该工具生成了一个验证测试矩阵以提供整体验证状态，并以超级链接html（超文本标记语言）格式生成了一项验证测试计划。各验证小组可通过其网络来共用测试矩阵和html验证测试计划，从而分享有关其工作进展的信息。