PROOF(1)						     CAO-VLSI Reference Manual							  PROOF(1)

NAME

       proof  - Formal proof between two behavioural descriptions

ORIGIN

       This  software  belongs	to  the  ALLIANCE CAD SYSTEM developed by the ASIM team at LIP6 laboratory of Universite Pierre et Marie CURIE, in
       Paris, France.

       Web : http://asim.lip6.fr/recherche/alliance/
       E-mail : alliance-users@asim.lip6.fr

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 descrip-
       tions 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 descrip-
	      tions containing large equations. It may be used when proof has failed or if you want to debug in step by step mode the two  differ-
	      ent 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).

BUG REPORT

       This tool is under development at the ASIM department of the LIP6 laboratory.
       We need your feedback to improve documentation and tools.

ASIM
/LIP6							  October 1, 1997							  PROOF(1)