Traineeship: Analysis of SDF graphs using a model-checker
Description
Multimedia applications often have throughput constraints. The constraints must be met while using as little resources as possible. It is therefore important to find implementations that meet the constraints and minimize the resource usage.
These applications are frequently specified as synchronous dataflow graphs. Communication between actors of these graphs requires storage space. The model-checker SPIN can be used to determine the minimal storage capacity to execute the graph under the given throughput constraint.
Currently, the SDF graphs are translated by hand to PROMELA, the input language of SPIN. This is a tedious task that may introduce errors. An objective of the project is to automate this process. For this purpose, an XML-based description format for SDF graphs must be defined. Given a description of the SDF graph in this format, a tool should generate the PROMELA code for a (timed) SDF graph.
Data communicated between actors in an SDF graph must be stored. In resource constrained systems, one wants to minimize this storage space. Sometimes it might be possible that a number of channels can use the same storage space. By changing the order (and time) in which data is produced and consumed, the storage space required can be minimized. Currently, implementations exist in PROMELA to deal with SDF graphs in which all channels share all storage space and in which each channel has its own storage space. A mixture of these two cases is not supported. It should be researched in this project how the SDF implementations in PROMELA can be extended to support this situation.
Model-checkers like SPIN translate the input model to an automaton. The state-space represented by this automaton is exhaustively traversed to check properties (called claims) of the model. The size of the state-space is determined by the automaton which on its turn is determined by the input model. Hence, different descriptions of the same model may result in different sizes for the state-space. This fact should be taken into consideration when a PROMELA model is developed.
When we use SPIN to prove a claim invalid, it generates a trace through the state-space which invalidates it. This trace contains in fact a periodic schedule of the SDF graph within the given buffer size and possibly timing constraints. A goal of the project is to extract the schedule from this trace and to present it to a user in a meaningful way. Other information such as the length of the transient phase before the schedule enters the periodic regime or the distribution of the buffers over the various fifos must also be extracted from the trace and provided to the user.
Often a designer is interested in exploring a trade-off between the used memory in the system and the throughput or latency. A design space exploration is then performed to find these trade-offs. Currently, the exploration is performed manually. The designer must change the values (e.g. bound on the buffer sizes) by hand. After that SPIN is run to see whether a periodic schedule within these constraints exists. This is a time consuming process that can be automated. An objective of this project is to create a tool that can automatically explore the design space within user specified bounds. The design space that must be evaluated during this exploration might become very large. As a result, it will not always be possible to find the minimal buffer size for a given timing constraint. Yet the design space has certain properties that can be exploited. Methods must be developed and implemented to deal with this situation and to efficiently traverse and prune the design space.
To test all developed techniques, a case study should be performed. The complexity of the design should be chosen such that it can be used to explore the boundaries of the approach. In other words, it should answer the question when it becomes impossible to find optimal solutions. The most logical application for this purpose seems the modem application.
Duration
December 2004 - March 2005
Student
Supervisor
|
