Provided by: alliance_5.0-20110203-4_i386
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 (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.
boom (1), boog (1), loon (1), asimut(1), vhdl(5), vbe(5).