@inproceedings{dfb2d9e5bf38437897a26566dc40c1cc,
title = "Automatic property generation for the formal verification of bus bridges",
abstract = "The automatic verification of designs is a challenging task and of high interest due to increasing time-to-market constraints. In this paper, we focus on the verification of bus bridges which are used in many hardware systems to connect two buses running different protocols. We developed an approach to assist the automatic generation of properties from the protocol specification for the formal verification of bus bridges. The technical contribution is that the final set of the verification suite is functionally complete in respect to the underlying verification tool which shows the absence of any verification holes. The approach uses an abstract model of bus bridges in terms of state machines which enables a generic work flow. In experimental evaluations we applied the approach to bus bridges based on the OCP/IP protocol family.",
author = "Mathias Soeken and Ulrich K{\"u}hne and Martin Freibothe and Gorschwin Fe and Rolf Drechsler",
year = "2011",
month = jul,
day = "11",
doi = "10.1109/DDECS.2011.5783129",
language = "English",
isbn = "9781424497560",
series = "Proceedings of the 2011 IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2011",
pages = "417--422",
booktitle = "Proceedings of the 2011 IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2011",
note = "14th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2011 ; Conference date: 13-04-2011 Through 15-04-2011",
}