SystemC waiting state automata. (1st January 2012)

• Record Type: Journal Article
• Authors: Harrath, Nesrine; Monsuez, Bruno
• Is Part Of: International journal of critical computer-based systems. Volume 3:Number 1/2(2012)
• Page Start: 60
• Page End: 95
• Publication Date: 2012-01-01
• Subjects: SystemC -- compositional verification -- automata -- time analysis -- model-checking; Computer systems -- Periodicals; Computer architecture -- Periodicals; 004
• Languages: English
• ISSNs: 1757-8779

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.