NAME

       proof  - Formal proof between two behavioural descriptions

SYNOPSIS

       proof [-a] [-d]  file1  file2

DESCRIPTION

       Made  to  run  on  a data-flow description, proof supports the same subset of VHDL as asimut and boom and
       boog (for further informations about this subset, please call the VHDL  manual).  proof  uses  a  Reduced
       Ordered Binary Decision Diagrams representation that permits the designer to prove easily the functionnal
       equivalence between two behavioral  descriptions.   proof  is  generally  used  in  order  to  compare  a
       behavioural specification with an extracted behaviour obtained by yagle.
       In default mode, a collapsing phase is done on the description by removing all the auxiliary signals (the
       BDD of the outputs, the registers and the buses are described from the inputs or the registers). The  two
       descriptions  must  contain the same ressources (signals register with the same name).  It is possible to
       use the .inf file in yagle (see further remark about YAGLE in this document) to rename the  registers  in
       the  extracted  behavioural  description  (see  man  yagle).  The  datas  and  the  commands (the guarded
       expressions) must match separatly. The buses corresponding to completely specified logical functions  are
       represented  by  a  logical  multiplexor  in  both descriptions.  The two descriptions must have the same
       interface (VHDL entity), if they do not, the formal proof is stopped.
       proof only uses two system environment variables related to the work directory.

ENVIRONMENT VARIABLES

       MBK_WORK_LIB gives the path for the behavioral descriptions. The default value is the current directory.

       MBK_CATA_LIB gives some auxiliary pathes for the  behavioral  descriptions.  The  default  value  is  the
              current directory.

OPTIONS

       Options may be given in any order before the filenames.

       -a This option asks proof to keep the common auxiliary signals. proof keeps all intermediate signals that
              have the same name in both descriptions (A common signal is considered as an input and  an  output
              of  each  description).  This option can be useful for descriptions containing large equations. It
              may be used when proof has failed or if you want to debug in step by step mode the  two  different
              descriptions.

       -d  The  program  displays errors when the behavioral descriptions are different. Equations are displayed
              when it's possible.

EXAMPLE

            proof -a -d adder1 adder2

YAGLE

       YAGLE (Functional abstraction) is now comercially distributed by Avertec (http://www.avertec.com/).  More
       information  can  be  obtained  at  their web site. Binaries of this tool can also be downloaded for non-
       commercial university research.

SEE ALSO

        boom (1), boog (1), loon (1), asimut(1), vhdl(5), vbe(5).