SystemC is a system level language recently proposed to raise the abstraction level for embedded systems design and verification. We propose a verification methodology for SystemC designs based on a combination of static code analysis and SystemC semantics described with abstract state machines (ASM). We abstract the source SystemC design into hypergraphs to keep an abstract (simplified) view of the design including only processes status, activation conditions and order of execution. This latter is then modeled with ASMs and compiled with the AsmL tool in order to generate a finite state machine that can be used for formal verification by external tools linked to ASM, such as model checkers or theorem provers. We can also generate a .NET representation of the abstracted SystemC model to guide test vectors generation and perform coverage analysis within the .NET framework. Our approach solves a number of problems classical verification techniques do face when used with SystemC through the efficient handling of the object--oriented aspect of SystemC and the complexity of its simulation environment.

Download PDF file: (PDF file)

Send comments and suggestions to: amjad@ece.concordia.ca