Verification and implementation of delay-insensitive processes in restrictive environments

A delay-insensitive module communicates with its environment through wires of unbounded delay. The environment may only need to interact with the module in a restricted way. it is worthwhile taking this into account when synthesising the module because it may allow for a cheaper, faster implementation. Formally, we introduce an operator to DI-algebra which weakens the specification of a module by taking its environment into account. Moreover, 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).