Collaborative: Software Verification for Hardware Models

0702743加州大学Rupak MajudarUniversity-SD协作：硬件模型的软件验证现代微处理器是有史以来构建的最复杂的工程制品之一，其设计复杂性在每一代人中都在增加。正确性是微处理器的一个基本问题：所有软件应用程序都隐含地假定处理器的操作是正确的。正如臭名昭著的奔腾除法错误所证明的那样，最终系统中的错误成本令人望而却步。验证这些复杂的设计是一个真正的挑战。为了验证复杂处理器高层模型的正确性，将形式化验证技术应用到复杂处理器高层模型的验证中，提出了一种基于状态空间的验证方法。用C、C++或SystemC等编程语言编写的高级处理器模型正变得越来越普遍，作为后续硬件实现的黄金参考模型。虽然硬件和处理器验证一直是一个活跃的研究领域，但本研究的新颖之处在于将软件验证中发展起来的高级设计结构和强大的自动抽象技术(如谓词抽象、形状分析和原子性)与硬件验证(如证明分解和内存抽象)的见解相结合。与通常用于硬件验证的位级模型不同，组合技术可能会产生更紧凑的模型，有助于将推理扩展到大型系统，例如对现代微体系结构的完整描述。这项研究将与研究人员开发研究生级别课程的教育目标相一致，该课程将形式验证的原则与可靠的系统设计原则相结合。

0702743Rupak MajumdarUniversity 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.