Remove eqtype declaration for term type

Remove trailing whitespace in examples directory.

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

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

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.

Improve synthesis for conditionals.

Updated dest_word_type, is_word_type and var2size to accept wordsTheory

Changed is_CONSTANT and dest_CONSTANT in vsynth.sml to deal with CONSTANT F and CONSTANT T (booth multiplier example)

Fixed bug in printing of comments preceding existentially quantified
Dtypes in Verilog.

Changed name of Verilog module from DTYPE to dtype
(looks nicer) and fixed minor typos in generated comments.

Juliano's experiments show that Altera FPGAs initialise faster if Verilog is
generated with registers as instances of a separate module than if we generate
an inlined behavioral statement always @(posedge clk) q <= d driving
a register q initialised by reg q = 1.

Deleted code for generating separate modules for each component.

For visual sanity checking have added printing of HOL source as a
comment in the Verilog, e.g.:

/*
COMB
(\((sw :bool),(in1 :word32),(in2 :word32)). (if sw then in1 else in2))
((v15 :num -> bool) <> (v12 :num -> word32) <> (v0 :num -> word32),
(v3 :num -> word32))
*/
assign v3 = v15 ? v12 : v0;

/*
?(v :word32).
DTYPE v ((clk :num -> bool),(v9 :num -> word32),(v30 :num -> word32))
*/
always @(posedge clk) v30 <= v9;

Note: only have one Dtype register now, defined by:

|- !v ck d q. DTYPE v (ck,d,q) = (q 0 = v) /\ Dtype (ck,d,q)

Sometimes the initial state doesn't matter for the HOL proofs (as in
example above), but the generated Verilog initialises all registers to 1.

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.]

Replace

initial q = x;

by

reg q = x;

Commenting out some rewrites that were (apparently) generating:
CONSTANT (0w,1w,2w,3w)

(* COMB_CONSTANT_1,COMB_CONSTANT_2,COMB_CONSTANT_3, *)

This make break other things. Also various changes to enhance
COMB_SYNTH_CONV which I wrongly thought was the problem, but which
may also break synthesis.

Not sure what changed in compile.sml, but better diagnostics added to
vsynth.sml

unimportant changes

Added new compiler with whole program compaction optimisation

Have added an optimized version of MAKE_CIRCUIT, called
NEW_MAKE_CIRCUIT. It should be a drop-in replacement,
although the circuits it returns are not always alpha-convertible
with those of MAKE_CIRCUIT. Please try it out ... it's much
faster (6 secs vs 45 for final call to MAKE_CIRCUIT in
dev/FactScript.sml).

odules AND, OR, NOT and MUX are named devAND, devOR, devNOT and devMUX to avoid name clash with quartus compiler.

Optimizations to MAKE_NETLIST. It runs much faster on most examples
now. The optimizations should get moved to MAKE_CIRCUIT as well.

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

Bugfix in generated Verilog ("!!" should be "||").

The conversion from HOL to Verilog now annotates the HDL with the HOL
source (for eyeball checking, since formal checking is
impossible). This makes the factorial example too big for the vlogger
demo software, so switched to iverilog in Fact.ml.

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

Minor bugfix in vsynth.sml + improved and additional examples.

Small modification to vsynth.sml (added global termToVerilogLib so
that the set of functions to print Verilog can be dynamically
extended).

Added to end of README some documentation of the (currently extremely
tedious) stuff needed to add a new combinational component to the
synthesis engine. Hope to automate this kind of extension in the
future.

Added Fact32/Xor32.ml to illustrate adding 32-bit XOR.

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).

Types ``:num`` are converted to Verilog wires or registers of width
[31:0], which is not in general valid. When such a conversion occurs,
a warning like:

Warning: type of inp is ``:num``, but is compiled to [31:0].

is printed. These warnings can be suppressed by evaluating:

numWarning := false;

(the ML reference numWarning has a default of true).

Added support for VeriLogger (http://www.syncad.com/vlg_form.htm, I
have an old free version). Added comments to Fact.ml example showing
how to change simulator.

Added support for the Verilog simulator cver and waveform viewer
dinotrace. See README for instructions for installing them (extremely
easy). These are now the defaults, though it is easy to revert to
iverilog and/or gtkwave:

verilog_simulator := iverilog;
waveform_viewer := gtkwave;

(more details in README).

Also made a tweak to paper (not sure what).

Improved testbench code generated by SIMULATE.

Improved waveform picture in paper.
Fact.ml generates waveform shown.

Mainly a bugfix for a nested varstruct problem spotted by Konrad
whilst compiling AES.

Also, taking the opportunity to checkin Various other tweaks
(e.g. FlipFlopT/F renamed to DtypeT/F).

Verilog testbench tweak to ensure load driven T after done goes to T for
Factorial example. Will improve further shortly.

Fixed proof of liveness (REC_e_f_g) and updated figures

Minor updates to some comments and default simulation parameters.

Verilog bugfix from Juliano. Factorial example now works!

Made all registers power up storing 0, except FlipFlopT which powers
up storing 1. This seems to get rid of the x-value problem (but still
not clear if the correct results are being computed)
----------------------------------------------------------------------
----------------------------------------------------------------------

Fixed a bug in RecConvert causing looping. Added a check to hwDefine
to print an error message if a recursive definition doesn't have a
measure.

General tidy up, including replacing the odd and ad-hoc definition of
DEL by a more conventional one (and thereby eliminating the need for
REG and REGF). README file has been updated.

Some, but not all, of the "x" value simulation problems have now gone
away.

Added SIMULATE (see README) to run Icarus Verilog and then launch GTKWave
from HOL.

Added PRINT_NET_VERILOG and PRINT_NET_SIMULATE to generate
Verilog from unclocked netlists using DEL and DFF.

Corrected some typos and made FactScript.sml dump FACT.vl for testing.

Simplified the API for generating Verilog and updated README (old
stuff still exists in vsynth.sml). Added Verilog support for =,+,-,<
(need a uniform way of doing this as currently one has to edit
compile.sml, compileScript.sml and vsynth.sml).

Get printing to Verilog working again.

First verion of MAKE_VERILOG. See README. Only tested on one example so far.
Has known bugs and is probably very flakey.