The Coq mailing list

[Brian Campbell <Brian.Campbell AT ed.ac.uk>]

On 20/09/14 10:40, Dominic Mulligan wrote:
> Brian Campbell is also doing something similar for the ARM M0 micro
> controller as part of the REMS project, but if I understand correctly
> his model is written in HOL4 and not yet complete. If you really need a
> RISC processor then perhaps that is better.

Yes, I'm using a model of ARM's Cortex-M0 core from Anthony Fox, which 
is in HOL4 and covers the user instructions.  The cores have a rather 
nice, simple timing model, but it does depend somewhat on decisions 
taken by the manufacturer and whether you run code from flash memory or 
SRAM.  Adding plain memory-mapped I/O would probably be easy, but the 
interrupt behaviour looks more subtle.  I recently presented a paper 
about validating the model's predictions against some hardware at FMICS, 
and could provide more details if anyone is interested.

  Brian


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.