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
output W0.

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?