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

越来越多的设备被设计为以数字形式处理数据，包括电视、电话、相机、音乐、计算机、软件、航空电子设备和加密设备。验证是确保设计正确且器械按预期运行的过程。设计错误可能会产生重要后果，从不得不召回数百万台设备导致时间和金钱损失，到使命或安全关键应用失败，可能导致生命损失。模拟是最容易应用的验证方法，但它本质上是不完整的，不能提供强有力的正确性保证。形式化验证是对基于模拟的方法的有力补充，有时甚至是替代。它可以产生正确性的数学证明，或者暴露设计中未被模拟发现的细微错误。形式化方法在过去的十年中取得了巨大的进步，使它们能够扩展到更大的问题，从而取代模拟。未来十年的类似进展将产生重大影响，不仅可以降低设计成本，提高关键应用的安全性，还可以通过应用并成功验证积极的逻辑优化技术来提高设计可靠性和质量，这是当前功率优化的绊脚石。该项目旨在研究形式验证的基本算法，目标是（i）创新形式验证的新方法，包括新算法和更好的数据结构;（ii）在一个通用的工业强度系统中实现和评估这些方法;以及（iii）将结果推广到学术界，政府和工业界。虽然，这个建议的重点是对微电子系统和软件的形式验证，在形式验证中使用的核心技术是非常普遍的，可以立即影响许多其他应用领域，如密码，生物和医疗保健系统。这些技术的可扩展性的提高可能会在新的领域（如合成生物学、软件合成）以及安全性是关键问题的领域（如汽车和航空控制系统）中开辟更广泛的适用性。此外，验证硬件和软件系统的等效性的增强能力鼓励使用先进的合成技术，从而例如提高微芯片的速度、功率和面积利用率。

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.