SBIR Phase I: Automatic Scalable Architectural Validation for Microprocessors

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

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.