Vachoux A. Applications of Specification and Design Languages for SoCs

Selected papers from 'FDL 2005', Springer, 2006, 318 p.This thematic area of FDL’05 deals with specification-driven designs,
formal verification techniques, mixed formal and simulation-based verification techniques, formal languages (B, CTL, Z, temporal logic, etc.), synchronous languages (Esterel, etc.), modeling concepts (e.g., StateCharts, Petri
Nets, finite state machines (FSMs), dataflow models, etc.), and models of
computation.
In this part, two contributions in this thematic area addressing two important
aspects in system design have been selected. The first aspect is assertion-based
design methods. Using assertions in design models provides means to write
specifications in a formal way that can be unambiguously understood and verified by designers and tools. They also provide a strong link between design
and verification activities early in the design flow. One emerging assertion language is the Property Specification Language (PSL). PSL is an IEEE standard
that has been designed to unify static (formal) and dynamic (simulation-based)
verification and that is currently supported by many commercial electronic design automation (EDA) tools. Chapter 1 by Dominique Borrione, Miao Liu,
Pierre Ostier, and Laurent Fesquet, entitled “PSL-Based Online Monitoring
of Digital System,” presents an original method for generating hardware assertion monitors. Such monitors capture the occurrence of events specified by
logical and temporal properties originally written as PSL assertions. The chapter illustrates the approach on an experimental field programmable gate-array
(FPGA)-based platform that includes a Nios-embedded processor.
The second aspect deals with the design of systems-on-chip (SOC) architecture and the mapping onto a network-on-chip (NoC) architecture. NoC is
an emerging paradigm that aims at providing efficient on-chip communication
services capable of supporting large quantities of heterogeneous processing
components (e.g., processor cores digital signal processings (DSPs), FPGAs/
application-specific integrated circuits (ASICs), and memories). Such SOCs
are one possible solution to sustain the ever increasing complexity of applications and are enabled by the constant improvements in manufacturing technologies. Chapter 2 by Zhonghai Lu, Ingo Sander, and Axel Jantsch, entitled
“Refining Synchronous Communication onto Network-on-Chip Best-Effort Services,” presents a novel approach to refine a system model specified with
perfectly synchronous communication onto an NoC best-effort communication
service. The approach starts from a formal synchronous model of the communication and ends with an NoC architecture providing best-effort communication service class. The use of perfectly synchronous models allows to cleanly
separate computation from communication and to better formalize and validate system specifications. The proposed refinement procedure then takes care
of deriving an efficient implementation of the communication onto the NoC architecture, for which the perfect synchrony assumption does not hold anymore.