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

Detailed Description

BDD test functions for the nanotrav program.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.


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
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1