“School of Computer Science”

Back to Papers Home
Back to Papers of School of Computer Science

Paper   IPM / Computer Science / 10886
School of Computer Science
  Title:   Process algebraic verification of SystemC codes
  Author(s): 
1.  H. Hojjat
2.  M.R. Mousavi
3.  M. Sirjani
  Status:   In Proceedings
  Proceeding: ACSD
  Year:  2008
  Pages:   62-67
  Publisher(s):   IEEE
  Supported by:  IPM
  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.

Download TeX format
back to top
scroll left or right