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

The Advanced Microcontroller Bus Architecture (AMBA) is an open System-onChip 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. Key words: System-on-Chip, theorem proving, model checking, tool combination.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Hasan Amjad
• Keywords: Advanced Microcontroller Bus Architecture, ENTCS 2006, System-onChip Bus Protocol, Theorem Proving