Synthesis of checker EFSMs from timing diagram specifications

Efficient design verification is a major preoccupation in hardware systems design. We report on a method that assists the verification of the implementations of synchronous bus protocols (e.g., PCI). To this end we convert a timing diagram specification of the protocol in the form of hierarchical annotated action diagrams (HAAD) into synchronous state machines-checkers that can be used to observe the activity on the bus during simulation, emulation or formal verification and signal an error signal if a protocol violation is detected. The checkers are coded in synthesizable RT-level Verilog or VHDL. We illustrate the method on a subset of the PCI bus protocol