PROOF(1) CAO-VLSI Reference Manual PROOF(1) NAME proof - Formal proof between two behavioural descriptions 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 sub- set, please call the VHDL manual). proof uses a Reduced Ordered Binary De- cision 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 ex- tracted behaviour obtained by yagle. 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 de- scription (see man yagle). The datas and the commands (the guarded expres- sions) must match separatly. The buses corresponding to completely speci- fied logical functions are represented by a logical multiplexor in both de- scriptions. The two descriptions must have the same interface (VHDL en- tity), if they do not, the formal proof is stopped. proof only uses two system environment variables related to the work direc- tory. 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 de- scriptions (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 descrip- tions. -d The program displays errors when the behavioral descriptions are dif- ferent. Equations are displayed when it's possible. EXAMPLE proof -a -d adder1 adder2 YAGLE 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 uni- versity research. SEE ALSO boom (1), boog (1), loon (1), asimut(1), vhdl(5), vbe(5). ASIM/LIP6 October 1, 1997 PROOF(1)
NAME | SYNOPSIS | DESCRIPTION | ENVIRONMENT VARIABLES | OPTIONS | EXAMPLE | YAGLE | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=proof&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>