1PROOF(1)                   CAO-VLSI Reference Manual                  PROOF(1)
2
3
4

NAME

6       proof  - Formal proof between two behavioural descriptions
7
8

ORIGIN

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
14       Web : http://asim.lip6.fr/recherche/alliance/
15       E-mail : alliance-users@asim.lip6.fr
16

SYNOPSIS

18       proof [-a] [-d]  file1  file2
19

DESCRIPTION

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

ENVIRONMENT VARIABLES

45
46       MBK_WORK_LIB gives  the  path  for  the  behavioral  descriptions.  The
47              default value is the current directory.
48
49
50       MBK_CATA_LIB  gives  some  auxiliary pathes for the behavioral descrip‐
51              tions. The default value is the current directory.
52

OPTIONS

54       Options may be given in any order before the filenames.
55
56
57       -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
65
66       -d The program displays errors when  the  behavioral  descriptions  are
67              different. Equations are displayed when it's possible.
68

EXAMPLE

70            proof -a -d adder1 adder2
71
72

YAGLE

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

SEE ALSO

80        boom (1), boog (1), loon (1), asimut(1), vhdl(5), vbe(5).
81
82
83
84
85
86
87ASIM/LIP6                       October 1, 1997                       PROOF(1)
Impressum