|
A Formal Methodology for Hardware/Software Co-design of Embedded Systems
Abstract:
Our methodology for control-dominated embedded reactive systems
is based on an implementation-independent
representation, Codesign Finite State
Machines (CFSMs). This representation allows us to
preserve semantical correctness throughout the design process,
because CFSMs assume unbounded, non-zero reaction delays, that
correspond both to hardware and software behavior.
CFSMs can be generated from a variety of specification languages, such as
Esterel, StateCharts, VHDL, Verilog.
Partitioning is user-driven, while our codesign
environment performs automatically all other
synthesis tasks.
We derive hardware directly from CFSMs, assuming single-cycle reaction
delays (but pipelining is also allowed by the model semantics).
We synthesize software using an intermediate representation,
Software Graphs, that allows better optimization and
tighter control over implementation costs than general-purpose compilers.
We are also planning to synthesize automatically
a real-time scheduler and I/O port drivers,
depending on the chosen micro-controller.
We perform system validation by mixing formal verification (made possible by
our finite-state model) with simulation (to identify and rule out
special cases).
UCB Design Technology Warehouse Homepage
|
