SBIR Phase I: Automatic Scalable Architectural Validation for Microprocessors

SBIR 第一阶段：微处理器的自动可扩展架构验证

• 批准号: 1215131
• 负责人: Zaher Andraus
• 金额: $ 14.99万
• 依托单位: Reveal Design Automation, Inc.
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-07-01 至 2012-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1215131&HistoricalAwards=false
• 关键词: SBIR; Phase; Automatic; Scalable; Architectural

This Small Business Innovation Research Phase I Project addresses the challenge of automating and scaling formal equivalence verification between architectural ESL/TLM SystemC models and RTL Verilog models for microprocessors and ASIC microcontrollers. The complexity of industrial processors, together with the differences in semantics of SystemC and Verilog, create a significant modeling gap that makes it infeasible to verify RTL Verilog implementations against their SystemC specification models. This gap impedes the progression currently taking place in EDA, wherein designers are moving upwards in the abstraction level for modeling and verifying hardware designs. Our formal equivalence verification technology will allow automatically obtaining RTL from ESL models using high-level synthesis tools, and formally verifying the correctness of the resulting models against the specification models. It will also allow manually written RTL models to be verified against ESL models originally created for architectural simulation. Expected challenges include overcoming the spatial and temporal modeling gaps, and verifying equivalence for an unlimited depth using finite equivalence formulations. By end of project, we anticipate to prototype a software program that will discover unintended behavior in microprocessor designs by ARM with respect to the reference architecture, or prove the lack of any bugs, with modest computational resources.Functional verification of microprocessor designs remains a key challenge for the industry due to exponentially growing verification costs - typically 50% of a design budget. Formal verification has potential to reduce these costs, however existing formal technology can only handle small RTL blocks and is only used by a handful of formal domain experts. With the industry shifting towards larger design blocks and higher-level ESL languages such as SystemC, a turn-key tool such as ours is necessary to bridge the ESL/RTL verification gap and addresses the needs of design and verification engineers who do not necessarily have formal domain expertise. Our target market includes both the integrated design manufacturing and fabless ASIC/SoC suppliers. A typical customer would be an ASIC design company looking to lower verification costs, decrease time-to-market, and reduce the risks of discovering errors during post-silicon verification or post-production. Formal semiconductor verification tools such as ours play an especially vital role in mission-critical semiconductor design markets such as ASICs for medical equipment, high-availability sensors, and automotive semiconductors. Our long-term goal is to make formal verification technologies scalable and directly usable by designers at higher abstraction levels, enabling exponential growth in design complexity without exponential growth in verification cost.

这个小型企业创新研究第一阶段项目解决了微处理器和 ASIC 微控制器的架构 ESL/TLM SystemC 模型与 RTL Verilog 模型之间的自动化和扩展形式等效性验证的挑战。工业处理器的复杂性以及 SystemC 和 Verilog 语义上的差异造成了显着的建模差距，使得根据 SystemC 规范模型验证 RTL Verilog 实现变得不可行。这一差距阻碍了 EDA 目前的发展，其中设计人员正在抽象级别上向上移动，以建模和验证硬件设计。我们的形式等价验证技术将允许使用高级综合工具从 ESL 模型自动获取 RTL，并根据规范模型形式验证生成模型的正确性。它还允许根据最初为建筑模拟创建的 ESL 模型来验证手动编写的 RTL 模型。预期的挑战包括克服空间和时间建模差距，以及使用有限等价公式验证无限深度的等价性。在项目结束时，我们预计将制作一个软件程序原型，该程序将发现 ARM 微处理器设计中相对于参考架构的非预期行为，或者证明不存在任何错误，并使用适度的计算资源。由于验证成本呈指数级增长（通常占设计预算的 50%），微处理器设计的功能验证仍然是业界的一个关键挑战。形式化验证有可能降低这些成本，但是现有的形式化技术只能处理小型 RTL 块，并且仅由少数形式化领域专家使用。随着行业转向更大的设计模块和更高级别的 ESL 语言（例如 SystemC），需要像我们这样的交钥匙工具来弥合 ESL/RTL 验证差距，并满足不一定具备正式领域专业知识的设计和验证工程师的需求。我们的目标市场包括集成设计制造和无晶圆厂 ASIC/SoC 供应商。典型的客户是 ASIC 设计公司，希望降低验证成本、缩短上市时间并降低在硅后验证或后期生产期间发现错误的风险。像我们这样的正式半导体验证工具在关键任务半导体设计市场（例如用于医疗设备的 ASIC、高可用性传感器和汽车半导体）中发挥着特别重要的作用。我们的长期目标是使形式验证技术具有可扩展性，并可供设计人员在更高抽象级别直接使用，从而使设计复杂性呈指数级增长，而验证成本不会呈指数级增长。