Skip to main content

Driver Synthesis

Driver Synthesis is one activity of the Trustworthy Systems project.

  • Aim: develop a practical methodology for automatic synthesis of device drivers from existing I/O device specifications.

  • Context: In this project we explore a radically new approach to driver development. We believe that the conventional manual driver development methodology is redundant since all the knowledge required to control the device from software is created during the design of the device and hence a driver for the device can be derived automatically from hardware design artifacts.

    Following this vision, we are implementing a driver synthesis tool called Termite that takes a high-level model of the I/O device written in one of standard hardware modelling languages (SystemC, SystemVerilog, or DML) and a formal specification of the interface between the driver and the operating system and generates a driver implementation in C.

  • Technical research challenges:

    • The state explosion problem. In driver synthesis we are dealing with complex device specifications that contain a large number of state variables. Existing game theoretic algorithms do no scale to systems of such complexity. We are developing techniques to eliminate this barrier, including abstraction and symbolic state space representation.
    • Partial information. In controlling an I/O device, the driver does not have complete visibility of its internal state. Synthesis under partial information involves an additional exponential blow-up in complexity in the worst case. In practice, this blow-up can often be avoided using compositional reasoning and abstraction
    • Practical driver synthesis. The synthesis tool will necessarily impose certain constraints on how device models are written. The goal is to make these constraints easy to understand for hardware engineers and to make sure that existing device models can be reused for synthesis with minimal changes.
  • More information can be found on the project page




  • Our approach to driver synthesis will not work without cooperation from hardware vendors. Therefore we are pursuing this research in collaboration with the OS Research Group at Intel Labs.
  • We are a proud recipient of a 2010 Google Research Award.

Served by Apache on Linux on seL4.