SmartDV’s AMBA AXI5 assertion IP is a verification component for formal property verification (FPV). It provides an efficient way to verify an ARM AMBA AXI5 master, slave, or interconnect interface block using any method of formal verification in any major formal verification engine. Additionally, it can be used for assertion-based verification in simulation.