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