Publications:Process algebraic verification of SystemC codes

Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Process algebraic verification of SystemC codes
Author H. Hojjat and Mohammad Reza Mousavi and M. Sirjani
Year 2008
PublicationType Conference Paper
HostPublication Application of Concurrency to System Design, 2008. ACSD 2008. 8th International Conference on
Conference 8th International Conference on Application of Concurrence System Design, Xian, PEOPLES R CHINA, JUN 23-27, 2008
Diva url
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.