Formal Analysis of SystemC Designs in Process Algebra

Hossein Hojjat, MohammadReza Mousavi, Marjan Sirjani, Fundamenta Informaticae, 107(1):19--42, 2011.

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.

@article{MousaviFI2010,
    author      = "Hojjat, Hossein and Mousavi, MohammadReza and Sirjani, Marjan",
    title       = "Formal Analysis of SystemC Designs in Process Algebra",
    journal     = "Fundamenta Informaticae",
    volume      = "107",
    number      = "1",
    pages       = "19--42",
    year        = "2011"
}