Protocol transducer which converts from one protocol to another is one of the key components in IP-based design methodology. Although there have been researches on automatic synthesis of such protocol transducers, they cannot efficiently deal with out-of-order type communications
frequently found in the state-of-the-art protocols. In this paper we present an automatic synthesis method which can deal with complicated state-of-the-art protocols by clearly separating control and datapath parts of the synthesized protocol transducers and introducing four types of configurations in the datapath parts of the protocol transducers. We also present a formal verification method based on inclusion checking between the given protocol transducer to be verified and the all possible protocol transducers which can be generated through our synthesis method. Experimental results show their practical usefulness even for protocol transducers with complicated state-of-the-art protocols.