形式验证工具创业公司的Jasper Design Automation公司正在提供一款用于帮助IC验证团队生成并跟踪验证计划的免费工具。Jasper公司主管市场的副总裁Craig Cochran先生说:该公司提供了“浅形式工具”和“深形式工具”。浅形式工具(例如,Jasper Gold Express)通常用于证明形式断言,而深形式工具(例如,Jasper Gold)则负责运行一个系统形式测试计划,用于描述设计中需要进行形式验证的最为关键的特征。这些工具随后将对上述特征进行系统验证。 大多数验证小组都混合运用了仿真、形式、代码覆盖和其它技术。验证小组必须区分这些功能的优先次序,并估计适合每种