Process algebraic verification of SystemC codes

H. Hojjat; M. Mousavi; M. Sirjani

doi:10.1109/ACSD.2008.4574597

Process algebraic verification of SystemC codes

H. Hojjat, M. Mousavi, M. Sirjani

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

6 Citations (Scopus)

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 processalgebraic 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.

Original language	English
Title of host publication	Proceedings 8th International Conference on Application of Concurrency to System Design (ACSD'08, Xian, China, June 23-27, 2008)
Publisher	Institute of Electrical and Electronics Engineers
Pages	62-67
ISBN (Print)	978-1-4244-1838-1
DOIs	https://doi.org/10.1109/ACSD.2008.4574597
Publication status	Published - 2008

Access to Document

10.1109/ACSD.2008.4574597

Cite this

@inproceedings{3b40972b1bff4ba9aabb0982c4d98218,

title = "Process algebraic verification of SystemC codes",

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 processalgebraic 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.",

author = "H. Hojjat and M. Mousavi and M. Sirjani",

year = "2008",

doi = "10.1109/ACSD.2008.4574597",

language = "English",

isbn = "978-1-4244-1838-1",

pages = "62--67",

booktitle = "Proceedings 8th International Conference on Application of Concurrency to System Design (ACSD'08, Xian, China, June 23-27, 2008)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

}

Process algebraic verification of SystemC codes. / Hojjat, H.; Mousavi, M.; Sirjani, M.
Proceedings 8th International Conference on Application of Concurrency to System Design (ACSD'08, Xian, China, June 23-27, 2008). Institute of Electrical and Electronics Engineers, 2008. p. 62-67.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Process algebraic verification of SystemC codes

AU - Hojjat, H.

AU - Mousavi, M.

AU - Sirjani, M.

PY - 2008

Y1 - 2008

N2 - 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 processalgebraic 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.

AB - 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 processalgebraic 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.

U2 - 10.1109/ACSD.2008.4574597

DO - 10.1109/ACSD.2008.4574597

M3 - Conference contribution

SN - 978-1-4244-1838-1

SP - 62

EP - 67

BT - Proceedings 8th International Conference on Application of Concurrency to System Design (ACSD'08, Xian, China, June 23-27, 2008)

PB - Institute of Electrical and Electronics Engineers

ER -

Process algebraic verification of SystemC codes

Abstract

Access to Document

Fingerprint

Cite this