177 lines
4.6 KiB
Groff
177 lines
4.6 KiB
Groff
.\" $Id: bdd.1,v 1.1 1999/05/31 17:30:13 alliance Exp $
|
|
.\" @(#)log.l 0.0 92/08/01 UPMC; Author: Luc Burgun
|
|
.pl -.4
|
|
.TH BDD 1 "October 1, 1997" "ASIM/LIP6" "cao\-vlsi reference manual"
|
|
.SH NAME
|
|
\fBbdd\fP \- Ordered binary decision diagrams representation
|
|
.so man1/alc_origin.1
|
|
.SH DESCRIPTION
|
|
\fIlibbdd.a\fP is a library that allows the representation of a boolean function by a binary decision diagram (BDD). A BDD is a canonical graphic representation for a boolean function. This canonical form enables to test for equivalence or satisfiability.
|
|
All the functions produce a reduced graph. The number of nodes is limited to 500.000 nodes corresponding to 10 Mb in memory.
|
|
.br
|
|
Functions are divided into two groups, the zero level functions (suffixed by \fIBdd\fP) are used to manage BDDs at a low level. A unique \fIIndex\fP must be associated to a identifier signal and the BDDs have to be create by calling the \fBapplyBdd()\fP function. The first level functions (suffixed by \fICct\fP) manage a multi-BDD associated to a combinatory part of a logical circuit. This description can be considered like a set of boolean equations :
|
|
.br
|
|
Output0 = F0(Input0, ... ,Inputn), ... ,Outputm = Fm(Input0, ... ,Inputn).
|
|
.br
|
|
Each function F0, .. , Fn is represented by a BDD in wich each \fIinput\fP is associated to an \fIindex\fP.
|
|
.TP
|
|
\fILow level functions and procedures\fP
|
|
.TP 20
|
|
\fBaddListBdd\fP
|
|
\- adds a BDD to a chained list of BDDs.
|
|
.TP 20
|
|
\fBapplyBdd\fP
|
|
\- applies an operator to a list of BDDs.
|
|
.TP 20
|
|
\fBapplyBinBdd\fP
|
|
\- applies an operator to two BDDs.
|
|
.TP 20
|
|
\fBcomposeBdd\fP
|
|
\- substitutes an index by a BDD in another BDD.
|
|
.TP 20
|
|
\fBconstraintBdd\fP
|
|
\- restricts a BDD to another BDD.
|
|
.TP 20
|
|
\fBcreateNodeTermBdd\fP
|
|
\- creates a terminal node of primary input.
|
|
.TP 20
|
|
\fBdestroyBdd\fP
|
|
\- removes the BDDs system.
|
|
.TP 20
|
|
\fBdisplayBdd\fP
|
|
\- displays a BDD.
|
|
.TP 20
|
|
\fBgcNodeBdd\fP
|
|
\- does a garbage collection.
|
|
.TP 20
|
|
\fBinitializeBdd\fP
|
|
\- initializes the BDDs system.
|
|
.TP 20
|
|
\fBmarkAllBdd\fP
|
|
\- marks all the nodes of the BDDs system.
|
|
.TP 20
|
|
\fBmarkBdd\fP
|
|
\- marks all the nodes of a BDD.
|
|
.TP 20
|
|
\fBnotBdd\fP
|
|
\- complements a BDD.
|
|
.TP 20
|
|
\fBnumberNodeAllBdd\fP
|
|
\- counts the number of nodes used in the BDDs system.
|
|
.TP 20
|
|
\fBnumberNodeBdd\fP
|
|
\- counts the number of nodes used in a BDD.
|
|
.TP 20
|
|
\fBresetBdd\fP
|
|
\- resets the BDDs system.
|
|
.TP 20
|
|
\fBsimplifDcOneBdd\fP
|
|
\- simplifies a BDD with don't cares on its on-set part.
|
|
.TP 20
|
|
\fBsimplifDcZeroBdd\fP
|
|
\- simplifies a BDD with don't cares on its off-set part.
|
|
.TP 20
|
|
\fBsupportChain_listBdd\fP
|
|
\- returns a chained list of nodes that are used in a given BDD.
|
|
.TP 20
|
|
\fBupVarBdd\fP
|
|
\- brings up an index in a BDD.
|
|
.TP
|
|
\fIHigh level functions and procedures\fP
|
|
.TP 20
|
|
\fBablToBddCct\fP
|
|
\- converts an ABL into a BDD within a circuit.
|
|
.TP 20
|
|
\fBaddInputCct\fP
|
|
\- adds an input to a circuit.
|
|
.TP 20
|
|
\fBaddOutputCct\fP
|
|
\- adds an output to a circuit.
|
|
.TP 20
|
|
\fBbddToAblcct\fP
|
|
\- converts a BDD into an ABL.
|
|
.TP 20
|
|
\fBcomposeCct\fP
|
|
\- composes all outputs within a circuit with a BDD.
|
|
.TP 20
|
|
\fBcountNodeCct\fP
|
|
\- counts the number of nodes used within a circuit.
|
|
.TP 20
|
|
\fBconstraintCct\fP
|
|
\- restricts all outputs with a BDD constraint within a circuit.
|
|
.TP 20
|
|
\fBcpOrderCct\fP
|
|
\- copies the association order of the inputs with the indexes in another circuit.
|
|
.TP 20
|
|
\fBdestroyCctfP
|
|
\- removes a circuit.
|
|
.TP 20
|
|
\fBdisplayCct\fP
|
|
\- displays a circuit.
|
|
.TP 20
|
|
\fBgcNodeCct\fP
|
|
\- does a garbarge collection.
|
|
.TP 20
|
|
\fBinitializeCct\fP
|
|
\- creates a circuit.
|
|
.TP 20
|
|
\fBproofCct\fP
|
|
\- checks the equivalence of two circuits.
|
|
.TP 20
|
|
\fBsearchInputCct\fP
|
|
\- searches for the index number associated to an input.
|
|
.TP 20
|
|
\fBsearchOutputCct\fP
|
|
\- searches for the BDD associated to an output.
|
|
.TP 20
|
|
\fBresetCct\fP
|
|
\- resets a circuit.
|
|
.TP 20
|
|
\fBupVarCct\fP
|
|
\- brings up the index of a primary input within a circuit.
|
|
|
|
.br
|
|
.SH SEE ALSO
|
|
.BR log (1),
|
|
.BR abl (1),
|
|
.BR addListBdd (3),
|
|
.BR applyBdd (3),
|
|
.BR applyBinBdd (3),
|
|
.BR composeBdd (3),
|
|
.BR constraintBdd (3),
|
|
.BR createNodeTermBdd (3),
|
|
.BR destroyBdd (3),
|
|
.BR displayBdd (3),
|
|
.BR gcNodeBdd (3),
|
|
.BR initializeBdd (3),
|
|
.BR markBdd (3),
|
|
.BR markAllBdd (3),
|
|
.BR notBdd (3),
|
|
.BR numberNodeAllBdd (3),
|
|
.BR numberNodeBdd (3),
|
|
.BR resetBdd (3),
|
|
.BR simplifDcOneBdd (3),
|
|
.BR simplifDcZeroBdd (3),
|
|
.BR supportChain_listBdd (3),
|
|
.BR upVarBdd (3),
|
|
.BR ablToBddCct (3),
|
|
.BR addInputCct (3),
|
|
.BR addOutputCct (3).
|
|
.BR bddToAblCct (3).
|
|
.BR composeCct (3),
|
|
.BR constraintCct (3),
|
|
.BR cpOrderCct (3),
|
|
.BR destroyCct (3),
|
|
.BR displayCct (3),
|
|
.BR gcNodeCct (3),
|
|
.BR initializeCct (3),
|
|
.BR numberNodeCct (3),
|
|
.BR proofCct (3),
|
|
.BR resetCct (3),
|
|
.BR searchInputCct (3),
|
|
.BR searchOutputCct (3),
|
|
.BR upVarCct (3).
|
|
|
|
.so man1/alc_bug_report.1
|
|
|