Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication Protocols

In general on-chip communication protocols, such as OCP[1], can be specified and represented with finite state machines (FSM). Such communication protocols are basically collections of individual transactions or commands, such as simple read/write and bust read/write, and each transaction or command can be specified with a FSM. So a given communication protocol can be represented with a set of FSMs which work jointly. Based on these FSM-based specifications, we have been developing not only pure formal and semi-formal verification techniques using FSMs as specifications, but also synthesis and debugging techniques, such as automatic generation of protocol converters and post-silicon verification/debugging supports. In this paper, we show first how FSM-based specifications can describe sate-of-the-art on-chip communication protocols, and then their application to such synthesis and verification/debug for SoC designs are presented.