Sat Mar 13 15:27:04 CET 2010
Logic simulation and SSA form
The problem I want to solve is to verify optimization rules of the
PIC18 compiler. I.e. to prove (or lesser: test) the correctness of a
transformation on object code.
I'd like to use a functional (dataflow network) model because it makes
manipulation of the object under test simpler, reducing the complexity
of the verification code.
So an essential part is the translation of imperative to functional
The plan I have is to translate each PIC18 instruction into a MIMO
logic function operating on bit vectors. To keep things simple I'd
like to model instructions as functions between particular states of
the machine. I.e. the "ADDLW k" instruction is
(k0,...,k7) -> (W0,...,W7) -> (W0,...,W7,C,Z,DC)
However, when composing these functions into a network, intermediate
nodes need to be named. I.e. the input W0 is not the same as the
This boils down to conversion of the imperative form to SSA form by
associating bit register names to different node names.
* I started working on a functional representation of networks using
type classes, and a Nand representation. Conclusion: what is
useful is a tagless representation as a typeclass Logic and
operations defined on it. This can then be given multiple
representations later by instantiating the classes. At this
moment an explicit representation (i.e. the NAND networks) is not
* A representation of dataflow networks is useful to _visualise_ the
network. I.e. the ai/Shared.hs module can be used.
* Problem to solve: construct SSA form from imperative program.
Every assignment creates a new variable. Problem: how to
represent and create variables?
It seems that this kind of behaviour is easy to do with Scheme
macros, using shadowing as in:
(let-values (((x y z) (op1 ...)))
(let-values (((x y z) (op2 ...))) ... ))
This then leads to a binding structure for the composite operation
that can be queried as a function, i.e. using abstract
How to do something like this in Haskell?