SBIR Phase II: Automatic Scalable Architectural Validation for Microprocessors

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

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.