cudd  3.0.0
The University of Colorado Decision Diagram Package
Functions
ntrBddTest.c File Reference

BDD test functions for the nanotrav program. More...

#include "ntr.h"
#include "cuddInt.h"
Include dependency graph for ntrBddTest.c:

Functions

int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
 Tests BDD minimization functions. More...
 
int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option)
 Tests BDD density-related functions. More...
 
int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option)
 Tests BDD decomposition functions. More...
 
int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
 Verify equivalence of combinational networks. More...
 
int Ntr_TestCofactorEstimate (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Tests BDD cofactor estimate functions. More...
 
int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
 Tests BDD clipping functions. More...
 
int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
 Tests BDD equivalence and containment with don't cares. More...
 
int Ntr_TestClosestCube (DdManager *dd, BnetNetwork *net, NtrOptions *option)
 Tests the Cudd_bddClosestCube function. More...
 
int Ntr_TestTwoLiteralClauses (DdManager *dd, BnetNetwork *net1, NtrOptions *option)
 Tests extraction of two-literal clauses. More...
 
int Ntr_TestCharToVect (DdManager *dd, BnetNetwork *net1, NtrOptions *option)
 Test char-to-vect conversion. More...
 
static int ntrTestMinimizationAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *name, DdNode *c, char *cname, NtrOptions *option)
 Processes one BDD for Ntr_TestMinimization. More...
 
static int ntrTestDensityAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option)
 Processes one BDD for Ntr_TestDensity. More...
 
static int ntrTestDecompAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option)
 Processes one BDD for Ntr_TestDecomp. More...
 
static int ntrTestCofEstAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *name, NtrOptions *option)
 Processes one BDD for Ntr_TestCofactorEstimate. More...
 
static int ntrTestClippingAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *name, DdNode *g, char *gname, NtrOptions *option)
 Processes one BDD for Ntr_TestClipping. More...
 
static int ntrTestEquivAndContainAux (DdManager *dd, BnetNetwork *net1, DdNode *f, char *fname, DdNode *g, char *gname, DdNode *d, char *dname, NtrOptions *option)
 Processes one triplet of BDDs for Ntr_TestEquivAndContain. More...
 
static int ntrTestClosestCubeAux (DdManager *dd, BnetNetwork *net, DdNode *f, char *fname, DdNode *g, char *gname, DdNode **vars, NtrOptions *option)
 Processes one pair of BDDs for Ntr_TestClosestCube. More...
 
static int ntrTestCharToVect (DdManager *dd, DdNode *f, NtrOptions *option)
 Processes one BDDs for Ntr_TestCharToVect. More...
 
static DdNodentrCompress2 (DdManager *dd, DdNode *f, int nvars, int threshold)
 Try hard to squeeze a BDD. More...
 
static BnetNodentrNodeIsBuffer (BnetNode *nd, st_table *hash)
 Checks whether node is a buffer. More...
 

Detailed Description

BDD test functions for the nanotrav program.

Author
Fabio Somenzi

Function Documentation

int Ntr_TestCharToVect ( DdManager dd,
BnetNetwork net1,
NtrOptions option 
)

Test char-to-vect conversion.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestClipping ( DdManager dd,
BnetNetwork net1,
BnetNetwork net2,
NtrOptions option 
)

Tests BDD clipping functions.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestClosestCube ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Tests the Cudd_bddClosestCube function.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestCofactorEstimate ( DdManager dd,
BnetNetwork net,
NtrOptions option 
)

Tests BDD cofactor estimate functions.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestDecomp ( DdManager dd,
BnetNetwork net1,
NtrOptions option 
)

Tests BDD decomposition functions.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestDensity ( DdManager dd,
BnetNetwork net1,
NtrOptions option 
)

Tests BDD density-related functions.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestEquivAndContain ( DdManager dd,
BnetNetwork net1,
BnetNetwork net2,
NtrOptions option 
)

Tests BDD equivalence and containment with don't cares.

Tests functions for BDD equivalence and containment with don't cares, including Cudd_EquivDC and Cudd_bddLeqUnless. This function uses as care set the first output of net2 and checkes equivalence and containment for of all the output pairs of net1.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestMinimization ( DdManager dd,
BnetNetwork net1,
BnetNetwork net2,
NtrOptions option 
)

Tests BDD minimization functions.

Tests BDD minimization functions, including leaf-identifying compaction, squeezing, and restrict. This function uses as constraint the first output of net2 and computes positive and negative cofactors of all the outputs of net1. For each cofactor, it checks whether compaction was safe (cofactor not larger than original function) and that the expansion based on each minimization function (used as a generalized cofactor) equals the original function.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_TestTwoLiteralClauses ( DdManager dd,
BnetNetwork net1,
NtrOptions option 
)

Tests extraction of two-literal clauses.

Returns
1 if successful; 0 otherwise.
Side effects
None
int Ntr_VerifyEquivalence ( DdManager dd,
BnetNetwork net1,
BnetNetwork net2,
NtrOptions option 
)

Verify equivalence of combinational networks.

The two networks are supposed to have the same names for inputs and outputs. The only exception is that the second network may miss output buffers that are present in the first network. This function tries to match both the output and the input of the buffer.

Returns
1 if successful and if the networks are equivalent; -1 if successful, but the networks are not equivalent; 0 otherwise.
Side effects
None
static DdNode* ntrCompress2 ( DdManager dd,
DdNode f,
int  nvars,
int  threshold 
)
static

Try hard to squeeze a BDD.

Returns
a pointer to the squeezed BDD if successful; NULL otherwise.
Side effects
None
See also
ntrTestDensityAux Cudd_SubsetCompress
static BnetNode* ntrNodeIsBuffer ( BnetNode nd,
st_table hash 
)
static

Checks whether node is a buffer.

Returns
a pointer to the input node if nd is a buffer; NULL otherwise.
Side effects
None
static int ntrTestCharToVect ( DdManager dd,
DdNode f,
NtrOptions option 
)
static

Processes one BDDs for Ntr_TestCharToVect.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestCharToVect
static int ntrTestClippingAux ( DdManager dd,
BnetNetwork net1,
DdNode f,
char *  name,
DdNode g,
char *  gname,
NtrOptions option 
)
static

Processes one BDD for Ntr_TestClipping.

It checks whether clipping was correct.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestClipping
static int ntrTestClosestCubeAux ( DdManager dd,
BnetNetwork net,
DdNode f,
char *  fname,
DdNode g,
char *  gname,
DdNode **  vars,
NtrOptions option 
)
static

Processes one pair of BDDs for Ntr_TestClosestCube.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestClosestCube
static int ntrTestCofEstAux ( DdManager dd,
BnetNetwork net,
DdNode f,
char *  name,
NtrOptions option 
)
static

Processes one BDD for Ntr_TestCofactorEstimate.

Returns
1 if successful; 0 otherwise.
Side effects
None
static int ntrTestDecompAux ( DdManager dd,
BnetNetwork net,
DdNode f,
char *  name,
NtrOptions option 
)
static

Processes one BDD for Ntr_TestDecomp.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestDecomp
static int ntrTestDensityAux ( DdManager dd,
BnetNetwork net,
DdNode f,
char *  name,
NtrOptions option 
)
static

Processes one BDD for Ntr_TestDensity.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestDensity ntrCompress1
static int ntrTestEquivAndContainAux ( DdManager dd,
BnetNetwork net1,
DdNode f,
char *  fname,
DdNode g,
char *  gname,
DdNode d,
char *  dname,
NtrOptions option 
)
static

Processes one triplet of BDDs for Ntr_TestEquivAndContain.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestEquivAndContain
static int ntrTestMinimizationAux ( DdManager dd,
BnetNetwork net1,
DdNode f,
char *  name,
DdNode c,
char *  cname,
NtrOptions option 
)
static

Processes one BDD for Ntr_TestMinimization.

Returns
1 if successful; 0 otherwise.
Side effects
None
See also
Ntr_TestMinimization