The University of New South Wales Intel

Hardware/Software Co-Verification

In current industry practice, design and verification of a hardware device and a software driver for it are completely separated, to the point where the driver developer often does not have access to hardware design documentation required to implement a correct driver. We are convinced that a dramatic improvement in the quality of device drivers can be achived via tighter integration of the hardware and software design and verification workflows.

In particular, we observe that the task of hardware verification based on the construction of a testing harness around a simulated model of the device has much in common with the task of writing and testing a driver for the device. Both tasks result in software that is conceptually and functionally similar, yet kept totally separate. The result is a particularly bad case of duplication of effort: the verification code is correct, but is discarded after the device has been manufactured; the driver code is inferior, but used in actual device operation.

In this project we demonstrate that the two tasks, and the software they produce, can and should be unified, and this will result in drastic improvement of device-driver quality and reduction in the development cost and time to market.

Our partners

  • This project is being pursued in collaboration with the OS Research Group at Intel Labs.

People

Publications

plain text PDF Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser
Improved device driver reliability through hardware verification reuse
Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, Newport Beach, CA, USA, March, 2011
plain text PDF Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser
Improved device driver reliability through verification reuse
Proceedings of the 6th Workshop on Hot Topics in System Dependability, Vancouver, BC, Canada, October, 2010