Protocol modeling and recasting for handshaking circuits

This thesis is concerned with asynchronous circuit design and verification. Specifically, we will focus on new methods of modeling the control of data transmission between submodules in asynchronous systems.;This thesis introduces the formal definitions of semi-hiding and converse semi-hiding operators, along with a study of the algebraic properties of these operators. First-cut algorithms for semihiding and converse semi-hiding operations have been implemented in FIREMAPS. Using these operators, specifications of circuit modules could be analyzed in the active-edge domain with less complexity and mapped to transition-level specifications if necessary.;Our methods of modeling will be applied to asynchronous circuit synthesis; the methods will also be applied to interface recasting, by which we mean transforming the communication protocol of a module interface while preserving its functional behavior. Therefore, a circuit that uses one protocol for communication at its interface can be recast to another circuit that uses a different protocol at its interface while preserving the functional behavior of the original circuit. Furthermore, our methods would permit a single module to use several different protocols at its interfaces. By applying our methods, an additional degree of flexibility will be offered to designers in asynchronous data transmission design: namely, the choice of protocols for synchronizing circuit components without affecting the functional behavior of such components.