The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

In case you are interested, there is also a formalization of the ARM v6 
or v7 instruction sets and its operational semantics in Coq available on 
http://gforge.inria.fr/projects/simsoc-cert/ but without timing information.

Best regards,

Frédéric.

Le 22/09/2014 16:41, Brian Campbell a écrit :
> 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