Formalization and verification of the AMBA AHB communication architecture using the ACL2 theorem prover

International audienceWe apply a method, based on an automatic theorem prover, to verify the correctness of communication systems at the first step of the design. The prover has reasoning capabilities that do not require fixed size systems, and large parameterized architectures, like IPs or SoCs can be modeled and proved correct through this approach. We illustrate the approach on an industrial onchip bus, the AMBA AHB