===============================================================================
== This directory contains Juliano's HOL files modified by MJCG & KXS        ==
== [see end of this file for version history]                                ==
===============================================================================

composeScript.sml ......... definition of devices and their composition
devScript.sml.............. definition and theorems on liveness
compileScript.sml ......... definitions and theorems to support compiler
compile.sml ............... convert to combinators and compile to circuits
vsynth.sml ................ convert a circuit made with MAKE_CIRCUIT to Verilog
FactScript.sml ............ synthesise naive factorial and dump Verilog
Fact.ml ................... synthesise and simulate factorial and run gtkwave
Fact32 .................... directory with word32 examples (including factorial)
dff ....................... Melham's temporal abstraction theory
Holmakefile ............... instructions for Holmake

*******************************************************************************
There are six levels of abstraction:

 S: Source       (subset of TFL)
 I: Intermediate (source combinators Atm, Seq, Par, Ite, Rec)
 D: Devices      (handshake hardware combinators: ATM, SEQ, PAR, ITE, REC)
 N: Netlist      (abstract device predicates: unclocked DEL, DELT, DELT and DFF)
 C: Circuit      (clocked synchronous device predicates: Dtype, Dff)
 V: Verilog      (netlist pretty-printed into Verilog)

The main user-level functions are hwDefine, cirDefine, REFINE_ALL and
MAKE_NETLIST for creating hardware, refining it and then creating a
netlist representation, and MAKE_CIRCUIT and MAKE_VERILOG for creating
Verilog HDL output.
*******************************************************************************

To make generated hardware devices a bit more readable, the following
(experimental) infixes are now defined in composeScript.sml

   set_fixity ";;" (Infixl 750); overload_on (";;", ``SEQ``)
   set_fixity "||" (Infixl 650); overload_on ("||", ``PAR``)

The bus concatenation operator <> is defined by:

   |- !f g. f <> g = (\t. (f t,g t))

Abstract device netlists are generated by MAKE_NETLIST and contain the
following combinational components:

  |- COMB f (inp,out)      = !t. out t = f (inp t)
  |- CONSTANT c out        = !t. out t = c
  |- MUX (sel,in1,in2,out) = !t. out t = (if sel t then in1 t else in2 t
  |- AND (in1,in2,out)     = !t. out t = in1 t /\ in2 t
  |- OR (in1,in2,out)      = !t. out t = in1 t \/ in2 t
  |- NOT (inp,out)         = !t. out t = ~inp t

and sequential components (registers):

  |- DEL (inp,out) = !t. out(t+1) = inp t
  |- DELT(inp,out) = (out 0 = T) /\ !t. out(t+1) = inp t
  |- DELF(inp,out) = (out 0 = F) /\ !t. out(t+1) = inp t
  |- DFF (d,clk,q) = !t. q(t+1) = if POSEDGE clk (t+1) then d(t+1) else q t

where:

  |- POSEDGE s t = if t=0 then F else ~s(t-1) /\ s t

The sequential components are then implemented in terms of clocked reqisters:

  |- Dtype  (ck,d,q) = !t. q (t+1) = (if Rise ck t then d t else q t)
  |- DtypeT (ck,d,q) = (q 0 = T) /\ Dtype(ck,d,q)
  |- DtypeF (ck,d,q) = (q 0 = F) /\ Dtype(ck,d,q)

where:

 |- Rise s t = ~(s t) /\ s(t+1)

The implementation of DEL, DELT, DELF, DFF in terms of Dtype, DtypeT
and DtypeF involves a temporal abstraction, since Dtype and the
flip-flops are edge-triggered on a clock, but DEL, DELT, DELF, DFF are
not.  The refinement from the unclocked level of abstraction to the
clocked circuit level is implemented formally using infrastructure
from Melham's theory of temporal abstraction in the directory dff:

Using Melham's dff theories it is proved in compileScript.sml that:

 |- InfRise clk ==> !d q. Dtype (clk,d,q)  ==> DEL (d at clk,q at clk)
 |- InfRise clk ==> !d q. DtypeT (clk,d,q) ==> DELT (d at clk,q at clk)
 |- InfRise clk ==> !d q. DtypeF (clk,d,q) ==> DELF (d at clk,q at clk)

Where

 |- Inf sig = !t. ?t'. t < t' /\ sig t'        (* sig true infinitely often) *)
 |- InfRise clk = Inf(Rise clk)      (* clk has infinitely many rising edges *)
 |- s at clk = s when (Rise clk)         (* s sampled at rising edges of clk *)

The term ``(s when P) n`` gives the value of s at the time when P is
true on the n-th occasion (``when`` is defined using the choice
operator in dff/tempabsScript.sml). Thus ``s at clk`` is ``s`` sampled
at rising edges of ``clk`` (the sampling being just before the clock rises).
Note that ``s at clk`` is similar to ``s@clk`` in PSL.

Clocked synchronous circuits using combinational logic and the
registers Dtype and Dff are synthesised using MAKE_CIRCUIT.

*******************************************************************************


hwDefine : term frag list -> thm * thm * thm
--------------------------------------------

Single entrypoint for definitions where proof of termination will
succeed. Allows measure function to be indicated in same quotation as
definition, or not.
                                                                         
    hwDefine lib `(eqns) measuring f`                                    
                                                                         
will use f as the measure function and attempt automatic termination
proof. If successful, returns (|- eqns, |- ind, |- dev) 

NB. the recursion equations must be parenthesized; otherwise, strange
    parse errors result. Also, the name of the defined function must be
    alphanumeric.
                                                                         
One can also not mention the measure function, as in Define:             
                                                                         
    hwDefine `eqns`                                                  
                                                                         
which will accept either non-recursive or recursive specifications. It
returns a triple (|- eqns, |- ind, |- dev) where the ind theorem
should be ignored (it will be boolTheory.TRUTH).

The result of a call to hwRefine is added to the front of a global
reference hwDefineLib, which is accessed by REFINE_ALL.

See FactScript.sml for examples.

REFINE: (term -> thm) -> thm -> thm
-----------------------------------
 
The first argument of REFINE is a "refine function", refine say,
which maps a term representing a circuit, <circuit> say, to a theorem

   |- <circuit'> ===> <circuit>

where ``===>`` is defined by:

   |- P ===> Q  =  !x. P x ==> Q x.

and <circuit'> is a term representing the result of refining <circuit>
with the function refine.

Evaluating

   REFINE refine (|- <circuit> ===> Dev f)

applies refine to <circuit> to get

   |- <circuit'> ===> <circuit>

and then uses transitivity of ===> (DEV_IMP_TRANS) to deduce:

   |- <circuit'> ===> Dev f

Two useful refine functions are ATM_REFINE and LIB_REFINE.


ATM_REFINE : term -> thm
------------------------

This maps ``DEV f`` to |- ATM f ===> DEV f


LIB_REFINE : thm list -> term -> thm
------------------------------------

Evaluating

   LIB_REFINE
    [|- <circuit> ===> DEV f1,
     |- <circuit> ===> DEV f2
     ...
     |- <circuit> ===> DEV fn]
    ``DEV fi``

returns the first theorem |- <circuit> ===> DEV fi that it finds in
the supplied list (i.e. the supplied library). Fails if no refinement
theorem found.

Refinement functions (analogously to conversions and tactics) can be
combined using combinators THENR, ORELSER, REPEATR, DEPTHR. 


THENR : (term -> thm) * (term -> thm) -> (term -> thm)
------------------------------------------------------

Combines refinements sequentially.


ORELSER : (term -> thm) * (term -> thm) -> (term -> thm)
--------------------------------------------------------

Tries first refinement and if that fails tries the second one.

REPEATR : (term -> thm) -> term -> thm
--------------------------------------

Repeates a refinement until no change. Will fail if the refinement
being repeated fails.

ALL_REFINE: term -> thm
-----------------------

ALL_REFINE tm evaluatges to the identity refinement |- tm ===> tm

DEPTHR : (term -> thm) -> (term -> thm)
---------------------------------------------

Scans through a term representing a circuit applying the supplied
refinement function to each subterm of the form ``DEV f`` and 
either generating

 |- DEV g ===> DEV f

if the refinement function returns this, or, if the refinement
function fails:

 |- DEV f ===> DEV f

A refined circuit is then build up using the "monotonicity" theorems:

  SEQ_DEV_IMP =
   |- !P1 P2 Q1 Q2.
       P1 ===> Q1 /\ P2 ===> Q2
       ==>
       (SEQ P1 P2 ===> SEQ Q1 Q2)

  PAR_DEV_IMP =
   |- !P1 P2 Q1 Q2.
       P1 ===> Q1 /\ P2 ===> Q2
       ==>
       (PAR P1 P2 ===> PAR Q1 Q2)

  ITE_DEV_IMP =
   |- !P1 P2 P3 Q1 Q2 Q3.
       P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3
       ==>
       (ITE P1 P2 P3 ===> ITE Q1 Q2 Q3)

  REC_DEV_IMP =
   |- !P1 P2 P3 Q1 Q2 Q3.
       P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3
       ==>
       (REC P1 P2 P3 ===> REC Q1 Q2 Q3)

  PRECEDE_DEV_IMP
  |- !f P Q. P ===> Q ==> PRECEDE f P ===> PRECEDE f Q 

Note that "DEPTHR refine" should never fail.

REFINE: thm -> thm
------------------

Refine using definitions in hwDefineLib and then convert all remaining
DEVs to ATMs. The definition is:

  fun REFINE_ALL th =
   REFINE
    (REPEATR
      (DEPTHR
        (LIB_REFINE(map #3 (!hwDefineLib))
          ORELSER ATM_REFINE
          ORELSER ALL_REFINE)))
    th;


add_combinational : string list -> unit
---------------------------------------

Add a list of constant names to the constants that are implemented as
combinational by the compiler. The definition is:

 fun add_combinational l = 
  (combinational_constants := union l (!combinational_constants)); 

The initial list of combinational constant names (i.e. the initial
value of the reference combinational_constants) is:

  ["T","F","/\\","\\/","~",",","o","CURRY","UNCURRY","COND",
   "FST","SND","=","Seq","Par","Ite","0","NUMERAL","BIT1","BIT2","ZERO",
   "+","-"];


is_combinational : term -> bool
-------------------------------

Test whether a terms is a combinational function of its free variables
(i.e. is built up using only combinational constants).

AddUnop : string * (term * string) -> unit
------------------------------------------

Evaluating

  AddUnop("<component name>", (``<HOL operator>``, "<Verilog operator>"))

defines a HOL component and a corresponding Verilog module and adds
these to the synthesis engine. Currently only types ``:bool``,
``:num`` and ``:word<n>`` are supported; ``:num`` is converted to
Verilog words of width [31:0] (and a warning is issued, since this is
in general invalid). Example:

 AddUnop  ("NOT32", (``$~:word32->word32`` , "~"));

If one doesn't intend to generate Verilog, then just give an arbitrary
string as the Verilog operator (invoking PRINT_VERILOG will then print
a module that uses this string, but you will only get an error when
the Verilog is used, e.g. a simulation is attempted).


AddBinop : string * (term * string) -> unit
-------------------------------------------

Evaluating

  AddBinop
   ("<component name>",
    (``<uncurried HOL binary operator>``, "<Verilog operator>"))

defines a HOL component and a corresponding Verilog module and adds
these to the synthesis engine. Currently only types ``:bool``,
``:num`` and ``:word<n>`` are supported; ``:num`` is converted to
Verilog words of width [31:0] (and a warning is issued, since this is
in general invalid). Examples:

 AddBinop ("ADD",     (``UNCURRY $+ : num#num->num``,           "+"))
 AddBinop ("SUB",     (``UNCURRY $- : num#num->num``,           "-"))

 AddBinop ("ADD32",   (``UNCURRY $+ : word32#word32->word32``,  "+"));
 AddBinop ("SUB32",   (``UNCURRY $- : word32#word32->word32``,  "-"))

 AddBinop ("LESS32",  (``UNCURRY $< : word32#word32->bool``,    "<"));
 AddBinop ("EQ32",    (``UNCURRY $= : word32#word32->bool``,    "=="))

If one doesn't intend to generate Verilog, then just give an arbitrary
string as the Verilog operator (invoking PRINT_VERILOG will then print
a module that uses this string, but you will only get an error when
the Verilog is used, e.g. a simulation is attempted).


MAKE_NETLIST : thm -> thm
-------------------------

Evaluating

 MAKE_NETLIST (|- <device> ===> DEV f)

unfolds <device> using the definitions of ATM, SEQ, PAR, ITE and REC
and normalises the resulting term into a form, <netlist> say,
corresponding to a netlist, and returns

 |- <netlist> 
    ==> 
    DEV f (load,(inp1<>...<>inpm),done,(out1<>...<>outn))


MAKE_CIRCUIT : thm -> thm
-------------------------

Evaluating

 MAKE_CIRCUIT (|- <device> ===> DEV f)

unfolds <device> into a netlist, then replaces DFF by an
implementation in terms of DEL and DELT, and then, using Melham's
temporal abstraction theory in dff, refines any unclocked DEL, DELT
and DELF to clocked Dtype and Dff, and returns:

 |- InfClock clk
    ==>
    <circuit> 
    ==> 
    DEV f (load at clk,
           (inp1<>...<>inpm) at clk,
           done at clk,
           (out1<>...<>outn) at clk)

See FactScript.sml for examples (e.g. FACT_cir).


cirDefine : term frag list -> thm * thm * thm
--------------------------------------------

Invoke hwDefine and then apply MAKE_CIRCUIT and REFINE_ALL to the device:

fun cirDefine qdef =
 let val (def,ind,dev) = hwDefine qdef
 in
  (def, ind, MAKE_CIRCUIT(REFINE_ALL dev))
 end;


PRINT_VERILOG : thm -> unit
---------------------------

Evaluating

 PRINT_VERILOG
  (|- InRise clk 
      ==>
      (?v0 .... vn. <circuit>)
      ==>
      DEV fun (load at clk,
               (inp1 <> ... <> inpu) at clk,
               done at clk,
               (out1 <> ... <> outv) at clk))

creates a module called fun that has the definitions of the modules
used in <circuit>, and prints it and the definitions it needs to
fun.vl.

The header is:

 module fun (clk,load,inp1,...,inpu,done,out1,...,outv);
  input  clk,load;
  input  [<size>:0] inp1,inp2;
  output done;
  output [<size>:0] out;
  wire   clk,done;

where <size> is the appropriate width computed from the types.  The
internal variables v0, ... ,vn are declared to be wires of appropriate
widths (computed from their types).

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


SIMULATE : thm -> (string * string) list -> unit
------------------------------------------------

If thm is:

  |- InRise clk 
      ==>
      (?v0 .... vn. <circuit>)
      ==>
      DEV fun (load at clk,
               (inp1 <> ... <> inpu) at clk,
               done at clk,
               (out1 <> ... <> outv) at clk)

the evaluating:

 SIMULATE thm [("inp1","val1"),...,("inpn","valn")]

dumps Verilog using 

 PRINT_SIMULATION thm (!period_default) [("inp1","val1"),...,("inpn","valn")]

(see below). It then runs a Verilog simulator on fun.vl and then calls
a waveform viewer on fun.vcd.

Currently iverilog (Icarus Verilog:
http://www.icarus.com/eda/verilog/) and cver (GPL Cver:
http://www.pragmatic-c.com/gpl-cver/) are supported as Verilog
simulators and gtkwave (GTKWave:
ftp://ftp.cs.man.ac.uk/pub/amulet/balsa/other-software/gtkwave-2.0.0pre5.tar.gz)
and dinotrace (which comes with GPS Cver) as waveform viewers.

GPS Cver and dinotrace are particularly easy to install, and are now
the default.  To install them, connect to examples/dev and execute:

 wget http://www.pragmatic-c.com/gpl-cver/downloads/gplcver-2.10c.linux.bin.tar.bz2;
 bunzip2 gplcver-2.10c.linux.bin.tar.bz2;
 tar -xf gplcver-2.10c.linux.bin.tar

which should create a directory gplcver-2.10c.linux.bin.

SIMULATE should then just work. Test by evaluating "use Fact.ml;" in hol,
which should launch dinotrace showing a trace of FACT 4 being computed.

You can change the default clock period, which is held in a reference

 val period_default   = ref 5;

To change the default simulator and viewer change the references
verilog_simulator and waveform_viewer. For example, to change to
iverilog and gtkwave do:

 val verilog_simulator = ref iverilog;
 val waveform_viewer   = ref gtkwave;

The executables are held in references, which have default values:

 val iverilog_path   = ref "/usr/bin/iverilog";
 val vvp_path        = ref "/usr/bin/vvp";
 val gtkwave_path    = ref "/usr/bin/gtkwave -a";
 val cver_path       = ref "./gplcver-2.10c.linux.bin/bin/cver";
 val dinotrace_path  = ref "./gplcver-2.10c.linux.bin/bin/dinotrace";

Note that cver_path and dinotrace_path are correct if the installation
described above is performed.


PRINT_SIMULATION : thm -> int -> (string * string) list -> unit
---------------------------------------------------------------

Evaluating

 PRINT_SIMULATION thm period stimulus
 
prints both the Verilog corresponding to thm (see PRINT_VERILOG) and
then adds a clock and a module Main containing an instance of the
clock and an instance of the module generated from thm.

The instance of Clock is created with time between edges as specified
by the parameter period (so really period is 2*period).

The clock line clk and the handshake completion line done are declared
to be boolean wires. 

The input load is declared to be a boolean register and the inputs
inp1, ... ,inpu are declared to be registers of the appropriate width.

A dumpfile called "file.vcd" is created. If the reference variable
dump_all_flag is false (the default) then only changes to clk, load,
and signals inp1, ... ,inpu, done, out1, ... ,outv are declared to
have their changes dumped to the VCD file. If dump_all_flag is true,
then changes to all variables are dumped.

The input variables are driven according to the parameter stimulus,
which is an ML list of tuples of the form:

 [("inp1",val),...,("inpu",val)]

where each input is driven with the supplied value (a string that
prints to a valid Verilog expression).

I am using Icarus Verilog for simulation
(http://www.icarus.com/eda/verilog/) and GTKWave
(http://www.cs.man.ac.uk/apt/tools/gtkwave/) for viewing VCD files.
Both are public domain and seem to work.


*******************************************************************************

Auxiliary functions of interest include the following.

Convert : thm -> thm
--------------------

Convert (|- f x = e) returns a theorem |- f = p, where p is a
combinatory expression built from the combinators Seq, Par and Ite.


RecConvert: : thm -> thm -> thm
-------------------------------

RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) (|- TOTAL(f1,f2,f3))
returns a theorem

 |- f = Rec(p1,p2,p3)

where p1, p2 and p3 are combinatory expressions built from the
combinators Seq, Par and Ite.

A term PRECEDE f d represents a device d preceded by combinational
logic and a term FOLLOW d f represents a device d followed by
combinational logic. 

  |- PRECEDE f d =
      (\(load,inp,done,out). ?v. COMB f (inp,v) /\ d(load,v,done,out))

  |- FOLLOW d f =
      (\(load,inp,done,out). ?v. d(load,inp,done,v) /\ COMB f (v,out))

The function f representing the combinational logic must only contain
constants declared combinational by having their names included in the
ML assignable list "combinational_constants".

Currently PRECEDE and FOLLOW are eliminated when generating netlists,
but they may appear in the output of the compiler (see the
CompileConvert example below).


CompileProg : thm list -> term -> thm
-------------------------------------

CompileProg takes a program and a constant defined in the program

 CompileProg : thm list -> term -> thm
               --------    ----
               program   constant

When the compiler encounters a function f that isn't an application of
Seq, Par or Ite, then DEV f is generated. It is assumed this
will subsequently be refined to hardware (see Refine).

Compile : thm -> thm
--------------------

Compile (|- c = e)  =  CompileProg [|- c = e] ``c``


CompileConvert : thm -> thm
---------------------------

Converts a non-recursive equation to combinators and then compiles to
a device implementation.

Example: 

 Fact;
 > val it = |- !n. Fact n = SND (FactIter (n,1)) : thm

 - CompileConvert Fact;
 > val it =
     |- FOLLOW (PRECEDE (Par (\n. n) (\n. 1)) (DEV FactIter)) SND 
        ===>
        DEV Fact : thm


RecCompileConvert : thm -> thm -> thm
-------------------------------------

Converts a recursive equation to combinators and then compiles to a
device implementation. Needs a totality theorem (user-supplied as third
argument).

Example:

- val FactIter =
    |- FactIter (n,acc) =
       (if n = 0 then (n,acc) else FactIter (n - 1,n * acc))

- val FactIter_TOTAL =
    |- TOTAL
         ((\(n,acc). n = 0),(\(n,acc). (n,acc)),(\(n,acc). (n - 1,n * acc)))

 - RecCompileConvert FactIter FactIter_TOTAL;
 > val it =
     |- REC(FOLLOW (DEV (\(n,acc). n) || DEV (\(n,acc). 0)) (UNCURRY $=))
           (DEV (\x. x))
           (DEV (\x. FST x - 1) || PRECEDE (\x. x) (DEV (UNCURRY $*)))
        ===>
        DEV FactIter


COMB_SYNTH_CONV : term -> thm
-----------------------------

One step of conversion of

 ``COMB 
    (\(i1,...,im). (<term1>,...,<termn>) 
    (inp1 <> ... <> inpm, out1 <> .... outn)``

to a netlist.

Example:

- COMB_SYNTH_CONV 
   ``COMB (\(m,n,p). (m-p, SUC(m+n+(p-1)))) (in1<>in2<>in3,out1<>out2)``;
> val it =
    |- COMB (\(m,n,p). (m - p,SUC (m + n + (p - 1))))
         (in1 <> in2 <> in3,out1 <> out2) =
       COMB (\(m,n,p). m - p) (in1 <> in2 <> in3,out1) /\
       COMB (\(m,n,p). SUC (m + n + (p - 1))) (in1 <> in2 <> in3,out2) : thm

To completely convert to a netlist COMB_SYNTH_CONV needs to be
iterated. Example:

- REDEPTH_CONV COMB_SYNTH_CONV 
   ``COMB (\(m,n,p). (m-p, SUC(m+n+(p-1)))) (in1<>in2<>in3,out1<>out2)``;
> val it =
    |- COMB (\(m,n,p). (m - p,SUC (m + n + (p - 1))))
         (in1 <> in2 <> in3,out1 <> out2) =
       (?v709 v710.
          (v709 = in1) /\ (v710 = in3) /\
          COMB (UNCURRY $-) (v709 <> v710,out1)) /\
       ?v711.
         (?v712 v713.
            (?v714 v715.
               (v714 = in1) /\ (v715 = in2) /\
               COMB (UNCURRY $+)
                 (v714 <> v715,v712)) /\
            (?v716 v717.
               (v716 = in3) /\ CONSTANT 1 v717 /\
               COMB (UNCURRY $-)
                 (v716 <> v717,v713)) /\
            COMB (UNCURRY $+)
              (v712 <> v713,v711)) /\
         COMB SUC (v711,out2) : thm

Note that the redundant variables are pruned by MAKE_NETLIST and also,
for readability, the example above uses ``v709`` but COMB_SYNTH_CONV
actually generates ``%%genvar%%709`.

COMB_SYNTH_CONV may print out some diagnostic stuff if it fails to
prove certain subgoals (though it may nevertheless still produce
something reasonable).  This output can be switched off by setting the
ML reference "if_print_flag" to false.


=============================================================================== 
====== ML definitions and commands to define 32-bit bitwise exclusive-or ======
=============================================================================== 

(*****************************************************************************)
(* The sources have lots of cut-and-paste-and-tweak style repetition for the *)
(* various combinational components (NOT, AND, OR, MUX, ADD, SUB, LESS, EQ). *)
(*                                                                           *)
(* The functions AddUnop and AddBinop cope with some of the repetition,      *)
(* but what follows might also be useful documentation.                      *)
(*                                                                           *)
(* Here are the steps currently needed to add a new component,               *)
(* illustrated with the addition of 32-bit bitwise exclusive-or (XOR32).     *)
(*                                                                           *)
(* These steps are a manual version of what is done when                     *)
(*                                                                           *)
(*  AddBinop ("XOR32", (``UNCURRY $# : word32#word32->word32``, "^"));       *)
(*                                                                           *)
(* is evaluated.                                                             *)
(*****************************************************************************)

(*****************************************************************************)
(* Step 1                                                                    *)
(* ------                                                                    *)
(* Define the component in HOL                                               *)
(* (assumes word32Theory loaded and open)                                    *)
(*****************************************************************************)
val XOR32_def =
 Define 
  `XOR32(in1,in2,out) = !t. out t = (in1 t) # (in2 t)`;

(*****************************************************************************)
(* Step 2                                                                    *)
(* ------                                                                    *)
(* Prove some boilerplate theorems and add to global lists:                  *)
(*****************************************************************************)
val COMB_XOR32 =
 store_thm
  ("COMB_XOR32",
   ``COMB (UNCURRY $#) (in1 <> in2, out) = XOR32(in1,in2,out)``,
   RW_TAC std_ss [COMB_def,BUS_CONCAT_def,XOR32_def]);

add_combinational_components[COMB_XOR32];

val XOR32_at =
 store_thm
  ("XOR32_at",
   ``XOR32(in1,in2,out)
     ==>
     XOR32(in1 at clk,in2 at clk,out at clk)``,
   RW_TAC std_ss [XOR32_def,at_def,tempabsTheory.when]);

add_temporal_abstractions[XOR32_at];

(*****************************************************************************)
(* Step 3                                                                    *)
(* ------                                                                    *)
(* Define a Verilog module as an ML string (XOR32vDef), a function to        *)
(* create an instance with a given size as a string (XOR32vInst), an         *)
(* instance counter (XOR32vInst_count -- used to create unique names for     *)
(* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as   *)
(* an instance, using the type of ``out`` to compute the word width          *)
(* needed to set parameter "size" in XOR32vDef (termToVerilog_XOR32).        *)
(* These functions are added to a couple of global lists.                    *)
(*****************************************************************************)
val XOR32vDef =
"// Combinational bitwise XOR32\n\
\module XOR32 (in1,in2,out);\n\
\ parameter size = 31;\n\
\ input  [size:0] in1,in2;\n\
\ output [size:0] out;\n\
\\n\
\ assign out = in1 ^ in2;\n\
\\n\
\endmodule\n\
\\n";

val XOR32vInst_count = ref 0;
fun XOR32vInst (out:string->unit) [("size",size)] [in1_name,in2_name,out_name] =
 let val count = !XOR32vInst_count
     val _ = (XOR32vInst_count := count+1);
     val inst_name = "XOR32" ^ "_" ^ Int.toString count
 in
 (out " XOR32        "; out inst_name;
  out " (";out in1_name;out",";out in2_name;out",";out out_name; out ");\n";
  out "   defparam ";out inst_name; out ".size = "; out size;
  out ";\n\n")
 end;

add_module ("XOR32", (XOR32vDef, XOR32vInst));

fun termToVerilog_XOR32 (out:string->unit) tm =
 if is_comb tm
     andalso is_const(fst(strip_comb tm))
     andalso (fst(dest_const(fst(strip_comb tm))) = "XOR32")
     andalso is_pair(rand tm)
     andalso (length(strip_pair(rand tm)) = 3)
     andalso all is_var (strip_pair(rand tm))
  then XOR32vInst
        out
        [("size", var2size(last(strip_pair(rand tm))))]
        (map (fst o dest_var) (strip_pair(rand tm)))
  else raise ERR "termToVerilog_XOR32" "bad component term";

termToVerilogLib := (!termToVerilogLib) @ [termToVerilog_XOR32];

===============================================================================
== This directory contains Juliano's HOL files modified by MJCG & KXS        ==
== [Revised version incorporating Juliano's new treatment of recursion]      ==
== [Revised version incorporating liveness]                                  ==
== [04.01.05: improved proofs from KXS in composeScript.sml & devScript.sml] ==
== [09.01.05: MJCG added converter to combinators Seq, Par, Ite, Rec]        ==
== [13.01.05: major tidy and update by MJCG]                                 ==
== [17.01.05: MJCG installed hwDefine and improved examples from KXS]        ==
== [18.01.05: MJCG added Refine and revised FactScript.sml]                  ==
== [19.01.05: MJCG changed to use refinement combinators]                    ==
== [20.01.05: MJCG added netlist synthesis]                                  ==
== [21.01.05: MJCG minor changes and README update]                          ==
== [27.01.05: MJCG added hw synthesis improvements]                          ==
== [28.01.05: MJCG more optimisations and updated README]                    ==
== [29.01.05: MJCG added COMB_SYNTH_CONV removed SEL operators]              ==
== [30.01.05: MJCG added dff: Melham's temporal abstraction theory]          ==
== [01.02.05: MJCG minor tweaks to MAKE_NETLIST and COMB_SYNTH_CONV]         ==
== [06.02.05: MJCG added refinement to clocked dtype registers]              ==
== [08.02.05: MJCG added ?-quantification of internal wires to MAKE_CIRCUIT] ==
== [10.02.05: MJCG split input and output busses]                            ==
== [11.02.05: Holmakefile (thanks to MN) + code improvements (thanks to KXS)]==
== [14.02.05: MJCG added vsynth (defines MAKE_VERILOG)]                      ==
== [15.02.05: MJCG revised MAKE_NETLIST and MAKE_CIRCUIT]                    ==
== [18.02.05: MJCG revised MAKE_VERILOG in vsynth; added MAKE_SIMULATION]    ==
== [28.02.05: MJCG revised added SIMULATE to run iverilog and gtkwave]       ==
== [20.04.05: MJCG updated section on adding new components]                 ==
== [17.05.05: MJCG added hwDefineLib and REFINE_ALL]                         ==
== [30.05.05: MJCG added cirDefine]                                          ==
===============================================================================

Indexes created Wed May 08 10:03:12 MDT 2024