Verification of AMBA Using a Combination of Model Checking and Theorem Proving
Hasan Amjad · Electronic Notes in Theoretical Computer Science · 2006
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.