Collaborative: Software Verification for Hardware Models

点击翻译按钮获取中文摘要

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.