View article

Device drivers are hard to develop and are notoriously unreliable [13, 20]. While constant innovation in the area of electronic design automation has led to dramatic improvements in the IC design process, device driver development practices have not changed much since the days of mainframe computers. As a result, it is common nowadays for a product release to be delayed by driver rather than silicon issues [42]. To address this long-standing problem, we propose a new driver development methodology that will allow faster creation of device drivers with fewer defects. The innovation at the heart of our methodology is the automatic synthesis of correct-by-construction device drivers from a formal model of the hardware device and a specification of the driver/OS interface. Our methodology has the following crucial properties.• Dramatic reduction in cost of driver development, maintenance and QA. This is achieved by synthesizing drivers automatically from existing device specifications provided by hardware designers as transaction-level device models (TLMs).• Support for hardware/software co-design and co-verification. Our approach allows device drivers to be created, tested, and formally verified early in the product design workflow, before the hardware device is available in silicon. The availability of the device driver in turn facilitates evaluation and validation of the hardware design.• Strong functional correctness guarantees. Our correct-by-construction approach to synthesis, combined with formal verification to detect bugs in input specifications and the synthesis algorithm, yields a high degree of confidence in the resulting device driver code.