Verification and Implementation of Delay-Insensitive Processes in Restrictive Environments

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 p...

• Type: Conference
• Year: 2004
• Where: ACSD
• Authors: Hemangee K. Kapoor, Mark B. Josephs, Dennis P. Furey
• Keywords: ACSD 2004, Delay-insensitive Module, Divergence Extension, Hardware, Unbounded Delay