Provided by: alliance_5.0-20110203-4_i386 bug


       proof  - Formal proof between two behavioural descriptions


       proof [-a] [-d]  file1  file2


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


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


            proof -a -d adder1 adder2


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


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