Affiliations: Dhirubhai Ambani Institute of Information and
Communication Technology, Gandhinagar, India. E-mail:
[email protected] | Centre for Concurrent Systems and VLSI, London South
Bank University, UK. E-mail: josephmb,[email protected]
Abstract: A delay-insensitive module communicates with its environment through
wires of unbounded delay. To avoid transmission interference, the absorption
of a signal transition must be acknowledged before another one is propagated
along the same wire. The environment may guarantee, however, to interact with
the module in an even more restrictive way. It is worthwhile taking this into
account when synthesising the module because it may allow for a cheaper, faster
implementation. The concept of restriction has been built into our translation
tool, di2pn (to help in synthesis), and our analysis tool, diana (to perform
equivalence and refinement checking). Formally, DI-Algebra is equipped with a new operator that weakens
the specification of a module by taking its environment into account. This
operator is a useful instance of divergence extension, a concept introduced by
Mallon. Divergence extension in general, and restriction and alternation in
particular, can be represented with the parallel composition operator and so
are amenable to algebraic reasoning.
