If two (or more) interfaces obey protocols each defined by an automaton
and if we have some over-arching design goal (e.g.\ data conservation)
then we can take the cross-product of the constituent automata and trim it to form our design.
Required trims:
See Convertibility verification and converter synthesis: two faces of the same coin. Passerone et al
May wish to consider various point-to-point data path patterns:
Can consider data patterns for more than two ports:
Greaves current research is to do apply this at the TLM level and between levels (with MJ Nam).
Certain design patterns require extra state to be 'thrown in', giving problems like the over large fictional FPGA problem for the SAT synthesis idea.