,®财产检查

,财产检查图标

详尽的验证之前仿真测试环境

,形式验证可以尽快设计完成之前调试模块集成,并发现潜在的错误之前仿真测试环境。共享一个共同的语言的前端,先进的模拟器,利用集成与统一的覆盖数据库(UCDB),,形式验证是完美的工具来加速错误检测,证明了RTL匹配指定的功能,证明bug修复不破坏任何东西,并达到覆盖关闭速度。

你确认是如何完成?吗?

即使是最文笔constrained-random testbenches不能遍历每一个设计的状态空间的一部分。事实是,对于甚至小的DUT,基于仿真的验证基本上是不完整的。它可以创建一个模拟testbench前需要许多星期,为将复杂bug写入IP提供机会窗口。是否特定的错误是由于一个过时的或被误解的规范,或者是一个基本的设计缺陷,它未被发现的时间越长,价格越贵,修复,和彻底的验证修复修复bug和不会产生不必要的副作用。

,财产检查
只有几个属性来定义目标行为和输入信号限制,,财产检查(PropCheck)可以详尽的验证你的RTL——没有testbench !熟悉的波形界面显示失败或成功的信号模式,和覆盖在Accellera-standard进展报告统一报道数据库(UCDB)格式。

解决方案:,PropCheck

,财产检查(PropCheck)支持通用assertion-based形式验证,确保设计符合其特定的功能需求。支持PSL,上海广电,OVL,包括是多时钟域的断言,PropCheck容易验证甚至非常大的设计有许多断言;分析设计vs的行为。所需的行为所描述的断言来识别所有设计状态可及的初始状态。

这个分析允许PropCheck探索整个状态空间广度优先的方式,与深度优先的方法用于仿真。PropCheck因此能够详尽发现任何可能发生的设计错误,不需要特定的刺激来检测错误。这确保了验证设计是在所有合法输入场景中没有错误。与此同时,这种方法本质上标识的覆盖点,这有助于加快覆盖关闭。

在引擎盖下,PropCheck世界级的,高容量,高吞吐量引擎有效地建立在各自的优势,相互配合实时;从而更快地完成验证。与Questa高级模拟器共享公共语言前端并利用与统一覆盖数据库(UCDB)的集成,,PropCheck加速缺陷检测是完美的工具,纠错和覆盖范围关闭。

特性

  • 提供详尽的验证没有通过assertion-based testbenches正式的验证
  • 多个合作正式引擎给最高的容量和性能
  • 集成先进,模拟器可以轻松调试断言失败
  • 电子集成/结果报告与UCBD允许用户交流他们的进展和成功与形式分析的主要数据库(通过验证验证管理器)
  • 支持上海广电,PSL,和OVL属性;Verilog或VHDL dut

好处

  • 早期的调试:验证块模拟测试之前准备好
  • 彻底的验证:详尽分析所有可能的场景
  • 覆盖关闭:跟踪和报告形式分析的成功在此工具中,以及出口这个数据中心验证跟踪工具
  • 硅后调试:复制观察到的故障来验证修正
聊天| 联系