id: 05977321
dt: j
an: 05977321
au: Hojjat, Hossein; Mousavi, Mohammad Reza; Sirjani, Marjan
ti: Formal analysis of systemc designs in process algebra.
so: Fundam. Inform. 107, No. 1, 19-42 (2011).
py: 2011
pu: Polish Mathematical Society, Warsaw; IOS Press, Amsterdam
la: EN
cc: 
ut: systemc; process algebra; formal verification; mCRL2
ci: 
li: doi:10.3233/FI-2011-391
ab: Summary: 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
    designs by providing a mapping to the process algebra mCRL2. Our
    mapping formalizes both the simulation semantics as well as exhaustive
    state-space exploration of SystemC designs. By exploiting the existing
    reduction techniques of mCRL2 and also its model-checking tools, we
    efficiently locate the race conditions in a system and resolve them. A
    tool is implemented to automatically perform the proposed mapping. This
    mapping and the implemented tool 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.
rv: