Output details

A refinement approach to design and verification of on-chip communication protocols

<04>

This paper describes a mathematically rigorous technique for the development of assured-correct on-chip communications protocols based on stepwise refinements that incrementally introduce new features. On-chip communications protocols are notoriously difficult to validate post-design. This work demonstrates the feasibility of a more tractable refinement-based approach, illustrating the framework by showing how two very general aspects of the industrial AMBA protocol can be derived formally. All the technical results presented here have been defined and proved strictly formally using the Isabelle/HOL theorem prover – the gold standard of mathematical rigour in a mathematical development of this kind.