testcudd.c

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

	/* Dump DDs of C and M if so requested. */
	if (dfile != NULL) {
	    dfunc[0] = C;
	    dfunc[1] = M;
	    if (blifOrDot == 1) {
		/* Only dump C because blif cannot handle ADDs */
		retval = Cudd_DumpBlif(dd,1,dfunc,NULL,onames,NULL,dfp);
	    } else {
		retval = Cudd_DumpDot(dd,2,dfunc,NULL,onames,dfp);
	    }
	    if (retval != 1) {
		(void) fprintf(stderr,"abnormal termination\n");
		exit(2);
	    }
	}

	Cudd_RecursiveDeref(dd, C);
	Cudd_RecursiveDeref(dd, M);

	if (clearcache) {
	    if (pr>0) {(void) printf("Clearing the cache... ");}
	    for (i = dd->cacheSlots - 1; i>=0; i--) {
		dd->cache[i].data = NIL(DdNode);
	    }
	    if (pr>0) {(void) printf("done\n");}
	}
	if (pr>0) {
	    (void) printf("Number of variables = %6d\t",dd->size);
	    (void) printf("Number of slots     = %6d\n",dd->slots);
	    (void) printf("Number of keys      = %6d\t",dd->keys);
	    (void) printf("Number of min dead  = %6d\n",dd->minDead);
	}

    } while (multiple && !feof(fp));

    fclose(fp);
    if (dfile != NULL) {
	fclose(dfp);
    }

    /* Second phase: experiment with Walsh matrices. */
    if (!testWalsh(dd,N,cmu,approach,pr)) {
	exit(2);
    }

    /* Check variable destruction. */
    assert(cuddDestroySubtables(dd,3));
    assert(Cudd_DebugCheck(dd) == 0);
    assert(Cudd_CheckKeys(dd) == 0);

    retval = Cudd_CheckZeroRef(dd);
    ok = retval != 0;  /* ok == 0 means O.K. */
    if (retval != 0) {
	(void) fprintf(stderr,
	    "%d non-zero DD reference counts after dereferencing\n", retval);
    }

    if (pr >= 0) {
	(void) Cudd_PrintInfo(dd,stdout);
    }

    Cudd_Quit(dd);

#ifdef MNEMOSYNE
    mnem_writestats();
#endif

    if (pr>0) (void) printf("total time = %s\n",
		util_print_time(util_cpu_time() - startTime));

    if (pr >= 0) util_print_cpu_stats(stdout);
    exit(ok);
    /* NOTREACHED */

} /* end of main */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Prints usage info for testcudd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
usage(char *prog)
{
    (void) fprintf(stderr, "usage: %s [options] [file]\n", prog);
    (void) fprintf(stderr, "   -C\t\tuse CMU multiplication algorithm\n");
    (void) fprintf(stderr, "   -D\t\tenable automatic dynamic reordering\n");
    (void) fprintf(stderr, "   -H\t\tread matrix in Harwell format\n");
    (void) fprintf(stderr, "   -M\t\tturns off memory allocation recording\n");
    (void) fprintf(stderr, "   -P\t\tprint BDD heap profile\n");
    (void) fprintf(stderr, "   -S n\t\tnumber of slots for each subtable\n");
    (void) fprintf(stderr, "   -X n\t\ttarget maximum memory in bytes\n");
    (void) fprintf(stderr, "   -a n\t\tchoose reordering approach (0-13)\n");
    (void) fprintf(stderr, "   \t\t\t0: same as autoMethod\n");
    (void) fprintf(stderr, "   \t\t\t1: no reordering (default)\n");
    (void) fprintf(stderr, "   \t\t\t2: random\n");
    (void) fprintf(stderr, "   \t\t\t3: pivot\n");
    (void) fprintf(stderr, "   \t\t\t4: sifting\n");
    (void) fprintf(stderr, "   \t\t\t5: sifting to convergence\n");
    (void) fprintf(stderr, "   \t\t\t6: symmetric sifting\n");
    (void) fprintf(stderr, "   \t\t\t7: symmetric sifting to convergence\n");
    (void) fprintf(stderr, "   \t\t\t8-10: window of size 2-4\n");
    (void) fprintf(stderr, "   \t\t\t11-13: window of size 2-4 to conv.\n");
    (void) fprintf(stderr, "   \t\t\t14: group sifting\n");
    (void) fprintf(stderr, "   \t\t\t15: group sifting to convergence\n");
    (void) fprintf(stderr, "   \t\t\t16: simulated annealing\n");
    (void) fprintf(stderr, "   \t\t\t17: genetic algorithm\n");
    (void) fprintf(stderr, "   -b\t\tuse blif as format for dumps\n");
    (void) fprintf(stderr, "   -c\t\tclear the cache after each matrix\n");
    (void) fprintf(stderr, "   -d file\tdump DDs to file\n");
    (void) fprintf(stderr, "   -g\t\tselect aggregation criterion (0,5,7)\n");
    (void) fprintf(stderr, "   -h\t\tprints this message\n");
    (void) fprintf(stderr, "   -k\t\tprint the variable permutation\n");
    (void) fprintf(stderr, "   -m\t\tread multiple matrices (only with -H)\n");
    (void) fprintf(stderr, "   -n n\t\tnumber of variables\n");
    (void) fprintf(stderr, "   -p n\t\tcontrol verbosity\n");
    (void) fprintf(stderr, "   -v n\t\tinitial variables in the unique table\n");
    (void) fprintf(stderr, "   -x n\t\tinitial size of the cache\n");
    exit(2);
} /* end of usage */


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

  Synopsis    [Opens a file.]

  Description [Opens a file, or fails with an error message and exits.
  Allows '-' as a synonym for standard input.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static FILE *
open_file(char *filename, char *mode)
{
    FILE *fp;

    if (strcmp(filename, "-") == 0) {
        return mode[0] == 'r' ? stdin : stdout;
    } else if ((fp = fopen(filename, mode)) == NULL) {
        perror(filename);
        exit(1);
    }
    return fp;

} /* end of open_file */


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

  Synopsis    [Tests Walsh matrix multiplication.]

  Description [Tests Walsh matrix multiplication.  Return 1 if successful;
  0 otherwise.]

  SideEffects [May create new variables in the manager.]

  SeeAlso     []

******************************************************************************/
static int
testWalsh(
  DdManager *dd /* manager */,
  int N /* number of variables */,
  int cmu /* use CMU approach to matrix multiplication */,
  int approach /* reordering approach */,
  int pr /* verbosity level */)
{
    DdNode *walsh1, *walsh2, *wtw;
    DdNode **x, **v, **z;
    int i, retval;
    DdNode *one = DD_ONE(dd);
    DdNode *zero = DD_ZERO(dd);

    if (N > 3) {
	x = ALLOC(DdNode *,N);
	v = ALLOC(DdNode *,N);
	z = ALLOC(DdNode *,N);

	for (i = N-1; i >= 0; i--) {
	    Cudd_Ref(x[i]=cuddUniqueInter(dd,3*i,one,zero));
	    Cudd_Ref(v[i]=cuddUniqueInter(dd,3*i+1,one,zero));
	    Cudd_Ref(z[i]=cuddUniqueInter(dd,3*i+2,one,zero));
	}
	Cudd_Ref(walsh1 = Cudd_addWalsh(dd,v,z,N));
	if (pr>0) {(void) printf("walsh1"); Cudd_PrintDebug(dd,walsh1,2*N,pr);}
	Cudd_Ref(walsh2 = Cudd_addWalsh(dd,x,v,N));
	if (cmu) {
	    Cudd_Ref(wtw = Cudd_addTimesPlus(dd,walsh2,walsh1,v,N));
	} else {
	    Cudd_Ref(wtw = Cudd_addMatrixMultiply(dd,walsh2,walsh1,v,N));
	}
	if (pr>0) {(void) printf("wtw"); Cudd_PrintDebug(dd,wtw,2*N,pr);}

	if (approach != CUDD_REORDER_NONE) {
#ifdef DD_DEBUG
	    retval = Cudd_DebugCheck(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
		return(0);
	    }
#endif
	    retval = Cudd_ReduceHeap(dd,(Cudd_ReorderingType)approach,5);
	    if (retval == 0) {
		(void) fprintf(stderr,"Error reported by Cudd_ReduceHeap\n");
		return(0);
	    }
#ifdef DD_DEBUG
	    retval = Cudd_DebugCheck(dd);
	    if (retval != 0) {
		(void) fprintf(stderr,"Error reported by Cudd_DebugCheck\n");
		return(0);
	    }
#endif
	    if (approach == CUDD_REORDER_SYMM_SIFT ||
	    approach == CUDD_REORDER_SYMM_SIFT_CONV) {
		Cudd_SymmProfile(dd,0,dd->size-1);
	    }
	}
	/* Clean up. */
	Cudd_RecursiveDeref(dd, wtw);
	Cudd_RecursiveDeref(dd, walsh1);
	Cudd_RecursiveDeref(dd, walsh2);
	for (i=0; i < N; i++) {
	    Cudd_RecursiveDeref(dd, x[i]);
	    Cudd_RecursiveDeref(dd, v[i]);
	    Cudd_RecursiveDeref(dd, z[i]);
	}
	FREE(x);
	FREE(v);
	FREE(z);
    }
    return(1);

} /* end of testWalsh */

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

  Synopsis    [Tests iterators.]

  Description [Tests iterators on cubes and nodes.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
testIterators(
  DdManager *dd,
  DdNode *M,
  DdNode *C,
  int pr)
{
    int *cube;
    CUDD_VALUE_TYPE value;
    DdGen *gen;
    int q;

    /* Test iterator for cubes. */
    if (pr>1) {
	(void) printf("Testing iterator on cubes:\n");
	Cudd_ForeachCube(dd,M,gen,cube,value) {
	    for (q = 0; q < dd->size; q++) {
		switch (cube[q]) {
		case 0:
		    (void) printf("0");
		    break;
		case 1:
		    (void) printf("1");
		    break;
		case 2:
		    (void) printf("-");
		    break;
		default:
		    (void) printf("?");
		}
	    }
	    (void) printf(" %g\n",value);
	}
	(void) printf("\n");
    }

    if (pr>1) {
	(void) printf("Testing prime expansion of cubes:\n");
	if (!Cudd_bddPrintCover(dd,C,C)) return(0);
    }

    /* Test iterator on nodes. */
    if (pr>2) {
	DdGen *gen;
	DdNode *node;
	(void) printf("Testing iterator on nodes:\n");
	Cudd_ForeachNode(dd,M,gen,node) {
	    if (Cudd_IsConstant(node)) {
#if SIZEOF_VOID_P == 8
		(void) printf("ID = 0x%lx\tvalue = %-9g\n",
			      (unsigned long) node /
			      (unsigned long) sizeof(DdNode),
			      Cudd_V(node));
#else
		(void) printf("ID = 0x%x\tvalue = %-9g\n",
			      (unsigned int) node /
			      (unsigned int) sizeof(DdNode),
			      Cudd_V(node));
#endif
	    } else {
#if SIZEOF_VOID_P == 8
		(void) printf("ID = 0x%lx\tindex = %d\tr = %d\n",
			      (unsigned long) node /
			      (unsigned long) sizeof(DdNode),
			      node->index, node->ref);
#else
		(void) printf("ID = 0x%x\tindex = %d\tr = %d\n",
			      (unsigned int) node /
			      (unsigned int) sizeof(DdNode),
			      node->index, node->ref);
#endif
	    }
	}
	(void) printf("\n");
    }
    return(1);

} /* end of testIterators */


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

  Synopsis    [Tests the functions related to the exclusive OR.]

  Description [Tests the functions related to the exclusive OR. It
  builds the boolean difference of the given function in three
  different ways and checks that the results is the same. Returns 1 if
  successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
testXor(DdManager *dd, DdNode *f, int pr, int nvars)
{
    DdNode *f1, *f0, *res1, *res2;
    int x;

    /* Extract cofactors w.r.t. mid variable. */
    x = nvars / 2;
    f1 = Cudd_Cofactor(dd,f,dd->vars[x]);
    if (f1 == NULL) return(0);
    Cudd_Ref(f1);

    f0 = Cudd_Cofactor(dd,f,Cudd_Not(dd->vars[x]));
    if (f0 == NULL) {
	Cudd_RecursiveDeref(dd,f1);
	return(0);
    }
    Cudd_Ref(f0);

    /* Compute XOR of cofactors with ITE. */
    res1 = Cudd_bddIte(dd,f1,Cudd_Not(f0),f0);
    if (res1 == NULL) return(0);
    Cudd_Ref(res1);

    if (pr>0) {(void) printf("xor1"); Cudd_PrintDebug(dd,res1,nvars,pr);}

    /* Compute XOR of cofactors with XOR. */
    res2 = Cudd_bddXor(dd,f1,f0);
    if (res2 == NULL) {
	Cudd_RecursiveDeref(dd,res1);
	return(0);
    }
    Cudd_Ref(res2);

    if (res1 != res2) {
	if (pr>0) {(void) printf("xor2"); Cudd_PrintDebug(dd,res2,nvars,pr);}
	Cudd_RecursiveDeref(dd,res1);
	Cudd_RecursiveDeref(dd,res2);
	return(0);
    }
    Cudd_RecursiveDeref(dd,res1);
    Cudd_RecursiveDeref(dd,f1);
    Cudd_RecursiveDeref(dd,f0);

    /* Compute boolean difference directly. */
    res1 = Cudd_bddBooleanDiff(dd,f,x);
    if (res1 == NULL) {
	Cudd_RecursiveDeref(dd,res2);
	return(0);
    }
    Cudd_Ref(res1);

    if (res1 != res2) {
	if (pr>0) {(void) printf("xor3"); Cudd_PrintDebug(dd,res1,nvars,pr);}
	Cudd_RecursiveDeref(dd,res1);
	Cudd_RecursiveDeref(dd,res2);
	return(0);
    }
    Cudd_RecursiveDeref(dd,res1);
    Cudd_RecursiveDeref(dd,res2);
    return(1);

} /* end of testXor */


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

  Synopsis    [Tests the Hamming distance functions.]

  Description [Tests the Hammming distance functions. Returns
  1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
testHamming(
  DdManager *dd,
  DdNode *f,
  int pr,
  int nvars)
{
    DdNode **vars, *minBdd, *zero, *scan;
    int i;
    int d;
    int *minterm;
    int size = Cudd_ReadSize(dd);

    vars = ALLOC(DdNode *, size);
    if (vars == NULL) return(0);
    for (i = 0; i < size; i++) {
	vars[i] = Cudd_bddIthVar(dd,i);
    }

    minBdd = Cudd_bddPickOneMinterm(dd,Cudd_Not(f),vars,size);
    Cudd_Ref(minBdd);
    if (pr > 0) {
	(void) printf("Chosen minterm for Hamming distance test: ");
	Cudd_PrintDebug(dd,minBdd,size,pr);
    }

    minterm = ALLOC(int,size);
    if (minterm == NULL) {
	FREE(vars);
	Cudd_RecursiveDeref(dd,minBdd);
	return(0);
    }
    scan = minBdd;
    zero = Cudd_Not(DD_ONE(dd));
    while (!Cudd_IsConstant(scan)) {
	DdNode *R = Cudd_Regular(scan);
	DdNode *T = Cudd_T(R);
	DdNode *E = Cudd_E(R);
	if (R != scan) {
	    T = Cudd_Not(T);
	    E = Cudd_Not(E);
	}
	if (T == zero) {
	    minterm[R->index] = 0;
	    scan = E;
	} else {
	    minterm[R->index] = 1;
	    scan = T;
	}
    }
    Cudd_RecursiveDeref(dd,minBdd);

    d = Cudd_MinHammingDist(dd,f,minterm,size);

    (void) printf("Minimum Hamming distance = %d\n", d);

    FREE(vars);
    FREE(minterm);
    return(1);

} /* end of testHamming */