@inproceedings{8bafafed909245c0b85369664ebb945f,
title = "HW/SW co-verification of embedded systems using bounded model checking",
abstract = "Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes more and more important. In this paper we present an integrated approach for formal verification of hardware and software. The approach is demonstrated on a RISC CPU. The verification is based on bounded model checking. Besides correctness proofs of the underlying hardware the hardware/software interface and programs using this interface can be formally verified.",
keywords = "Bounded model checking, Embedded systems, Formal verification, Hardware/software co-verification, PSL, SystemC",
author = "Daniel Gro{\ss}e and Ulrich K{\"u}hne and Rolf Drechsler",
year = "2006",
month = nov,
day = "16",
language = "English",
isbn = "1595933476",
series = "Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI",
pages = "43--48",
booktitle = "GLSVLSI'06 - Proceedings of the 2006 ACM Great Lakes Symposium on VLSI",
note = "GLSVLSI'06 - 2006 ACM Great Lakes Symposium on VLSI ; Conference date: 30-04-2006 Through 02-05-2006",
}