Title :
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
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;
Conference_Titel :
Software Engineering Conference (APSEC), 2013 20th Asia-Pacific
Conference_Location :
Bangkok
Print_ISBN :
978-1-4799-2143-0
DOI :
10.1109/APSEC.2013.57
