History log of /seL4-l4v-master/HOL4/examples/ARM/experimental/lpc_devicesScript.sml
Revision Date Author Comments
# 845531b5 14-Sep-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove trailing whitespace in source files.


# 198feb8b 24-Aug-2010 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Removed some junk.


# 4c082b28 24-Aug-2010 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

This example shows how models of memory mapped I/O devices can be
connected to the current version of Anthony's ARM model. The idea is
to take the ARM next-state function and build a wrapper around it. The
wrapper essentially models the effect of the environment, i.e. the I/O
devices, as a relational operational semantics.

This example is based on polling, but interrupt-driven I/O devices
should also fit into the same wrapper-based approach.