使用 Magellan 验证 MIPS 设计
SNUG San Jose 2008
2008
12 页
使用 Magellan 验证 MIPS 设计
会议: SNUG San Jose 2008 作者: MIPS Technologies 页数: 12
摘要
MIPS Technologies 设计日益增长的复杂性以及对更快更高效验证技术的需求，使得将形式验证 Formal Verification工具集成到设计验证流程中的重要性日益增加。同时，对断言 Assertion的大量使用为集成纯形式化和半形式化工具以验证现有模型检查器准备了良好的环境。
此前阻碍形式验证工具更早应用的主要问题是它们相对较差的性能以及与主流验证流程（仿真、加速和仿真 Emulation）的脱节。然而，最近一些工具，特别是 Synopsys 的 Magellan，通过提供相对改善的执行时间、内存使用和管理、证明能力，以及与 VCS 仿真器更紧密的集成，克服了这些限制。
通过更新其验证框架，MIPS Technologies 的目标是：(1) 提高验证的完备性；(2) 使能单元级验证工作的复用；(3) 提供更高效的错误捕获能力。Magellan 满足了这些目标的大部分，性能与其他现有工具相当。此外，它提出了一种有趣而高效的方法学，将纯粹形式化（模型检查）证明与随机仿真相结合，形成一种混合验证方法。
图片索引
共 3 张图片，存放于 _images/ 目录。