End-to-end verification of ARM processors with ISA-formal

Alastair D. Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Erin Shepherd, Peter Vrabel, Ali Zaidi
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]

Proceedings of the 2016 International Conference on Computer Aided Verification (CAV'16)
Lecture Notes in Computer Science, volume 9780
Toronto, Canada
Springer Verlag
Pages 42-58
July 2016
Note(s): Arm architecture, ISA specification, instruction set architecture, bounded model checking, dependent type, ASL, CPU verification
Papers: reid:fmcad:2016, reid:oopsla:2017

Arm Architecture Specification Language (ASL)

  • Formal verification of pipelined Y86-64 microprocessors with UCLID5 [bryant:cmu:2018]
  • End-to-end formal verification of a RISC-V processor extended with capability pointers [gao:fmcad:2021]
  • 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]