Sat Mar 13 09:04:52 CET 2010
Composing partial state maps
I need to get this going.. Let's look at the assembler typing/sim
stuff, either in staged Scheme or in Haskell.
First point is the datasheet. Let's use the 12F675 since the
instruction set is simpler than the 18F series.
What are the high-level problems?
* Functional dependencies. This is easy:
input constraint: 0 <= k <= 255
function: (W) <- (W) + k
status function: C, DC, Z
This needs a low-level logic language to express the
semantics. I.e. at the bottom this should be logic gates, but
certain compositions should be acellerated by "simulator
The status functions need to be made explicit, so the function
k -> W -> (W,C,DC,Z)
* Composition / dependency analysis.
The interesting problem is how to take descriptions that map
partial state to partial state, and lift them to complete state
maps so they can be composed and then possibly re-embedded in a
minimal representation for dependency or "clobber" analysis.
What are the low-level problems?
1. The basic level is logic gates: the bottom line of semantics should
be as simple as possible.
2. Solve composition of logic gates by dependency analysis.
3. Solve the mapping (simulation) problem, i.e. implement certain
networks by operations present in an implemented target, which
could be a high level language, a real machine, an FPGA circuit
(build accelerated compiler verifiers on FPGA!), ...
What is the essential idea?
I'm dealing with information on at least 2 levels: network
connectivity (meta-lang) and network function (object-lang).
I.e. staging is essential: There are going to be computations on the
meta-lang (figuring out dependencies, lifting dependencies to
How this is implemented doesn't really matter much (Scheme, Haskell,
* Scheme: highest flexibility (hackability due to more operational
nature: just do it) and very simple staging (macros & modules).
* MetaOCaml: typed staging, might be useful for figuring out static
structure of the program itself better.
* Haskell: very flexible type system, but type-level computations
are somewhat complex.
Functions and resources.
1. FUNCTIONS: object language: functional dependencies
(AND,OR,NOT,compositions) between nodes.
2. RESOURCES: meta language / type system: _physical_
instantiations of functional networks connecting shared nodes.
Tagless interpreters and embedding of staging in non-staged
languages are going to be essential components to provide insights.
Hardware languages are about instantiation of macros. Is it possible
to use the ideas behind Ziggurat to provide higher level semantics
of compositions? I.e. it's simple to pool together a huge number of
gates into an abstraction, and simulate it by simulating the instance
directly. What is interesting though is to abstract it n the
meta-level (semantics!) not just the human-modular level.
What I mean is: composition of modules in hardware description
languages is about abstraction for the engineer: the engineer has a
(fuzzy) model about how something works and can use this to "proove"
correctness of compositions. Can this be made more formal? Can we
use the specification (simplification) as a type of a hardware module?
I.e. how to relate low-level properties/semantics to high-level.
The real problem seems to be management of state (resource). I.e. an
I2C interface isn't a function, it's a state machine.
Anyways.. There's something to learn here.