SBIR Phase II: Automatic Scalable Architectural Validation for Microprocessors

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

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.