SHF: Small: Bit-level Formal Verification: Keeping Pace with Industrial Needs

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

More and more devices are being designed to process data in digital form including TVs, phones, cameras, music, computers, software, avionics, and encryption devices. Verification is the process of ensuring that designs are correct and that the devices do what is intended. A design error can have important consequences, from having to recall millions of devices resulting in the loss of time and money, to a failure in a mission or safety critical application, possibly causing loss of life. Simulation is the most easily applied method of verification, but it is inherently incomplete and cannot give strong guarantees for correctness. Formal verification is a powerful supplement, or sometimes alternative, to simulation-based approaches. It can produce a mathematical proof of correctness, or expose subtle bugs in a design not uncovered by simulation. Formal methods have seen great progress in the last decade, allowing them to scale up to larger problems where they can replace simulation. Similar progress in the next decade would have a significant impact in not only keeping design costs down and better guarantying safety in critical applications, but also in improving design reliability and enhancing quality by allowing aggressive logic optimization techniques to be applied and successfully verified, a current stumbling block in power optimization. This project proposes to research the fundamental algorithms of formal verification with the goals of (i) innovating new methods in formal verification, including new algorithms and better data structures; (ii) implementing and evaluating these in a common, industrial-strength system, and (iii) promoting the results to the academic, governmental, and industrial communities. Although, the focus of this proposal is on the formal verification of micro-electronic systems and software, the core techniques used in formal verification are very general and can immediately impact many other application areas, such as cryptographic, biologic and health-care systems. Improved scalability of the techniques may well open up wider applicability in new domains such as synthetic biology, software synthesis and areas where safety is a critical issue such as automotive and aviation control systems. In addition, the enhanced ability to verify equivalence of hardware and software systems encourages the use of advanced synthesis techniques, resulting for example in improved speed, power, and area utilization in micro-chips.