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 DdNode *	ntrCompress2 (DdManager dd, DdNode f, int nvars, int threshold)
	Try hard to squeeze a BDD. More...

static BnetNode *	ntrNodeIsBuffer (BnetNode nd, st_table hash)
	Checks whether node is a buffer. More...

Detailed Description

BDD test functions for the nanotrav program.

Author: Fabio Somenzi

Copyright

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

◆ Ntr_TestCharToVect()

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

Test char-to-vect conversion.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_TestClipping()

int Ntr_TestClipping	(	DdManager *	dd,
		BnetNetwork *	net1,
		BnetNetwork *	net2,
		NtrOptions *	option
	)

Tests BDD clipping functions.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_TestClosestCube()

int Ntr_TestClosestCube	(	DdManager *	dd,
		BnetNetwork *	net,
		NtrOptions *	option
	)

Tests the Cudd_bddClosestCube function.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_TestCofactorEstimate()

int Ntr_TestCofactorEstimate	(	DdManager *	dd,
		BnetNetwork *	net,
		NtrOptions *	option
	)

Tests BDD cofactor estimate functions.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_TestDecomp()

int Ntr_TestDecomp	(	DdManager *	dd,
		BnetNetwork *	net1,
		NtrOptions *	option
	)

Tests BDD decomposition functions.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_TestDensity()

int Ntr_TestDensity	(	DdManager *	dd,
		BnetNetwork *	net1,
		NtrOptions *	option
	)

Tests BDD density-related functions.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_TestEquivAndContain()

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

◆ Ntr_TestMinimization()

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

◆ Ntr_TestTwoLiteralClauses()

int Ntr_TestTwoLiteralClauses	(	DdManager *	dd,
		BnetNetwork *	net1,
		NtrOptions *	option
	)

Tests extraction of two-literal clauses.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Ntr_VerifyEquivalence()

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

◆ ntrCompress2()

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

◆ ntrNodeIsBuffer()

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

◆ ntrTestCharToVect()

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

◆ ntrTestClippingAux()

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

◆ ntrTestClosestCubeAux()

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

◆ ntrTestCofEstAux()

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

◆ ntrTestDecompAux()

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

◆ ntrTestDensityAux()

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

◆ ntrTestEquivAndContainAux()

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

◆ ntrTestMinimizationAux()

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

Functions

Detailed Description

Function Documentation

◆ Ntr_TestCharToVect()

◆ Ntr_TestClipping()

◆ Ntr_TestClosestCube()

◆ Ntr_TestCofactorEstimate()

◆ Ntr_TestDecomp()

◆ Ntr_TestDensity()

◆ Ntr_TestEquivAndContain()

◆ Ntr_TestMinimization()

◆ Ntr_TestTwoLiteralClauses()

◆ Ntr_VerifyEquivalence()

◆ ntrCompress2()

◆ ntrNodeIsBuffer()

◆ ntrTestCharToVect()

◆ ntrTestClippingAux()

◆ ntrTestClosestCubeAux()

◆ ntrTestCofEstAux()

◆ ntrTestDecompAux()

◆ ntrTestDensityAux()

◆ ntrTestEquivAndContainAux()

◆ ntrTestMinimizationAux()