Process algebraic verification of SystemC codes

Author

Hojjat, H. ; Mousavi, M.R. ; Sirjani, M.

Author_Institution

Inst. for Studies in Theor. Phys. & Math., Univ. of Tehran, Tehran

fYear

2008

fDate

23-27 June 2008

Firstpage

62

Lastpage

67

Abstract

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC codes by providing a mapping to the process algebra mCRL2. The outstanding advantages of mCRL2 are the support for different data types and a powerful tool-set for model reduction and analysis. A tool is implemented to automatically perform the proposed mapping. This translation enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.

Keywords

hardware description languages; process algebra; program verification; IEEE standard system-level language; SystemC code; data type; formal analysis; hardware/software codesign; mCRL2 process algebra; model reduction tool-set; pipelined MIPS processor; process algebraic verification; single-cycle processor; Algebra; Computer industry; Hardware; Logic; Mathematics; Physics; Reduced order systems; Sequential circuits; Software standards; System-level design;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 2008. ACSD 2008. 8th International Conference on

Conference_Location

Xian

ISSN

1550-4808

Print_ISBN

978-1-4244-1838-1

Electronic_ISBN

1550-4808

Type

conf

DOI

10.1109/ACSD.2008.4574597

Filename

4574597