Sciweavers

Share
DATE
2009
IEEE

Correct-by-construction generation of device drivers based on RTL testbenches

9 years 6 months ago
Correct-by-construction generation of device drivers based on RTL testbenches
Abstract—The generation of device drivers is a very time consuming and error prone activity. All the strategies proposed up to now to simplify this operation require a manual, even formal, specification of the device driver functionalities. In the systemlevel design, IP functionalities are tested by using testbenches, implemented to contain the communication protocols to correctly interact with the device. The aim of this paper is to present a methodology to automatically generate device drivers from the testbench of any RTL IP. The only manual step required is to tag the states corresponding to the different device functionalities. The Extended Finite State Machines (EFSMs) are then used to create a correct-by-construction two-level device driver: the lower level deals with architectural choices, while the higher one is derived from the EFSMs and it implements the communication protocols. The effectiveness of this methodology has been proved by applying it to a platform provided by...
Nicola Bombieri, Franco Fummi, Graziano Pravadelli
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where DATE
Authors Nicola Bombieri, Franco Fummi, Graziano Pravadelli, Sara Vinco
Comments (0)
books