SBIR Phase II: Automatic Scalable Architectural Validation for Microprocessors

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

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

This Small Business Innovation Research (SBIR) Phase II project addresses the challenge of automating and scaling formal equivalence verification between architectural 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 represent a product for architectural validation of general purpose microcontrollers, capable of proving equivalence or finding bugs with reasonable computational resources.The broader impact/commercial potential of this project 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. The products resulting from this project will provide substantial benefit by ensuring design correctness for mission-critical components such as implantable medical devices, aviation hardware, and satellite/space systems. In addition to hardware verification, the work done in this project will contribute to firmware and software verification, which has utilized similar techniques in the past. It will additionally contribute to exploring industrial-oriented algorithms and heuristics in the domain of automated reasoning and constraint satisfaction problems, used in theorem proving, machine learning, scheduling optimization, gaming, and network security.

这个小型企业创新研究（SBIR）第二阶段项目解决了自动化和扩展微处理器和ASIC微控制器的体系结构SystemC模型和RTL Verilog模型之间的形式等效验证的挑战。工业处理器的复杂性，以及SystemC和Verilog的语义差异，造成了一个显着的建模差距，使得它不可行的验证RTL Verilog实现对他们的SystemC规范模型。这一差距阻碍了目前EDA的发展，其中设计人员正在抽象级别上向上移动，以建模和验证硬件设计。我们的形式等价验证技术将允许自动获得RTL ESL模型使用高层次的综合工具，并正式验证所得到的模型对规范模型的正确性。它还将允许手动编写的RTL模型与最初为架构仿真创建的ESL模型进行验证。预期的挑战包括克服空间和时间建模的差距，并验证等价性的无限深度使用有限的等价配方。到项目结束时，我们预计将开发一个软件程序原型，该软件程序将代表通用微控制器架构验证的产品，能够证明等效性或通过合理的计算资源发现错误。该项目更广泛的影响/商业潜力是使形式验证技术可扩展，并可由设计人员在更高的抽象级别直接使用，使得设计复杂性指数增长而验证成本指数增长。该项目产生的产品将通过确保植入式医疗设备、航空硬件和卫星/空间系统等关键任务组件的设计正确性而带来巨大的好处。除硬件验证外，本项目中所做的工作将有助于固件和软件验证，这些验证在过去使用了类似的技术。它还将有助于探索自动推理和约束满足问题领域中面向工业的算法和算法，用于定理证明，机器学习，调度优化，游戏和网络安全。