The Coq mailing list

[Dominic Mulligan <dominic.p.mulligan AT googlemail.com>]

You should still be able to obtain our developments from the project website: cerco.cs.unibo.it. They are all written in Matita though, not Coq. The paper "On the correctness of an optimising assembler..." by me and Claudio Sacrrdoti Coen is probably the most relevant piece of work describing the 8051 model and assembler we built and verified for it. 8051 is not RISC though and in many respects quite strange due to its age.

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.

Dom

On Saturday, 20 September 2014, David MENTRÉ <dmentre AT linux-france.org> wrote:

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