The Coq mailing list

[David MENTRÉ <dmentre AT linux-france.org>]

Hello,

2014-09-20 05:38, Abhishek Anand:
> Is there a formalization of the operational semantics
> of a microcontroller (preferably RISC)
> such that the formalization includes timing behaviour,
> such as how long (e.g. clock cycles)  programs take to run?

You should have a look at publications and results of project CerCo:

  http://www.pps.univ-paris-diderot.fr/cerco

Especially that paper: http://hal.inria.fr/hal-00702665/en

> It would be great if formalization includes the instructions for interacting
> with ADCs and digital IO pins.

I don't think that have gone so far.

> If not, does someone have suggestions about a cheap
> microcontroller that has a simple instruction set
> with a simple and well documented timing behaviour?

They modeled 8051 processor.

The developments seem to be no longer accessible but the authors would 
probably send it to you.

Best regards,
david