testcudd.c

主要进行大规模的电路综合

/**CFile***********************************************************************

  FileName    [testcudd.c]

  PackageName [cudd]

  Synopsis    [Sanity check tests for some CUDD functions.]

  Description [testcudd reads a matrix with real coefficients and
  transforms it into an ADD. It then performs various operations on
  the ADD and on the BDD corresponding to the ADD pattern. Finally,
  testcudd tests functions relate to Walsh matrices and matrix
  multiplication.]

  SeeAlso     []

  Author      [Fabio Somenzi]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "util.h"
#include "cuddInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define TESTCUDD_VERSION	"TestCudd Version #1.0, Release date 3/17/01"

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: testcudd.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
#endif

static char *onames[] = { "C", "M" }; /* names of functions to be dumped */

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void usage ARGS((char * prog));
static FILE *open_file ARGS((char *filename, char *mode));
static int testIterators ARGS((DdManager *dd, DdNode *M, DdNode *C, int pr));
static int testXor ARGS((DdManager *dd, DdNode *f, int pr, int nvars));
static int testHamming ARGS((DdManager *dd, DdNode *f, int pr, int nvars));
static int testWalsh ARGS((DdManager *dd, int N, int cmu, int approach, int pr));

/**AutomaticEnd***************************************************************/


/**Function********************************************************************

  Synopsis    [Main function for testcudd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
main(int argc, char **argv)
{
    FILE *fp;           /* pointer to input file */
    char *file = "";	/* input file name */
    FILE *dfp = NULL;	/* pointer to dump file */
    char *dfile;	/* file for DD dump */
    DdNode *dfunc[2];	/* addresses of the functions to be dumped */
    DdManager *dd;	/* pointer to DD manager */
    DdNode *one, *zero;	/* fast access to constant functions */
    DdNode *M;
    DdNode **x;		/* pointers to variables */
    DdNode **y;		/* pointers to variables */
    DdNode **xn;       	/* complements of row variables */
    DdNode **yn_;      	/* complements of column variables */
    DdNode **xvars;
    DdNode **yvars;
    DdNode *C;		/* result of converting from ADD to BDD */
    DdNode *ess;	/* cube of essential variables */
    DdNode *shortP;	/* BDD cube of shortest path */
    DdNode *largest;	/* BDD of largest cube */
    DdNode *shortA;	/* ADD cube of shortest path */
    DdNode *constN;	/* value returned by evaluation of ADD */
    DdNode *ycube;	/* cube of the negated y vars for c-proj */
    DdNode *CP;		/* C-Projection of C */
    DdNode *CPr;	/* C-Selection of C */
    int    length;	/* length of the shortest path */
    int    nx;			/* number of variables */
    int    ny;
    int    maxnx;
    int    maxny;
    int    m;
    int    n;
    int    N;
    int    cmu;			/* use CMU multiplication */
    int    pr;			/* verbose printout level */
    int    harwell;
    int    multiple;		/* read multiple matrices */
    int    ok;
    int    c;			/* variable to read in options */
    int    approach;		/* reordering approach */
    int    autodyn;		/* automatic reordering */
    int    groupcheck;		/* option for group sifting */
    int    profile;		/* print heap profile if != 0 */
    int    keepperm;		/* keep track of permutation */
    int    clearcache;		/* clear the cache after each matrix */
    int    blifOrDot;		/* dump format: 0 -> dot, 1 -> blif, ... */
    int    retval;		/* return value */
    int    i;			/* loop index */
    long   startTime;		/* initial time */
    long   lapTime;
    int    size;
    unsigned int cacheSize, maxMemory;
    unsigned int nvars,nslots;

    startTime = util_cpu_time();

    approach = CUDD_REORDER_NONE;
    autodyn = 0;
    pr = 0;
    harwell = 0;
    multiple = 0;
    profile = 0;
    keepperm = 0;
    cmu = 0;
    N = 4;
    nvars = 4;
    cacheSize = 127;
    maxMemory = 0;
    nslots = CUDD_UNIQUE_SLOTS;
    clearcache = 0;
    groupcheck = CUDD_GROUP_CHECK7;
    dfile = NULL;
    blifOrDot = 0; /* dot format */

    /* Parse command line. */
    while ((c = util_getopt(argc, argv, "CDHMPS:a:bcd:g:hkmn:p:v:x:X:"))
	   != EOF) {
	switch(c) {
	case 'C':
	    cmu = 1;
	    break;
	case 'D':
	    autodyn = 1;
	    break;
	case 'H':
	    harwell = 1;
	    break;
	case 'M':
#ifdef MNEMOSYNE
	    (void) mnem_setrecording(0);
#endif
	    break;
	case 'P':
	    profile = 1;
	    break;
	case 'S':
	    nslots = atoi(util_optarg);
	    break;
	case 'X':
	    maxMemory = atoi(util_optarg);
	    break;
	case 'a':
	    approach = atoi(util_optarg);
	    break;
	case 'b':
	    blifOrDot = 1; /* blif format */
	    break;
	case 'c':
	    clearcache = 1;
	    break;
	case 'd':
	    dfile = util_optarg;
	    break;
	case 'g':
	    groupcheck = atoi(util_optarg);
	    break;
	case 'k':
	    keepperm = 1;
	    break;
	case 'm':
	    multiple = 1;
	    break;
	case 'n':
	    N = atoi(util_optarg);
	    break;
	case 'p':
	    pr = atoi(util_optarg);
	    break;
	case 'v':
	    nvars = atoi(util_optarg);
	    break;
	case 'x':
	    cacheSize = atoi(util_optarg);
	    break;
	case 'h':
	default:
	    usage(argv[0]);
	    break;
	}
    }

    if (argc - util_optind == 0) {
	file = "-";
    } else if (argc - util_optind == 1) {
	file = argv[util_optind];
    } else {
	usage(argv[0]);
    }
    if ((approach<0) || (approach>17)) {
	(void) fprintf(stderr,"Invalid approach: %d \n",approach);
	usage(argv[0]);
    }

    if (pr >= 0) {
	(void) printf("# %s\n", TESTCUDD_VERSION);
	/* Echo command line and arguments. */
	(void) printf("#");
	for (i = 0; i < argc; i++) {
	    (void) printf(" %s", argv[i]);
	}
	(void) printf("\n");
	(void) fflush(stdout);
    }

    /* Initialize manager and provide easy reference to terminals. */
    dd = Cudd_Init(nvars,0,nslots,cacheSize,maxMemory);
    one = DD_ONE(dd);
    zero = DD_ZERO(dd);
    dd->groupcheck = (Cudd_AggregationType) groupcheck;
    if (autodyn) Cudd_AutodynEnable(dd,CUDD_REORDER_SAME);

    /* Open input file. */
    fp = open_file(file, "r");

    /* Open dump file if requested */
    if (dfile != NULL) {
	dfp = open_file(dfile, "w");
    }

    x = y = xn = yn_ = NULL;
    do {
	/* We want to start anew for every matrix. */
	maxnx = maxny = 0;
	nx = maxnx; ny = maxny;
	if (pr>0) lapTime = util_cpu_time();
	if (harwell) {
	    if (pr >= 0) (void) printf(":name: ");
	    ok = Cudd_addHarwell(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
	    &m, &n, 0, 2, 1, 2, pr);
	} else {
	    ok = Cudd_addRead(fp, dd, &M, &x, &y, &xn, &yn_, &nx, &ny,
	    &m, &n, 0, 2, 1, 2);
	    if (pr >= 0)
		(void) printf(":name: %s: %d rows %d columns\n", file, m, n);
	}
	if (!ok) {
	    (void) fprintf(stderr, "Error reading matrix\n");
	    exit(1);
	}

	if (nx > maxnx) maxnx = nx;
	if (ny > maxny) maxny = ny;

	/* Build cube of negated y's. */
	ycube = DD_ONE(dd);
	Cudd_Ref(ycube);
	for (i = maxny - 1; i >= 0; i--) {
	    DdNode *tmpp;
	    tmpp = Cudd_bddAnd(dd,Cudd_Not(dd->vars[y[i]->index]),ycube);
	    if (tmpp == NULL) exit(2);
	    Cudd_Ref(tmpp);
	    Cudd_RecursiveDeref(dd,ycube);
	    ycube = tmpp;
	}
	/* Initialize vectors of BDD variables used by priority func. */
	xvars = ALLOC(DdNode *, nx);
	if (xvars == NULL) exit(2);
	for (i = 0; i < nx; i++) {
	    xvars[i] = dd->vars[x[i]->index];
	}
	yvars = ALLOC(DdNode *, ny);
	if (yvars == NULL) exit(2);
	for (i = 0; i < ny; i++) {
	    yvars[i] = dd->vars[y[i]->index];
	}

	/* Clean up */
	for (i=0; i < maxnx; i++) {
	    Cudd_RecursiveDeref(dd, x[i]);
	    Cudd_RecursiveDeref(dd, xn[i]);
	}
	FREE(x);
	FREE(xn);
	for (i=0; i < maxny; i++) {
	    Cudd_RecursiveDeref(dd, y[i]);
	    Cudd_RecursiveDeref(dd, yn_[i]);
	}
	FREE(y);
	FREE(yn_);

	if (pr>0) {(void) printf(":1: M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}

	if (pr>0) (void) printf(":2: time to read the matrix = %s\n",
		    util_print_time(util_cpu_time() - lapTime));

	C = Cudd_addBddPattern(dd, M);
	if (C == 0) exit(2);
	Cudd_Ref(C);
	if (pr>0) {(void) printf(":3: C"); Cudd_PrintDebug(dd,C,nx+ny,pr);}

	/* Test iterators. */
	retval = testIterators(dd,M,C,pr);
	if (retval == 0) exit(2);

	cuddCacheProfile(dd,stdout);

	/* Test XOR */
	retval = testXor(dd,C,pr,nx+ny);
	if (retval == 0) exit(2);

	/* Test Hamming distance functions. */
	retval = testHamming(dd,C,pr,nx+ny);
	if (retval == 0) exit(2);

	/* Test selection functions. */
	CP = Cudd_CProjection(dd,C,ycube);
	if (CP == NULL) exit(2);
	Cudd_Ref(CP);
	if (pr>0) {(void) printf("ycube"); Cudd_PrintDebug(dd,ycube,nx+ny,pr);}
	if (pr>0) {(void) printf("CP"); Cudd_PrintDebug(dd,CP,nx+ny,pr);}

	if (nx == ny) {
	    CPr = Cudd_PrioritySelect(dd,C,xvars,yvars,(DdNode **)NULL,
		(DdNode *)NULL,ny,Cudd_Xgty);
	    if (CPr == NULL) exit(2);
	    Cudd_Ref(CPr);
	    if (pr>0) {(void) printf(":4: CPr"); Cudd_PrintDebug(dd,CPr,nx+ny,pr);}
	    if (CP != CPr) {
		(void) printf("CP != CPr!\n");
	    }
	    Cudd_RecursiveDeref(dd, CPr);
	}
	FREE(xvars); FREE(yvars);

	Cudd_RecursiveDeref(dd, CP);
	Cudd_RecursiveDeref(dd, ycube);

	/* Test functions for essential variables. */
	ess = Cudd_FindEssential(dd,C);
	if (ess == NULL) exit(2);
	Cudd_Ref(ess);
	if (pr>0) {(void) printf(":4: ess"); Cudd_PrintDebug(dd,ess,nx+ny,pr);}
	Cudd_RecursiveDeref(dd, ess);

	/* Test functions for shortest paths. */
	shortP = Cudd_ShortestPath(dd, M, NULL, NULL, &length);
	if (shortP == NULL) exit(2);
	Cudd_Ref(shortP);
	if (pr>0) {
	    (void) printf(":5: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
	}
	/* Test functions for largest cubes. */
	largest = Cudd_LargestCube(dd, Cudd_Not(C), &length);
	if (largest == NULL) exit(2);
	Cudd_Ref(largest);
	if (pr>0) {
	    (void) printf(":5b: largest");
	    Cudd_PrintDebug(dd,largest,nx+ny,pr);
	}
	Cudd_RecursiveDeref(dd, largest);

	/* Test Cudd_addEvalConst and Cudd_addIteConstant. */
	shortA = Cudd_BddToAdd(dd,shortP);
	if (shortA == NULL) exit(2);
	Cudd_Ref(shortA);
	Cudd_RecursiveDeref(dd, shortP);
	constN = Cudd_addEvalConst(dd,shortA,M);
	if (constN == DD_NON_CONSTANT) exit(2);
	if (Cudd_addIteConstant(dd,shortA,M,constN) != constN) exit(2);
	if (pr>0) {(void) printf("The value of M along the chosen shortest path is %g\n", cuddV(constN));}
	Cudd_RecursiveDeref(dd, shortA);

	shortP = Cudd_ShortestPath(dd, C, NULL, NULL, &length);
	if (shortP == NULL) exit(2);
	Cudd_Ref(shortP);
	if (pr>0) {
	    (void) printf(":6: shortP"); Cudd_PrintDebug(dd,shortP,nx+ny,pr);
	}

	/* Test Cudd_bddIteConstant and Cudd_bddLeq. */
	if (!Cudd_bddLeq(dd,shortP,C)) exit(2);
	if (Cudd_bddIteConstant(dd,Cudd_Not(shortP),one,C) != one) exit(2);
	Cudd_RecursiveDeref(dd, shortP);

	if (profile) {
	    retval = cuddHeapProfile(dd);
	}

	size = dd->size;

	if (pr>0) {
	    (void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
	}

	/* Reorder if so requested. */
        if (approach != CUDD_REORDER_NONE) {
#ifndef DD_STATS
	    retval = Cudd_EnableReorderingReporting(dd);
	    if (retval == 0) {
		(void) fprintf(stderr,"Error reported by Cudd_EnableReorderingReporting\n");
		exit(3);
	    }
#endif
#ifdef DD_DEBUG
	    retval = Cudd_DebugCheck(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
		exit(3);
	    }
	    retval = Cudd_CheckKeys(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
		exit(3);
	    }
#endif
	    retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
	    if (retval == 0) {
		(void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
		exit(3);
	    }
#ifndef DD_STATS
	    retval = Cudd_DisableReorderingReporting(dd);
	    if (retval == 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DisableReorderingReporting\n");
		exit(3);
	    }
#endif
#ifdef DD_DEBUG
	    retval = Cudd_DebugCheck(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
		exit(3);
	    }
	    retval = Cudd_CheckKeys(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_CheckKeys\n");
		exit(3);
	    }
#endif
	    if (approach == CUDD_REORDER_SYMM_SIFT ||
	    approach == CUDD_REORDER_SYMM_SIFT_CONV) {
		Cudd_SymmProfile(dd,0,dd->size-1);
	    }

	    if (pr>0) {
		(void) printf("Average distance: %g\n", Cudd_AverageDistance(dd));
	    }

	    if (keepperm) {
		/* Print variable permutation. */
		(void) printf("Variable Permutation:");
		for (i=0; i<size; i++) {
		    if (i%20 == 0) (void) printf("\n");
		    (void) printf("%d ", dd->invperm[i]);
		}
		(void) printf("\n");
		(void) printf("Inverse Permutation:");
		for (i=0; i<size; i++) {
		    if (i%20 == 0) (void) printf("\n");
		    (void) printf("%d ", dd->perm[i]);
		}
		(void) printf("\n");
	    }

	    if (pr>0) {(void) printf("M"); Cudd_PrintDebug(dd,M,nx+ny,pr);}

	    if (profile) {
		retval = cuddHeapProfile(dd);
	    }

	}