A SystemC Semantics in Guarded Assignment Systems and Its Applications with VERDS

Author

Naiju Zeng ; Wenhui Zhang

Author_Institution

State Key Lab. of Comput. Sci., Univ. of Chinese Acad. of Sci., Beijing, China

Volume

1

fYear

2013

fDate

2-5 Dec. 2013

Firstpage

371

Lastpage

379

Abstract

SystemC is an IEEE standard system-level language and has been widely adopted in development of embedded systems. Due to the complexity of SystemC specifications, formal verification of SystemC is still at a preliminary stage and no complete formal semantics for SystemC exists so far. This work presents an executable semantics of a subset of SystemC in guarded assignment systems and its applications with the symbolic model checker VERDS. The semantics preserves most of the structures of SystemC for hardware-software co-design. And the guarded assignment system is a general model which is widely supported by many model checkers. Among all the symbolic model checkers, VERDS is a competitive one with the new data structure ternary boolean diagrams (TBDs). The scalability and the efficiency of the applications of our semantics with VERDS have been demonstrated by experimental results.

Keywords

Boolean functions; C language; IEEE standards; data structures; decision diagrams; embedded systems; formal specification; formal verification; hardware-software codesign; programming language semantics; IEEE standard system-level language; SystemC formal verification; SystemC semantics; SystemC specifications complexity; TBD; data structure ternary Boolean diagrams; embedded system development; executable semantics; guarded assignment systems; hardware-software co-design; symbolic model checker VERDS; Generators; Model checking; Printers; Process control; Receivers; Semantics; Software; SystemC; VERDS; model checking; semantics;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference (APSEC), 2013 20th Asia-Pacific

Conference_Location

Bangkok

ISSN

1530-1362

Print_ISBN

978-1-4799-2143-0

Type

conf

DOI

10.1109/APSEC.2013.57

Filename

6805428