Arm Architecture Specification Language (ASL)

[Google Scholar]

Notes: Arm architecture, ISA specification, Dependent type, Liquid type
Papers: reid:cav:2016, reid:fmcad:2016, reid:oopsla:2017, reid:phd:2019

ASL is the ISA specification language used by Arm to specify their A-, R- and M-profile processor architectures (reid:fmcad:2016). Those specifications have been extensively tested, formally validated (reid:oopsla:2017) and have been used to formally validate Arm’s processor implementations (reid:cav:2016).

ASL is an executable, strongly-typed, imperative language with support for dependent types and for throwing and catching exceptions. For the first 20–25 years of Arm’s history, specifications were created after the corresponding implementation as documentation of what had been built. […] specifications are now written and tested before implementation starts.

The ASL language was created by reverse engineering a specification language from the pseudocode notation used in Arm’s existing documentation, fixing the pseudocode in the documentation and evolving that pseudocode into a formal specification.
— Alastair Reid (reid:phd:2019)

Arm architecture, Dependent type, ISA specification, Sail ISA specification language

  • ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
  • Examiner: Automatically locating inconsistent instructions between real devices and CPU emulators for Arm [jiang:arxiv:2021]
  • End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
  • Trustworthy specifications of ARM v8-A and v8-M system level architecture [reid:fmcad:2016]
  • Who guards the guards? Formal validation of the ARM v8-M architecture specification [reid:oopsla:2017]
  • Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
  • Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]