Verification of AMBA Using a Combination of Model Checking and Theorem Proving

The Advanced Microcontroller Bus Architecture (AMBA) is an open System-on-Chip bus protocol for high-performance buses on low-power devices. We demonstrate the combined use of model checking and theorem proving to verify both control and datapath properties in a seamless manner.