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