1PROOF(1) CAO-VLSI Reference Manual PROOF(1)
2
6 proof - Formal proof between two behavioural descriptions
7
10 This software belongs to the ALLIANCE CAD SYSTEM developed by the ASIM
11 team at LIP6 laboratory of Université Pierre et Marie CURIE, in Paris,
12 France.
13 Web : http://asim.lip6.fr/recherche/alliance/
15 E-mail : alliance-users@asim.lip6.fr
16
18 proof [-a] [-d] file1 file2
19
21 Made to run on a data-flow description, proof supports the same subset
22 of VHDL as asimut and boom and boog (for further informations about
23 this subset, please call the VHDL manual). proof uses a Reduced Ordered
24 Binary Decision Diagrams representation that permits the designer to
25 prove easily the functionnal equivalence between two behavioral
26 descriptions. proof is generally used in order to compare a
27 behavioural specification with an extracted behaviour obtained by
28 yagle.
29 In default mode, a collapsing phase is done on the description by
30 removing all the auxiliary signals (the BDD of the outputs, the regis‐
31 ters and the buses are described from the inputs or the registers). The
32 two descriptions must contain the same ressources (signals register
33 with the same name). It is possible to use the .inf file in yagle (see
34 further remark about YAGLE in this document) to rename the registers in
35 the extracted behavioural description (see man yagle). The datas and
36 the commands (the guarded expressions) must match separatly. The buses
37 corresponding to completely specified logical functions are represented
38 by a logical multiplexor in both descriptions. The two descriptions
39 must have the same interface (VHDL entity), if they do not, the formal
40 proof is stopped.
41 proof only uses two system environment variables related to the work
42 directory.
43
45 MBK_WORK_LIB gives the path for the behavioral descriptions. The
47 default value is the current directory.
48 MBK_CATA_LIB gives some auxiliary pathes for the behavioral descrip‐
51 tions. The default value is the current directory.
52
54 Options may be given in any order before the filenames.
55 -a This option asks proof to keep the common auxiliary signals. proof
58 keeps all intermediate signals that have the same name in both
59 descriptions (A common signal is considered as an input and an
60 output of each description). This option can be useful for
61 descriptions containing large equations. It may be used when
62 proof has failed or if you want to debug in step by step mode
63 the two different descriptions.
64 -d The program displays errors when the behavioral descriptions are
67 different. Equations are displayed when it's possible.
68
70 proof -a -d adder1 adder2
71
74 YAGLE (Functional abstraction) is now comercially distributed by
75 Avertec (http://www.avertec.com/). More information can be obtained at
76 their web site. Binaries of this tool can also be downloaded for non-
77 commercial university research.
78
80 boom (1), boog (1), loon (1), asimut(1), vhdl(5), vbe(5).
81ASIM/LIP6 October 1, 1997 PROOF(1)