Using Reo for formal specification and verification of system designs

Author

Razavi, Niloofar ; Sirjani, Marjan

Author_Institution

Dept. of Electr. & Comput. Eng., Tehran Univ.

fYear

2006

fDate

27-30 July 2006

Firstpage

113

Lastpage

122

Abstract

In this paper, we introduce a component-based approach to specify and verify system-level designs. A coordination language, Reo, is used to support hierarchical design and verification. We move from functional specification to implementation through different levels of abstraction, considering TLM/RTL mixed levels and hardware/software co-designs. We discuss the mapping of a system design written in SystemC to Reo circuits, and how we can compositionally construct its behavior using constraint automata. A case study is used to show the applicability of our approach

Keywords

automata theory; formal specification; formal verification; hardware description languages; hardware-software codesign; Reo circuits; SystemC; TLM/RTL mixed levels; component-based approach; constraint automata; coordination language; formal specification; formal verification; functional specification; hardware/software codesign; hierarchical design; system-level designs; Automata; Circuits; Computer science; Formal specifications; Formal verification; Hardware; Microelectronics; Process design; Software systems; System-level design;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Methods and Models for Co-Design, 2006. MEMOCODE '06. Proceedings. Fourth ACM and IEEE International Conference on

Conference_Location

Napa, CA

Print_ISBN

1-4244-0421-5

Type

conf

DOI

10.1109/MEMCOD.2006.1695912

Filename

1695912