HW/SW co-verification of a RISC CPU using bounded model checking

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the 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.

Original languageEnglish
Title of host publicationProceedings - Sixth International Workshop on Microprocessor Test and Verification
Subtitle of host publicationCommon Challenges and Solutions, MTV 2005
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages133-137
Number of pages5
ISBN (Print)0769526276, 9780769526270
DOIs
Publication statusPublished - 1 Jan 2005
Externally publishedYes
Event2005 6th International Workshop on Microprocessor Test and Verification - Austin, TX, United States
Duration: 3 Nov 20054 Nov 2005

Publication series

NameProceedings - International Workshop on Microprocessor Test and Verification
ISSN (Print)1550-4093

Conference

Conference2005 6th International Workshop on Microprocessor Test and Verification
Country/TerritoryUnited States
CityAustin, TX
Period3/11/054/11/05

Fingerprint

Dive into the research topics of 'HW/SW co-verification of a RISC CPU using bounded model checking'. Together they form a unique fingerprint.

Cite this