riscv
/
alliance
mirror of https://gitlab.lip6.fr/vlsi-eda/alliance.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

offuscated man

This commit is contained in:
Christophe Alexandre 2002-10-17 16:14:59 +00:00
parent 653790f8ce
commit d09ef85ce3
1 changed files with 11 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
alliance/src/proof/man1/proof.1
View File

@ -1,4 +1,4 @@
.\" $Id: proof.1,v 1.1 2002/04/18 12:47:46 ludo Exp $
.\" $Id: proof.1,v 1.2 2002/10/17 16:14:59 xtof Exp $
.\" @(#)Labo.l 1.2 91/11/01 UPMC; Author: BURGUN L.
.pl -.4
.TH PROOF 1 "October 1, 1997" "ASIM/LIP6" "CAO\-VLSI Reference Manual"
@ -13,11 +13,11 @@ proof
.br
.SH DESCRIPTION
.br
Made to run on a data-flow description, \fBproof\fP supports the same subset of VHDL as asimut and bop and scmap (for further informations about this subset, please call the VHDL manual). \fBproof\fP uses a Reduced Ordered Binary Decision Diagrams representation that permits the designer to prove easily the functionnal equivalence between two behavioral descriptions.
Made to run on a data-flow description, \fBproof\fP supports the same subset of VHDL as asimut and boom and boog (for further informations about this subset, please call the VHDL manual). \fBproof\fP uses a Reduced Ordered Binary Decision Diagrams representation that permits the designer to prove easily the functionnal equivalence between two behavioral descriptions.
\fBproof\fP is generally used in order to compare a behavioural specification with an extracted behaviour obtained by \fByagle\fP.
.br
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 \fI.inf\fP file in \fByagle\fP to rename the registers in the extracted behavioural description (see man \fByagle\fP). 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.
It is possible to use the \fI.inf\fP file in \fByagle\fP (see further remark about \fBYAGLE\fP in this document) to rename the registers in the extracted behavioural description (see man \fByagle\fP). 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 \fBproof\fP is stopped.
.br
\fBproof\fP only uses two system environment variables related to the work directory.
@ -47,10 +47,16 @@ The program displays errors when the behavioral descriptions are different. Equa
.br
proof -a -d adder1 adder2
.SH YAGLE
.br
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.
.SH SEE ALSO
.br
\fBbop\fP (1), \fBglop\fP (1), \fBscmap\fP (1), \fBc4map\fP (1),
\fBasimut\fP(1), \fBvhdl\fP(5), \fByagle\fP(1), \fBvbe\fP(5).
\fBboom\fP (1), \fBboog\fP (1), \fBloon\fP (1),
\fBasimut\fP(1), \fBvhdl\fP(5), \fBvbe\fP(5).
.so man1/alc_bug_report.1