SBIR Phase I: Automatic Scalable Architectural Validation for Microprocessors

这个小型企业创新研究第一阶段项目解决了在微处理器和ASIC微控制器的架构ESL/TLM SystemC模型和RTL Verilog模型之间自动化和扩展形式等效验证的挑战。工业处理器的复杂性，加上SystemC和Verilog在语义上的差异，造成了一个显著的建模差距，使得根据它们的SystemC规范模型验证RTL Verilog实现变得不可行的。这种差距阻碍了当前EDA的发展，在EDA中，设计人员正在向抽象层次上移动，以便对硬件设计进行建模和验证。我们的形式等价验证技术将允许使用高级综合工具从ESL模型中自动获得RTL，并根据规范模型正式验证结果模型的正确性。它还允许手工编写的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.