The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi,

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?

It would be great if formalization includes the instructions for interacting

with ADCs and digital IO pins.

If not, does someone have suggestions about a cheap

microcontroller that has a simple instruction set

with a simple and well documented timing behaviour?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/