Trustworthy specifications of ARM v8-A and v8-M system level architecture

Alastair D. Reid
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016)
Mountain View, CA, USA
Pages 161-168
October 2016
Note(s): Arm architecture, ISA specification, instruction set architecture, dependent type, type inference, ASL, formal specification
Papers: reid:cav:2016, reid:oopsla:2017

Arm Architecture Specification Language (ASL)

  • The fallacy of spec-based design [bhatt:sefm:2003]
  • 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]
  • 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]