Overview

ForSyDe is a methodology with a formal basis for modeling and design of heterogeneous systems-on-chip and cyber-physical systems that has been developed with the following objectives:

  • System design must start at a high level of abstraction. The designer shall focus on functionality, and low-level implementation details shall not be an issue at the design stage;
  • Design methodology must give a solid base for the incorporation of formal methods. This means that verification must be a first class citizen from the start;
  • Abstraction gap between specification and implementation must be bridged by formal refinement techniques.

These goals are achieved in practice through an ecosystem of tools which are developed in line with scientific publications. News about ForSyDe-related research and development can be seen in the news page as well as in the GitHub organization page.

Our Name

ForSyDe is officially an acronym for Formal System Design.

ForSyDe also resembles with the word foresight. According to the Merriam-Webster dictionary

foresight noun
fore·​sight ; \ˈfȯr-ˌsīt\

Definition of foresight

  1. an act or the power of foreseeing : prescience
    Through foresight she could tell what the outcome would be.

  2. provident care : prudence
    had the foresight to invest his money wisely

  3. an act of looking forward
    also : a view forward

This definition captures the essence of our vision: formal design should pave a clear way towards a correct implementation. Through a formal model a designer can thus foresee the desired system realization. This is also the story behind our logo.

Our Vision

ForSyDe envisions a correct-by-construction design flow by combining:

  • Modelling framework based on theory of models of computation;
  • Predictable platforms providing guarantees for extra functional properties.

The design flow can be sketched as below:

The key components of the design flow are:

  • Formally analysable application models based on a formal foundation to enable formal analysis and reasoning;
  • Predictable platforms providing service guarantees;
  • Analysis methods enabling powerful design tools;
  • Design entry language based on the formal foundation enabling
    • Simulation of the application model;
    • Automatic abstraction of formal analysable model.

Tools

Visit the Tools page for our current portfolio of tools supporting this design process and links to further documentation, and our GitHub organization page for a list with all projects published under the ForSyDe umbrella. Among them we highlight:

  • ForSyDe-Shallow: a shallow-EDSL capturing the main modeling concepts of ForSyDe.
  • ForSyDe-Deep: a deep-embedded EDSL which can synthesize a subset of ForSyDe models down to VHDL.
  • ForSyDe-Atom: a shallow-EDSL which extends the ForSyDe modeling scope with concepts like “layers” and “atoms”.
  • ForSyDe-SystemC: is the SystemC embedding of ForSyDe, which uses the host language for both simulation, structure parsing and C code extraction.
  • DeSyDe: the previous design space exploration tool in the ForSyDe design flow. It is based on constraint programming and provides certificates of feasibility and optimality for a a design.
  • IDeSyDe: the current design space exploration tool in ForSyDe design flow. It is based on the concept of design space identification in order to systematically combine and extend different design space exploration scenarios without sacrificing exploration performance.