Arm is investing in formal models of its architecture since 2016: first the concurrency model, which has now expanded from user level concurrency to cover features such as page tables and instruction fetch. More recently, Arm is developing a formal semantics of its Architecture Specification Language (ASL), which is used in the Arm Architecture Reference Manual (Arm ARM) to describe the semantics of each instruction in the Instruction Set. Equipped with those two formalisations, Arm is now looking to develop lightweight verification methods to check architectural properties.

To enable this goal, the Arm Architecture Formal Team would like to propose a tutorial on some aspects of those formalisations. The Arm Architecture Formal Team is responsible, amongst other things, for the maintenance of the formal memory model of the Arm architecture. The team is also responsible for the definition, and maintenance, of a formal semantics and reference interpreter for Arm’s Architecture Specification Language (ASL).