Synthesis and formal verification of on-chip protocol transducers through decomposed specification

Protocol transducer which realizes translations between multiple protocols 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. By using simulation-based filtering methods followed by a complete analysis of the entire design and state space, large and complicated protocol transducers can be efficiently and formally verified. Experimental results show their practical usefulness even for protocol transducers for complicated state-of-the-art protocols.