System Modeling and Transformational Design Refinement in ForSyDe.

The scope of the Formal System Design (ForSyDe) methodology is high-level modeling and refinement of systems-on-a-chip and embedded systems. Starting with a formal specification model, that captures the functionality of the system at a high abstraction level, it provides formal design-transformation methods for a transparent refinement process of the system model into an implementation model that is optimized for synthesis. The main contribution of this paper is the ForSyDe modeling technique and the formal treatment of transformational design refinement We introduce process constructors, that cleanly separate the computation part of a process from the synchronization and communication part. We develop the characteristic function for each process type and use it to define semantic preserving and design decision transformations. These transformations are characterized by name, the format of the original process network, the transformed process network, and a design implication. The implication expresses the relation between original and transformed process network by means of the characteristic function. The objective of the refinement process is a model that can be implemented cost efficiently. To this end, process constructors and processes have a hardware and software interpretation which shall facilitate accurate performance and cost estimations. In a study of a digital equalizer example, we illustrate the modeling and refinement process and focus in particular on refinement of the clock domain, communication refinement, and resource sharing. [ABSTRACT FROM AUTHOR]