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.
In this SBIR Phase I Project, we prototyped a commercial version of Reveal, a fully automated formal verification system that is able to scale well to modern industrial-size microprocessors without compromising verification coverage. By utilizing partial abstraction and reduction to constraint reasoning, Reveal is able to verify high-level properties on the control logic of microprocessors and microcontrollers implementing various types of optimizations such as pipelining. Reveal is demonstrated using an intuitive equivalence-based verification methodology that requires minimal knowledge about the design or sophisticated formal verification techniques. The project experimented with applying Reveal on the RTL description of a commercial processor by ARM. Reveal exposed a genuine case of unintended behavior, exposed numerous artificially instilled ones, and proved correctness of the refined version of the design, all within minutes of CPU-time. The project advanced two aspects of Reveal's core algorithms. First, it studied the effect of utilizing high-level as well as low-level structures in the design, in order to guide the abstraction/refinement framework. The Reveal framework (based on word-level UF-based abstraction/refinement) is very robust in the sense that structural heuristics have the potential of achieving orders of magnitude speedup for solving using partial abstraction and formula simplifications. Second, it studied the potential of automating the formulation of equivalence-based correctness criterion. In the second commercial core we applied Reveal on, it was evident that due to the way microprocessors are designed today (especially with the high-level optimizations such as pipelining), simplified formulations of ISA-like models can be automatically related (for equivalence) to the RTL model by controlling a minimal set of high-level control signals (or input combinations) for stalling and flushing. However, reasoning on infinite sequences of instructions may require multiple formulations, both inductive and reset-based, to cope with unreachable states and false alarms due to temporal abstraction. Overall, the high-degree of automation in the correctness formulation within Reveal, coupled with the simplicity of the abstraction and solving heuristics, equip the designer or verification engineer with effective means to overcome the state explosion problem without compromising verification coverage and without spending days or weeks of setup time. With the deployment of Reveal, we believe that comprehensive verification of complex microprocessor cores is now feasible.
