The ForSyDe Methodology

The ForSyDe (Formal System Design) methodology has been developed with the objective to move system design (i.e. System on Chip, Hardware and Software systems) to a higher level of abstraction and to bridge the abstraction gap by transformational design refinement.

ForSyDe is based on carefully selected formal foundations. First, the designer must supply a initial specification model, which

  • Can mix different Models of Computation (MoCs) i.e. Synchronous MoC, Untimed MoC ...
  • Is modelled by a network of processes interconnected by signals. Each process is created by a process constructor, allowing to separate communication and computation.

Then, the abstract specification model is refined by different Design Transformations into a detailed implementation model, which is finally translated into a target implementation language.

ForSyDe research currently pursues two main goals:

System modeling with heterogeneous models of computation

We have developed libraries for different computational models allowing the simulation of heterogeneous systems using Haskell and SystemC. The libraries stretch from continuous time to synchronous time models. Using ForSyDe's shallow-embedded DSL (Domain Specific Language) we are able to simulate electronic systems with analog and digital parts.

Refinement and Implementation Mapping of the Specified Models

We have outlined a methodology for transformational design refinement. The system, initially described as an abstract specification model, is refined into a more detailed implementation through semantic preserving and non-semantic preserving design transformations. Then, the resulting implementation model is translated into a target language for a target platform.

So far, we have centered our efforts around the synchronous computational model. As part of this work, we have created a deep-embedded DSL with which is possible to generate GraphML diagrams and synthesizable VHDL out of syncrhonous system descriptions. In addition, it is possible to simulate systems descriptions mixing the deep-embedded and shallow-embedded APIs.