Title: SystemC waiting state automata

 

Author: 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

 

Journal: Int. J. of Critical Computer-Based Systems, 2012 Vol.3, No.1/2, pp.60 - 95

 

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.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2012.045077

 

Available online 24 Jan 2012

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article