Process algebraic verification of SystemC codes

H. Hojjat, M. Mousavi, M. Sirjani

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

6 Citations (Scopus)

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 processalgebraic 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.
Original languageEnglish
Title of host publicationProceedings 8th International Conference on Application of Concurrency to System Design (ACSD'08, Xian, China, June 23-27, 2008)
PublisherInstitute of Electrical and Electronics Engineers
Pages62-67
ISBN (Print)978-1-4244-1838-1
DOIs
Publication statusPublished - 2008

Fingerprint Dive into the research topics of 'Process algebraic verification of SystemC codes'. Together they form a unique fingerprint.

Cite this