An embedded system is loosely defined as any system that utilizes
electronics but is not perceived or used as a general-purpose computer.
Traditionally, one or more electronic circuits or microprocessors are
literally embedded in the system, either taking up roles that used to be
performed by mechanical devices, or providing functionality that is not
otherwise possible.
The goal of this book is to investigate how formal methods can be
applied to the domain of embedded system design. The emphasis is on the
specification, representation, validation, and design exploration of
such systems from a high-level perspective. The authors review the
framework upon which the theories and experiments are based, and through
which the formal methods are linked to synthesis and simulation.
A formal verification methodology is formulated to verify general
properties of the designs and demonstrate that this methodology is
efficient in dealing with the problem of complexity and effective in
finding bugs. However, manual intervention in the form of abstraction
selection and separation of timing and functionality is required. It is
conjectured that, for specific properties, efficient algorithms exist
for completely automatic formal validations of systems.
Synchronous Equivalence: Formal Methods for Embedded Systems presents
a brand new formal approach to high-level equivalence analysis. It opens
design exploration avenues previously uncharted. It is a work that can
stand alone but at the same time is fully compatible with the synthesis
and simulation framework described in another book by Kluwer Academic
Publishers Hardware-Software Co-Design of Embedded Systems: The POLIS
Approach, by Balarin et al.
Synchronous Equivalence: Formal Methods for Embedded Systems will be
of interest to embedded system designers (automotive electronics,
consumer electronics, and telecommunications), micro-controller
designers, CAD developers and students, as well as IP providers,
architecture platform designers, operating system providers, and
designers of VLSI circuits and systems.
