Scalable Formal Verification of Digital Integrated Circuits

Award Information
Agency: National Science Foundation
Branch: N/A
Contract: 0945757
Agency Tracking Number: 0945757
Amount: $175,450.00
Phase: Phase I
Program: SBIR
Awards Year: 2010
Solicitation Year: 2010
Solicitation Topic Code: IC
Solicitation Number: NSF 09-541
Small Business Information
330 E. Liberty Street, Lower, Ann Arbor, MI, 48105
DUNS: 830853946
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Zaher Andraus
 (734) 272-8231
Business Contact
 Zaher Andraus
Title: MEng
Phone: (734) 272-8231
Research Institution
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.

* Information listed above is at the time of submission. *

Agency Micro-sites

SBA logo
Department of Agriculture logo
Department of Commerce logo
Department of Defense logo
Department of Education logo
Department of Energy logo
Department of Health and Human Services logo
Department of Homeland Security logo
Department of Transportation logo
Environmental Protection Agency logo
National Aeronautics and Space Administration logo
National Science Foundation logo
US Flag An Official Website of the United States Government