is aimed at giving formal specifications of SystemC designs and to
perform formal analysis of SystemC processes. Furthermore, is a
single-formalism that can be used for specifying concurrent systems,
finite state systems and real-time systems (as in SystemC). Desired properties
(e.g. safety and liveness) of these systems specified in
can be verified with existing formal
verification tools (e.g. SMV, SPIN and Uppaal) by translating them formally
into different formalisms that are the input languages
of the formal verification tools (i.e. single-formalism-multi-solution).
Transaction Level Modelling (TLM) is a relatively young kind of approach meant to ease the handling of the constantly growing complexity of electronic systems; by raising the level of abstraction it allows system architects, embedded software engineers, and system developers, to explore architectural alternatives, to start software development, and to produce raw performance estimation at a much earlier stage than it would be possible if a Register Transfer Level (RTL) description of the system were used as platform reference.
With alternatives exploration in mind, the main advantage of TLM is the simulation speed-up that it offers w.r.t. cycle-accurate representation, essentially due to the different abstraction level, which turns into a much smaller amount of information to be handled. The main disadvantage shown by TLM, so far, is the lack of a formal semantics, that could be used both for consistency checking during description refinement, and for property checking on untimed descriptions, mainly aimed at checking functional correctness on an abstraction of the final system. Various attempts to give TLM a formal background have already been made, but none of those has proposed a framework to allow checking on specific aspects of the component being designed with the most suited formal checking tool. To reach such a goal we have focused our attention on SystemC as a language for TLM, and selected as the language to formally represent SystemC designs.
In the frame of a tight collaboration between industrial entities and
research institute CEOL (Centre for Efficiency-Oriented Languages), several tools for
are currently being developed. These tools
enable automatic translations from SystemC codes to
specifications and from specifications to various formalisms
that are the input languages of some existing formal verification
tools. Using tools in combination
with some formal verification tools yields automatic verifications of SystemC
designs via specifications (for different verification
This research activity is currently funded by
Solari - Hong Kong (http://www.solari-hk.com/)
and partnered with
International Software and Productivity Engineering Institute - USA (http://www.intspei.com),
Intelligent Support Ltd. - United Kingdom (http://www.isupport-ltd.co.uk)
Minteos - Italy (http://www.minteos.com).
For questions, suggestions and comments, please send mail to SystemCFL@gmail.com