Difference between revisions of "Publications:Process algebraic verification of SystemC codes"
From CERES
(Created page with "<div style='display: none'> == Do not edit this section == </div> {{PublicationSetupTemplate|Author=H. Hojjat, Mohammad Reza Mousavi, M. Sirjani |PID=584683 |Name=Hojjat, H. (...") |
(No difference)
|
Latest revision as of 04:43, 26 June 2014
Title | Process algebraic verification of SystemC codes |
---|---|
Author | H. Hojjat and Mohammad Reza Mousavi and M. Sirjani |
Year | 2008 |
PublicationType | Conference Paper |
Journal | |
HostPublication | Application of Concurrency to System Design, 2008. ACSD 2008. 8th International Conference on |
DOI | http://dx.doi.org/10.1109/ACSD.2008.4574597 |
Conference | 8th International Conference on Application of Concurrence System Design, Xian, PEOPLES R CHINA, JUN 23-27, 2008 |
Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584683 |
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. |