ECF processes and asynchronous circuit design

Abstract

Specifying hardware can present major challenges, especially when one is faced with a system that involves a large degree of concurrency. We propose a simple formal framework for representing concurrent systems. The framework is based on Enhanced Characteristic Functions (ECFs), which assign labels to sequences of communication actions. Labels represent properties of a process after a sequence of actions has been executed. A process in the framework is called an ECF process.

The general ECF model does not rely on a particular set of labels. Instead, the labels must satisfy a number of simple properties, which we use to define the operations on processes: refinement, hiding, and process product. The properties of labels, lifted to processes, lead to a number of desirable properties of these operations.

An instantiation of the general ECF model is obtained by choosing a particular set of labels. We study two instantiated ECF models, one addressing safety properties, and one addressing progress properties of processes. In each of the two models we give a correctness condition for a process and we show that the refinement relation has three equivalent characterizations. We also give alternative definitions of hiding for both the safety and the progress model. Finally, we show that ECF processes lend themselves well to a design technique based on the Factorization Theorem.

We define a specification composition, which combines behavioral constraints into one specification. Constraints are expressed by so-called snippets. We propose a part-wise design method that is applicable to specifications expressed in terms of snippets. This design method allows us to find in isolation implementations of the snippets. These partial implementations are then combined into an implementation of original specification. We illustrate the part-wise design method on a number of examples.