Authors: Nesrine Harrath; Bruno Monsuez
Addresses: Laboratory of Electronics and Computer Engineering, ENSTA ParisTech, 32 Bd Victor, 75739 Paris Cedex 15, France. ' Laboratory of Electronics and Computer Engineering, ENSTA ParisTech, 32 Bd Victor, 75739 Paris Cedex 15, France
Abstract: SystemC is becoming a de facto standard for the system level description of system-on-chip. However, most formal verification techniques used for verifying hardware components use a very low level design, usually a netlist or RTL, but time-to-market requirements have rushed the industry towards design paradigms that offer a very high level of abstraction. As part of this process, we propose a verification methodology for SystemC designs based on a combination of static code analysis and SystemC simulation semantics. We propose a new formal hybrid model for verifying properties of SystemC models at the transaction level within a delta-cycle. We prove that this model is compositional since it guarantees that possible interference between the SystemC process and its environment is already taken into account. Besides, it describes both functional and non-functional aspects of SystemsC designs, it is amenable for adding more constraints about system behaviour such as time properties and counters. Finally, we infer algorithms for symbolic composition and reduction of automata to eventually model the whole system behaviour.
Keywords: SystemC; compositional verification; automata; time analysis; model checking; system-on-chip; modelling.
International Journal of Critical Computer-Based Systems, 2012 Vol.3 No.1/2, pp.60 - 95
Published online: 24 Jan 2012 *Full-text access for editors Access for subscribers Purchase this article Comment on this article