Collaborative: Software Verification for Hardware Models

0702603Ranjit JhalaUniversity of California - sd协作：硬件模型的软件验证现代微处理器是有史以来构建的一些最复杂的工程工件，它们的设计复杂性每一代都在增加。正确性是微处理器的基本问题：所有软件应用程序都隐含地假设处理器的正确操作。正如臭名昭著的奔腾分区错误所证明的那样，最终系统中错误的成本是令人望而却步的。验证这些复杂的设计是一个真正的挑战。当前设计验证的广泛模拟实践是不够的，因为它只能行使状态空间的一小部分，留下许多关键属性未检查。本研究将形式验证技术应用于验证复杂处理器的高级模型的正确性。用C、c++或SystemC等编程语言编写的高级处理器模型，作为后续硬件实现的黄金参考模型，正变得越来越普遍。虽然硬件和处理器验证一直是一个活跃的研究领域，但本研究的新颖之处在于将软件验证中开发的高级设计结构和强大的自动化抽象技术（如谓词抽象、形状分析和原子性）与硬件验证（如证明分解和内存抽象）的见解相结合。与硬件验证中通常使用的位级模型不同，组合技术可能产生更紧凑的模型，帮助推理扩展到大型系统，例如现代微体系结构的完整描述。这项研究将与研究人员的教育目标相结合，即开发研究生水平的课程，将形式核查原则与可靠的系统设计原则结合起来。

0702603Ranjit JhalaUniversity of California - SDCollaborative: Software Verification for Hardware ModelsModern microprocessors are some of the most complex engineering artifacts ever constructed, and their design complexity has been increasing in every generation. Correctness is a fundamental concern for microprocessors: all software applications implicitly assume correct operation of the processor. As demonstrated by the infamous Pentium division bug, the cost of bugs in the final system is prohibitive. Validating these complex designs is a real challenge. Current practice of extensive simulation for design validation is inadequate as it can only exercise a small portion of the state space, leaving many key properties unchecked.This research applies techniques from formal verification to verifying the correctness of higher-level models of complex processors. Higher level processor models written in programming languages like C, C++, or SystemC, are becoming more and more prevalent as golden reference models for subsequent hardware implementations. While hardware and processor verification have been an active area of research, the novelty of this research is to merge the high-level design structure and powerful automated abstraction techniques developed in software verification (such as Predicate Abstraction, Shape Analysis, and Atomicity) with the insights from hardware verification (such as proof decomposition and memory abstraction). Instead of the usual bit-level models used in hardware verification, the combined techniques are likely to produce more compact models, helping the reasoning to scale to large systems, such as the complete description of a modern microarchitecture.The research will tie in with the investigators' educational objectives of developing graduate level courses that combine the principles of formal verification with the principles of reliable system design.