Empyrean FormalMC

         在大算力、高可靠的应用场景下，电路规模、场景复杂度上升，集成方式多样化，对可靠性、安全性要求严苛。而数字仿真存在完备性和效率瓶颈，硬件仿真/原型验证底层调试能力有限等问题，需要更完备、更高效的逻辑功能验证手段。

         通过形式化建模，将RTL / Netlist表示成自动机，用户/工具以断言形式输入期望功能，形式化验证工具自动遍历自动机，通过寻找反例来检验断言是否成立。它通过数理逻辑推理的方式，遍历状态空间并搜索Bug，覆盖全部设计状态。

         形式化属性验证工具Empyrean Formal™MC有业界领先的引擎和验证策略，在空泛性检查、功能覆盖率分析、图形化界面等方面表现优异，支持通用硬件设计语言、支持不可综合的设计自动黑盒化、支持常用断言语言、支持位级和字级建模。同时FormalMC还具备多个创新引擎如错误追踪引擎，可以从初始状态开始发现数千个时钟周期的Bug，提供了一个超越纯粹形式化和仿真的独特验证范围。