Updating h/w synthesis stuff so that it works again.

Updated Juliano's hardware compilation to work with wordsTheory. There are
now some nasty parser warnings with "===>", "<>" and possibly others.

The dev/booth example was/is broken (I haven't attempted to repair it).

Have updated dev/AES/word8 and Crypto/AES. Perhaps dev/AES should be removed?

The hardware compilation for Crypto/TEA and Crypto/RC6 are now broken.
Updating the Crypto examples should be straightforward. Once done I can
delete src/n_bit.

Added propositional logic (pedagogical example)
and updated the README. Some other files
seem to have been changed as well.

Initial (probably buggy) release of a new Verilog back end. This
generates "behavioral" rather than "structural" Verilog (i.e. the body
of a generated module consists of continuous assignments and always
statements rather than module instances). I haven't deleted the code
for generating separate module definitions and instances for
components (this is now obsolete and I'll delete it once the new
approach has been validated). There is now a single way of linking
combinational HOL code to Verilog:


(*****************************************************************************)
(* Library associating HOL terms with ML functions for generating *)
(* combinational Verilog. Typical example: *)
(* *)
(* add_vsynth *)
(* [(``\(in1,in2). in1 >> in2``, *)
(* (fn[i1,i2] => ("{{31{" ^ i1 ^ "[31]}}," ^ i1 ^ "} >> " ^i2))), *)
(* (``UNCURRY $>>``, *)
(* (fn[i1,i2] => ("{{31{" ^ i1 ^ "[31]}}," ^ i1 ^ "} >> " ^i2)))] *)
(* *)
(* which will cause both *)
(* *)
(* ``COMB (\(in1,in2). in1 >> in2) (x<>y, z)`` *)
(* *)
(* and *)
(* *)
(* ``COMB (UNCURRY $>>) (x<>y, z)`` *)
(* *)
(* to generate the Verilog statement *)
(* *)
(* assign z = {{31{x[31]}},x} >> y; *)
(*****************************************************************************)

AddBinop can now be defined by:

fun AddBinop (_:string, (hbinop,vbinop)) =
add_vsynth[(hbinop, fn[i1,i2] => (i1 ^ " " ^ vbinop ^ " " ^ i2))];

[Note that a module name isn't needed anymore.]

Added cirDefine to generate circuits in one step. Tweaked examples.
Updated README.

Added REFINE_ALL that uses previous results of hwDefine that are now
stored in a reference hwDefineLib. See Fact.ml for an example.

Various other tweaks and improvements (e.g. refinement combinators
simplified and extended).

Proved

|- !n. FACT n < 2 ** WL ==> (FACT n = w2n(Fact32(n2w n)))

and similar results for Mult, MultIter in Fact32Script.sml.

README updated.

Various recentish changes. Fact/Fact32 examples will be developed
further, but future versions of paper.tex will probably be made in
another CVS repository hosted at Cambridge. Will keep
http://www.cl.cam.ac.uk/~mjcg/proposals/dev/ updated.

Lots of changes aimed at partially automating the adding of new HOL
and Verilog unary and binary operators to synthesis. Read about
AddUnop, AddBinop in README and see how they are used in Fact.ml and
Fact32/Fact32.ml

32-bit factorial example now works thanks to Konrad's
improved hwDefine.

Upgraded hwDefine to handle decrement-based iterations on words. Now
the factorials on word32 work.

Various tweaks. Added a preliminary very version of the factorial
example that works with values of type ``:word32`` rather than with
``:num``. Needed some messy support for n-bit numerals (``0w``,
``1w``, ``2w``, ... etc).