SBIR Phase I: Scalable Formal Verification of Digital Integrated Circuits

SBIR 第一阶段：数字集成电路的可扩展形式验证

• 批准号: 0945757
• 负责人: Zaher Andraus
• 金额: --
• 依托单位: Reveal, LLC
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-01-01 至 2010-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0945757&HistoricalAwards=false
• 关键词: SBIR; Phase; Scalable; Formal; Verification

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.

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