PROOF(1)

NAME

proof
    - Formal proof between two behavioural descriptions

ORIGIN
This software belongs to the ALLIANCE CAD system from the
CAO-VLSI team at MASI laboratory, University P. and M. Curie
4, place Jussieu ; 75252 PARIS Cedex 05 ; FRANCE
FAX: (33-1) 44.27.62.86 ; E-mail cao-vlsi@masi.ibp.fr

SYNOPSIS

proof [-a] [-d] [-p] file1  file2

DESCRIPTION
Made to run on a data-flow description, proof supports the same subset of VHDL as asimut and logic (for further information about the subset of VHDL used in MASI Cao/Vlsi, please call the VHDL manual or e-mail to cao-vlsi@masi.ibp.fr). proof uses Ordered Binary Decision Diagrams that permit to prove easily the functionnal equivalence between two behavioral descriptions. proof is generally used to compare a behavioural specification with an extracted behaviour obtained by desb.
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 desb to rename the registers in the extracted behavioural description (see man desb). The datas and the commands (the guarded expressions) must matched separatly. The buses corresponding to a completely specified logical function 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 uses only one system environment variable.

ENVIRONMENT VARIABLES

MBK_WORK_LIB gives the path 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.

-p The polarity of the edge triggered is changed within the first description.

EXAMPLE
    proof -a -d adder1 adder2

SEE ALSO
logic(1), asimut(1), vhdl(5), desb(1).

BUGS
Please, report problems or bugs to cao-vlsi@masi.ibp.fr or more precisely burgun@masi.ibp.fr