SystemC waiting-state automata - ENSTA Paris - École nationale supérieure de techniques avancées Paris Accéder directement au contenu
Chapitre D'ouvrage Année : 2012

SystemC waiting-state automata

Résumé

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.
Fichier non déposé

Dates et versions

hal-00672901 , version 1 (22-02-2012)

Identifiants

Citer

Nesrine Harrath, Bruno Monsuez. SystemC waiting-state automata. inderscience. International Journal of Critical Computer-Based Systems (IJCCBS), inderscience, pp. 60 - 95, 2012, Vol. 3, No.1/2, ⟨10.1504/IJCCBS.2012.045077⟩. ⟨hal-00672901⟩

Collections

ENSTA ENSTA_U2IS
66 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More