SystemC waiting state automata Online publication date: Tue, 24-Jan-2012
by Nesrine Harrath; Bruno Monsuez
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 3, No. 1/2, 2012
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.
Online publication date: Tue, 24-Jan-2012
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.If you still need assistance, please email firstname.lastname@example.org