The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

It might be hard to find a current microcontroller which would fit thr bill. Modern pipeline design practices don't lead to such tight specifications regarding timing. Contention for functional units, out of order execution, power management, and especially cache, all contribute to variable execution timings for instructions. This would be especially true for small chips with integrated DSP capabilities.

On Sep 19, 2014 8:39 PM, "Abhishek Anand" <abhishek.anand.iitg AT gmail.com> wrote:

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/