table of contents
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 Université Pierre et Marie CURIE, in Paris, France.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.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 adder2YAGLE¶
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.October 1, 1997 | ASIM/LIP6 |