SBIR Phase I: Scalable Formal Verification of Digital Integrated Circuits

这个小型企业创新研究第一阶段项目解决了扩展数字集成电路（如微处理器，ASIC微控制器和SOC产品）的硅前功能验证的挑战。工业设计的复杂性导致了具有巨大错误空间的大状态空间，并且阻止了设计者能够全面地推理部署在众多设备中的系统的正确性，这些设备的实时故障会导致严重的损失、金钱损失和其他损失。早期的研究表明，使用抽象和推理方法可以显着降低复杂性，这些方法应用于用于生产的设计描述。 未来的预期挑战包括自动调整抽象，以及有效减少推理引擎，以科普设计规模的指数级增长。Reveal的努力通过迭代抽象和细化过程自动化正式验证过程，专门解决了设计师和验证工程师的需求。Reveal的目标市场包括集成设计制造和无晶圆ASIC/SOC供应商。一个典型的潜在客户是ASIC半导体设计公司，他们希望降低验证成本，缩短上市时间，并减少在硅后验证或后期生产过程中发现错误的风险。鉴于Reveal的主要功能是发现半导体设计中的错误，其对高度复杂的设备的影响，但对故障的容忍度也很低，否则可能会对人类生命构成威胁。这些市场的例子包括医院设备的半导体设计和制造，高可用性传感器和汽车半导体。

This Small Business Innovation Research Phase I Project addresses the challenge of scaling pre-silicon functional verification of digital integrated circuits such as microprocessors, ASIC microcontrollers, and SOC products. The complexity of industrial designs results in an large state space with vast room for errors, and prevents designers from being able to comprehensively reason about the correctness of systems deployed in numerous devices, whose real-time failure causes serious losses, monetary and otherwise. Earlier research showed that complexity can be significantly reduced using abstraction and reasoning methods that are applied on design descriptions used for production. Expected challenges moving forward include automatic tuning of the abstraction, and effective reduction to reasoning engines that can cope with the exponential blowup in the size of designs. Reveal's effort specifically addresses the needs of designer and verification engineers by automating the formal verification process through an iterative abstraction and refinement process. The target market for Reveal includes both the integrated design manufacturing and fabless ASIC/SOC suppliers. A typical potential customer would be an ASIC semiconductor design company who is looking to lower its verification costs, decrease time-to-market, and reduce the risks of discovering errors during post-silicon verification or post-production. Given that Reveal's primary function is to find errors in semiconductor design, its implications for equipment with high degrees of complexity, but also with little to no tolerance for failure, which otherwise may pose threat to human lives. Examples of these markets are semiconductor design and manufacturing for hospital equipment, high-availability sensors, and automotive semiconductors.