Collaborative: Software Verification for Hardware Models

University Of California-Los Angeles, Los Angeles CA

Investigators

Abstract

0702743 Rupak Majumdar University of California - SD Collaborative: Software Verification for Hardware Models Modern 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.