Adrian Isles, Principal Architect, Averant
Jeremy Sonander, Application Engineer, Saros Technology UK
Mike Turpin, Principal Verification Engineer, ARM UK

We show how designs that implement the AMBA protocol specification can be verified automatically using Static Functional Verification (SFV) technology. SFV is an approach for verifying the correctness of RTL designs by using formal analysis to prove that a property holds for a design under all inputs, sequences of inputs and states. This provides a level of confidence in the correctness of a design that is unachievable with simulation. We show how different AMBA protocol rules can be described using the Property Specification Language (PSL). A methodology is also provided that allows these rules to be reused across various designs that implement the AMBA protocol specification.