Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Remove eqtype declaration for term type

Remove trailing whitespace in examples directory.

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

Changed hol-mode.src and src/parse/PPBackEnd.sml so that type variables are displayed in purple.

"Everybody's cute... Everybody's cute, even me. But in purple, I'm STUNNING!"
(Centauri Ambassador Londo Molari, Babylon 5, The Parliament of Dreams)

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!

Get dev stuff working again.

Avoid parsing incompatibilities with wordsTheory.

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.

Small change to hwDefine2: the function addTerminationTheorems allows the user to add new theorems to prove termination

Changed hwDefine to work with wordsTheory

Update NEW_MAKE_CIRCUIT with Mike Gordon's improvement of the synthesis for conditionals. Changes are indicated by (* new *)

Improve synthesis for conditionals.

Changed inlineCompile to accept Let-exps.
Also updating Mike's change to COMB_SYNTH_CONV to deal
with more cases involving tuples.

Improved hwDefine to solve more termination problems ... don't
always have to give a measure, for example.

Catching up MAKE_NETLIST to recent changes.

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

Spotted another optimization (getting rid of unnecessary applications
of higher-order rewriting, as usual).

Also added newcirDefine, which should behave as cirDefine, except
faster.

Made STEP5 of MAKE_NETLIST (and NEW_MAKE_CIRCUIT) much faster. Seems
basically constant time now, rather than being the bottleneck it
was before.

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

*** empty log message ***

Preliminary attempt to handle combinational lets.
Example:

> val H_def = |- H x = x + 1 : thm
- add_combinational["H"];
> val J_def = |- J x = (let y = H x in y + y + y) : thm
- MAKE_CIRCUIT(EXPAND_COMPONENTS(REFINE_ALL J_dev));
> val it =
|- InfRise clk ==>
(?v0 v1 v2 v3 v4 v5 v6.
DtypeT (clk,load,v3) /\ NOT (v3,v2) /\ AND (v2,load,v1) /\
NOT (v1,done) /\ CONSTANT 1 v5 /\
COMB (UNCURRY $+) (inp <> v5,v4) /\
COMB (UNCURRY $+) (v4 <> v4,v6) /\
COMB (UNCURRY $+) (v6 <> v4,v0) /\ Dtype (clk,v0,out)) ==>
DEV J (load at clk,inp at clk,done at clk,out at clk) : thm

Support for lets, by having a Let combinator. The intent is to use
Let as a way of avoiding the translation to Seq and Par, which
doesn't keep the sharing of the let. The Let expression eventually
is replaced by an ordinary "let" which, thanks to Mike, is dealt
with in COMB_SYNTH_CONV.

Improving COMB_SYNTH_CONV treatment of ``let (v1,v2) = ... in ...``.
Example:

> val tm =
``COMB
(\(x1,x2,x3,x4).
(let (y1,(y2,y3),y4) = (x1 + x2,(x3,x2),x3 + x4) in
let (z1,z2) = (y1 + y2,y3 + y4) in
z1 - z2 + (z2 - z1))) (in1 <> in2 <> in3 <> in4,out)`` : term

- (TOP_DEPTH_CONV COMB_SYNTH_CONV THENC EXISTS_OUT_CONV) tm;
> val it =
|- COMB
(\(x1,x2,x3,x4).
(let (y1,(y2,y3),y4) = (x1 + x2,(x3,x2),x3 + x4) in
let (z1,z2) = (y1 + y2,y3 + y4) in
z1 - z2 + (z2 - z1))) (in1 <> in2 <> in3 <> in4,out) =
?v0 v1 v2 v3 v4 v5.
COMB (UNCURRY $+) (in1 <> in2,v1) /\
COMB (UNCURRY $+) (in3 <> in4,v0) /\
COMB (UNCURRY $+) (v1 <> in3,v3) /\
COMB (UNCURRY $+) (in2 <> v0,v2) /\
COMB (UNCURRY $-) (v3 <> v2,v5) /\
COMB (UNCURRY $-) (v2 <> v3,v4) /\
COMB (UNCURRY $+) (v5 <> v4,out) : thm

Changing a dest_abs to dest_pabs makes paired lets work:

- (REDEPTH_CONV(COMB_SYNTH_CONV) THENC EXISTS_OUT_CONV)
``COMB(\(x1,x2,x3).
(let (y1,(y2,y3),y4) = (x1+x2,(x1+1,x2-1),x3) in y1+y1+y2+y4+y3))
(in1 <> in2 <> in3,out)``;
<<HOL message: inventing new type variable names: 'a>>
> val it =
|- COMB
(\(x1,x2,x3).
(let (y1,(y2,y3),y4) = (x1 + x2,(x1 + 1,x2 - 1),x3) in
y1 + y1 + y2 + y4 + y3)) (in1 <> in2 <> in3,out) =
?v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15.
COMB (UNCURRY $+) (in1 <> in2,v2) /\ CONSTANT 1 v6 /\
COMB (UNCURRY $+) (in1 <> v6,v5) /\ CONSTANT 1 v7 /\
COMB (UNCURRY $-) (in2 <> v7,v4) /\
COMB (UNCURRY $,) (v5 <> v4,v3) /\
COMB (UNCURRY $,) (v3 <> in3,v1) /\
COMB (UNCURRY $,) (v2 <> v1,v0) /\
COMB (\((x1,x2,x3),y1,(y2,y3),y4). y1)
((in1 <> in2 <> in3) <> v0,v15) /\
COMB (\((x1,x2,x3),y1,(y2,y3),y4). y1)
((in1 <> in2 <> in3) <> v0,v14) /\
COMB (UNCURRY $+) (v15 <> v14,v13) /\
COMB (\((x1,x2,x3),y1,(y2,y3),y4). y2)
((in1 <> in2 <> in3) <> v0,v12) /\
COMB (UNCURRY $+) (v13 <> v12,v11) /\
COMB (\((x1,x2,x3),y1,(y2,y3),y4). y4)
((in1 <> in2 <> in3) <> v0,v10) /\
COMB (UNCURRY $+) (v11 <> v10,v9) /\
COMB (\((x1,x2,x3),y1,(y2,y3),y4). y3)
((in1 <> in2 <> in3) <> v0,v8) /\
COMB (UNCURRY $+) (v9 <> v8,out) : thm
-
May need to do something to eliminate the `rewiring' COMBs.

Added a case to COMB_SYNTH_CONV to handle let-terms
(experimental extension intended to be useful for Konrad).
For example:

- COMB_SYNTH_CONV
``COMB(\(x1,x2,x3). let y = x1 + x2 in y - x3) (in1 <> in2 <> in3, out)``;
> val it =
|- COMB (\(x1,x2,x3). (let y = x1 + x2 in y - x3))
(in1 <> in2 <> in3,out) =
?%%genvar%%805.
COMB (\(x1,x2,x3). x1 + x2) (in1 <> in2 <> in3,%%genvar%%805) /\
COMB (\((x1,x2,x3),y). y - x3)
((in1 <> in2 <> in3) <> %%genvar%%805,out) : thm

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

Added a new "sw" directory for the software compiler being
written by Li, Owens, and Slind. This is a temporary hiding
place for work-in-progress.

Optimization of standardization apart of variables, done in
first phase of MOVE_EXISTS_OUT_CONV. My previous solution,
using subst, was dumb. By building up a substitution continuation
on the way down from the root of the term, and applying it at all
variables, things are much faster. There may be lessons for the
implementation of Term.subst here ...

Optimized renaming done in STANDARDIZE_EXISTS_CONV. Still too
slow ... good test of subst.

Yet another insignificant tweak.

Duh. Changed ifprint to if_print.

Fixed subtle bug in COMB_SYNTH_CONV where

COMB (\(x,x).t) (inp,out)

not being dealt with properly in processing results of
BUS_MATCH. Also added a bit of debug support.

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

Better error message when trying to hwDefine a non-function.
Need to think about hwDefine `c = (T,F,F,T)`, which Konrad needs.

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.

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

Changed the proof in RecCompileConvert to a (hopefully) more general one able that accepts the interface of APPLY_NEXTd (Booth multiplier example).

Extended hwDefine to automatically handle decrement-based iterations
on words. Also the reference variable "termination_simps" can be
updated to add in new theorems that help establish termination.

Note that we can't handle the problem once-and-forall, since each
different word length needs a new theorem (wordnTheory.WORD_PRED_THM).

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

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

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.

First hack at fixing problem in hwDefine.

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

Have changed the way inputs and outputs are split by MAKE_NETLIST and
MAKE_CIRCUIT. This is partly to improve the circuits (fewer variables)
and partly to make the representation in HOL closer to Verilog. A
benificial side-effect is that the code is simpler (and probably more
efficient - ABS_IN_OUT_SPLIT_CONV has gone, for example). See README
for updated descriptions. Note that synthesis to Verilog (vsynth.sml)
is broken -- but I'm revising that so that separate modules are
generated for the design and the stimulus (i.e. environment). Will fix
soon(ish).

Minor tweak to stuff in comments. No code changes.

Tidying up.

Some tweaks, and rollback to (hopefully) working version of MAKE_CIRCUIT.

Reverting to old and inefficent version of COMB_SYNTH_CONV. I ran
regression test on new code, but didn't check results fully (I wonder
how common this is in the real world). Was failing to split inputs in:

val MULTd_net = time MAKE_NETLIST MULTd_dev;

from booth/boothDevScript.sml.

Code improvements from KXS. Not sure what are the other things
"cvs ci" is picking up!

Refine away "at clk" temporal abstractions on ``inp`` and ``out``
in circuits made with MAKE_CIRCUIT.

Split inputs and outputs. Now get the following from Konrad's example:

val to_state_net =
|- (\(load,inp,done,out).
?v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18
v19 v20 v21 v22 v23 v24 v25 v26 v27 v28 v29 v30 v31 v32 v33
v34.
(inp =
v15 <> v14 <> v13 <> v12 <> v11 <> v10 <> v9 <> v8 <> v7 <>
v6 <> v5 <> v4 <> v3 <> v2 <> v1 <> v0) /\
(out =
v31 <> v30 <> v29 <> v28 <> v27 <> v26 <> v25 <> v24 <> v23 <>
v22 <> v21 <> v20 <> v19 <> v18 <> v17 <> v16) /\
DEL (load,v34) /\ NOT (v34,v33) /\ AND (v33,load,v32) /\
NOT (v32,done) /\ DEL (v15,v31) /\ DEL (v11,v30) /\
DEL (v7,v29) /\ DEL (v3,v28) /\ DEL (v14,v27) /\
DEL (v10,v26) /\ DEL (v6,v25) /\ DEL (v2,v24) /\
DEL (v13,v23) /\ DEL (v9,v22) /\ DEL (v5,v21) /\ DEL (v1,v20) /\
DEL (v12,v19) /\ DEL (v8,v18) /\ DEL (v4,v17) /\
DEL (v0,v16)) ===> DEV to_state : thm

Also made MK_CIRCUIT split inputs and outputs. Seems to work. Probably
needs tuning.

Currently failing attempt to split up input and output busses.
See: BUS_SPLIT and ABS_IN_OUT_SPLIT_CONV. Will slog on in the morning,
but totally burned out now. Need to get unwinding working.

Another tweak and removed some annoying warning messages. I hope the Utah
examples are compiling better now. I'm still tuning though ...

Another tweak (use COMB_ID more aggressively).

Experimental tweak to compiler to better handle Konrad's examples like:

to_state
(b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15) =
(b0,b4,b8,b12,b1,b5,b9,b13,b2,b6,b10,b14,b3,b7,b11,b15)

Not fully tested (but have to dash to Wadler's talk).

Existentially quantify local wires in circuits using

(*****************************************************************************)
(* |- P ==> Q *)
(* ---------------- (x not free in Q) *)
(* |- (?x. P) ==> Q *)
(*****************************************************************************)
fun ANTE_EXISTS_INTRO v th =
(let val (t1,t2) = dest_imp(concl th)
val exists_tm = mk_exists(v,t1)
val th1 = ASSUME exists_tm
val th2 = UNDISCH th
val th3 = CHOOSE (v,th1) th2
in
DISCH exists_tm th3
end)
handle HOL_ERR _ => th;

For some reason rewriting with LEFT_FORALL_IMP_THM didn't work.

Made COMB_SYNTH_CONV compile conditionals using MUX. A few other
tweaks and renamings.

Removing tex (renamed to doc). Tweak to compiler.

Tweaks to compiler. Also added ML function "add_combinational" to declare
functions as combinational for synthesis (see README for details).

Added MAKE_CIRCUIT that generates circuits build out of clocked dtype
registers. Details in the the updated README.

Minor tweaks to MAKE_NETLIST and COMB_SYNTH_CONV. Also a few theorems
for later use in temporal refinement.

Add "0" to combinational_constants. Further improves circuit for FACT.

Implemented DEL in terms of simpler primitives (DEL_def replaced by DEL_THM).

I may reimplement COMB_SYNTH_CONV to be less clunky (it currently uses
unwindLib and tactics to validate synthesis on-the-fly). Until I get
around to this, I've added some diagnostic printing if a proof failure
happens.

Added a crude tool COMB_SYNTH_CONV to synthesise functions
representing combinational circuits to netlists. Probably not robust,
but works on FactScript.sml. Added REDEPTH_CONV COMB_SYNTH_CONV
to MAKE_NETLIST.

Tidy up. Upated README. Added more optimisations
(see description of PRECEDE and FOLLOW in README).

Improvements to synthesis (both to speed and generated netlists). Aiming
to get to a form that can be pretty printed to Verilog.

Minor cleanup and improvement of netlist synthesis.

Improved synthesis of comninational circuits:

- val (RightShift,_,RightShift_dev) =
hwDefine
`RightShift (b1,b2,b3,b4,b5,b6,b7,b8) = (F,b1,b2,b3,b4,b5,b6,b7)`;
<<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd, 'e, 'f, 'g, 'h>>
Definition has been stored under "RightShift_def".
> val RightShift =
|- !b1 b2 b3 b4 b5 b6 b7 b8.
RightShift (b1,b2,b3,b4,b5,b6,b7,b8) = (F,b1,b2,b3,b4,b5,b6,b7) : thm
val RightShift_dev =
|- DEV
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). F)
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). b1)
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). b2)
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). b3)
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). b4)
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). b5)
(Par (\(b1,b2,b3,b4,b5,b6,b7,b8). b6)
(\(b1,b2,b3,b4,b5,b6,b7,b8). b7)))))))) ===>
DEV RightShift : thm
- val RightShift_cir = MAKE_NETLIST (REFINE (DEPTHR ATM_REFINE) RightShift_dev);
> val RightShift_cir =
|- (\(load,inp,done,out).
?v0 v1 v2 v3.
DEL (load,v3) /\ NOT (v3,v2) /\ AND (v2,load,v1) /\
NOT (v1,done) /\
COMB
((\x. F) <>
(FST <>
((\x. FST (SND x)) <>
((\x. FST (SND (SND x))) <>
((\x. FST (SND (SND (SND x)))) <>
((\x. FST (SND (SND (SND (SND x))))) <>
((\x. FST (SND (SND (SND (SND (SND x)))))) <>
(\x. FST (SND (SND (SND (SND (SND (SND x))))))))))))))
(inp,v0) /\ DEL (v0,out)) ===> DEV RightShift : thm

Renamed "Compile" to "CompileProg" and defined Compile
to have a more useful meaning. Renamed ConvertCompile to
CompileConvert (as it now does Compile(Convert ...)). Updated README.

Removing some junk from a failed experiment (FactTheory now builds
much more quickly).

Very preliminary attempt to improve netlist synthesis by merging
combinational logic preceding a DEV into the interface to the
DEV. Goal is to cut down the number of handshakes, especially those
packaging up 'selector' logic like ``\(m,n).n`` etc.

Needs further thought and examples.

Minor tweaks; improved and updated README.

Tweaks to improve netlists created with MAKE_NETLIST
(see README). May add more such changes tomorrow.

Added MAKE_NETLIST to generate netlist representations in HOL.

See README and revised FactScript.sml.

Used some old code to drag existential quantifiers to the head of a
conjunction in which I spotted the rather unacceptable:

mk_oracle_thm(Tag.read "EXISTS_OUT_CONV")([],mk_eq(t,t3))

Will need to make this respectable sometime soon. May be a performance
challenge though.

Konrad: is there something better to use off-the-shelf
(EXISTS_OUT_CONV is hol88 era code)

Revision of yesterday's version to make refinements more analogous
to conversions. I've also changed some names around (Sorry).

See README for latest stuff.

Main changes are:

1. Refine renamed to REFINE and now doesn't "depth" scan the circuit.
The scanning is done explicitly by an operator DEPTHR (which
is analogous to DEPTH_CONV).

2. Have added refinement combining operators THENR, ORELSER.

3. Lib renamed to LIB_REFINE.

4. ATMfn renamed to ATM_REFINE.

An example (see FactScript.sml) is:

REFINE
(DEPTHR(LIB_REFINE[FactIter_dev])
THENR DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev])
THENR DEPTHR(LIB_REFINE[MultIter_dev])
THENR DEPTHR ATM_REFINE)
Fact_dev;

I hope this is converging! I should take a rest and do some more PSL
proofs now.

Changed the "design flow" model to be more flexible. Hardware can now
be refined, so top-down development better supported. See README and
revised FactScript.sml example. Libraries are only used for
refinement, not in generating hardware (so library argument of
hwDefine has gone). This is experimental. Comments?

Installing KXS's hwDefine. See README.

Adding Juliano Iyoda's theory of handshaking devices and various
supporting HOL tools. See the README file. Putting the stuff here so that
Cambridge and Utah can collaborate on further developments
----------------------------------------------------------------------
composeScript.sml devScript.sml compileScript.sml CVS: compile.sml
FactScript.sml CVS:
----------------------------------------------------------------------