Scalable Formal Verification of Digital Integrated Circuits

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.