SmartDV’s Avalon assertion IP provides an efficient way to verify the Avalon Interface using formal verification. The model supports key features of the Avalon Interface, including burst transfers and pipelined transfers. Additionally, the IP can be used in assertion-based verificaton in simulation.