Publications:Formal analysis of systemc designs in process algebra
From CERES
| Title | Formal analysis of systemc designs in process algebra |
|---|---|
| Author | Hossein Hojjat and Mohammad Reza Mousavi and Marjan Sirjani |
| Year | 2011 |
| PublicationType | Journal Paper |
| Journal | Fundamenta Informaticae |
| HostPublication | |
| DOI | http://dx.doi.org/10.3233/FI-2011-391 |
| Conference | |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:583421 |
| 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 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. |
