A framework for automated HW/SW co-verification of SystemC designs using tmed automata [Elektronische Ressource] / vorgelegt von Paula Herber

© Paula Herber

Sujets

• Informatik

Informations

• Publié par: technische_universitat_berlin
• Publié le: 01 janvier 2010
• Nombre de lectures: 19
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

A Framework for Automated HW/SW Co-Veri cation
of SystemC Designs using Timed Automata
vorgelegt von
Diplom-Ingenieur
Paula Herber
von der Fakultat IV { Elektrotechnik und Informatik
der Technischen Universitat Berlin
zur Erlangung des akademischen Grades
Doktor der Ingenieurwissenschaften
{ Dr.-Ing. {
genehmigte Dissertation
Promotionsausschuss:
Vorsitzender: Prof. Dr. Ben Juurlink
Berichtende: Prof. Dr. Sabine Glesner
Berichtender: Prof. Dr. Rolf Drechsler
Tag der wissenschaftlichen Aussprache: 25. Februar 2010
Berlin 2010
D 83Abstract
Embedded systems are usually composed of deeply integrated hardware and
software components. They are often used in domains where a failure results
in high nancial losses or even in serious injury or death. As a consequence, it
is indispensable to ensure the correctness of the digital components that con-
trol these systems with systematic and comprehensive verication techniques.
To model and simulate complex HW/SW systems, the system level design lan-
guage SystemC is widely used. However, the co-verication techniques used
for SystemC are mostly ad-hoc and non-systematic. With that, it is either
very expensive to verify a given design, or the results are not reliable.
In this thesis, we present an approach to overcome this problem by a sys-
tematic, comprehensive, and formally founded quality assurance process, which
allows automated co-verication of digital HW/SW systems that are modeled
in SystemC. The main idea is to apply model checking to verify that an abstract
design meets a requirements specication and to generate conformance tests to
check whether rened designs conform to this abstract design. With that, we
obtain guarantees about the abstract design, which serves as a specication,
and we can ensure the consistency of each re ned design to that. The result
is a HW/SW co-veri