This paper presents a unifying framework for the modeling of asynchronous
pipeline circuits.
A pipeline protocol is captured in a graph-based model which
defines the partial ordering of both its control and data events.
The relationship between an entire space of different protocols is
then captured in a semi-lattice,
which has well-defined top and bottom elements, corresponding to
the most concurrent and least concurrent protocol variants, respectively.
This framework also provides a set of correct-by-construction transformation
rules which allows for the systematic exploration of the
entire design space by their successive application.
To the best of our knowledge, this is the first formal framework
for asynchronous pipelines which can capture protocols from a variety of
logic style families, including both dynamic and static. It is also the first
to provide a formal foundation for the design-space exploration of asynchronous
pipelines.