cuddgencof.c

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

cuddAddConstrainRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
    DdNode	 *one, *zero;
    unsigned int topf, topc;
    int		 index;

    statLine(dd);
    one = DD_ONE(dd);
    zero = DD_ZERO(dd);

    /* Trivial cases. */
    if (c == one)		return(f);
    if (c == zero)		return(zero);
    if (Cudd_IsConstant(f))	return(f);
    if (f == c)			return(one);

    /* Now f and c are non-constant. */

    /* Check the cache. */
    r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c);
    if (r != NULL) {
	return(r);
    }
    
    /* Recursive step. */
    topf = dd->perm[f->index];
    topc = dd->perm[c->index];
    if (topf <= topc) {
	index = f->index;
	Fv = cuddT(f); Fnv = cuddE(f);
    } else {
	index = c->index;
	Fv = Fnv = f;
    }
    if (topc <= topf) {
	Cv = cuddT(c); Cnv = cuddE(c);
    } else {
	Cv = Cnv = c;
    }

    if (!Cudd_IsConstant(Cv)) {
	t = cuddAddConstrainRecur(dd, Fv, Cv);
	if (t == NULL)
	    return(NULL);
    } else if (Cv == one) {
	t = Fv;
    } else {		/* Cv == zero: return Fnv @ Cnv */
	if (Cnv == one) {
	    r = Fnv;
	} else {
	    r = cuddAddConstrainRecur(dd, Fnv, Cnv);
	    if (r == NULL)
		return(NULL);
	}
	return(r);
    }
    cuddRef(t);

    if (!Cudd_IsConstant(Cnv)) {
	e = cuddAddConstrainRecur(dd, Fnv, Cnv);
	if (e == NULL) {
	    Cudd_RecursiveDeref(dd, t);
	    return(NULL);
	}
    } else if (Cnv == one) {
	e = Fnv;
    } else {		/* Cnv == zero: return Fv @ Cv previously computed */
	cuddDeref(t);
	return(t);
    }
    cuddRef(e);

    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd, e);
	Cudd_RecursiveDeref(dd, t);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert2(dd, Cudd_addConstrain, f, c, r);
    return(r);

} /* end of cuddAddConstrainRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addRestrict.]

  Description [Performs the recursive step of Cudd_addRestrict.
  Returns the restricted ADD if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_addRestrict]

******************************************************************************/
DdNode *
cuddAddRestrictRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode	 *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
    unsigned int topf, topc;
    int		 index;

    statLine(dd);
    one = DD_ONE(dd);
    zero = DD_ZERO(dd);

    /* Trivial cases */
    if (c == one)		return(f);
    if (c == zero)		return(zero);
    if (Cudd_IsConstant(f))	return(f);
    if (f == c)			return(one);

    /* Now f and c are non-constant. */

    /* Check the cache. */
    r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c);
    if (r != NULL) {
	return(r);
    }

    topf = dd->perm[f->index];
    topc = dd->perm[c->index];

    if (topc < topf) {	/* abstract top variable from c */
	DdNode *d, *s1, *s2;

	/* Find cofactors of c. */
	s1 = cuddT(c);
	s2 = cuddE(c);
	/* Take the OR by applying DeMorgan. */
	d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2);
	if (d == NULL) return(NULL);
	cuddRef(d);
	r = cuddAddRestrictRecur(dd, f, d);
	if (r == NULL) {
	    Cudd_RecursiveDeref(dd, d);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_RecursiveDeref(dd, d);
	cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
	cuddDeref(r);
	return(r);
    }

    /* Recursive step. Here topf <= topc. */
    index = f->index;
    Fv = cuddT(f); Fnv = cuddE(f);
    if (topc == topf) {
	Cv = cuddT(c); Cnv = cuddE(c);
    } else {
	Cv = Cnv = c;
    }

    if (!Cudd_IsConstant(Cv)) {
	t = cuddAddRestrictRecur(dd, Fv, Cv);
	if (t == NULL) return(NULL);
    } else if (Cv == one) {
	t = Fv;
    } else {		/* Cv == zero: return(Fnv @ Cnv) */
	if (Cnv == one) {
	    r = Fnv;
	} else {
	    r = cuddAddRestrictRecur(dd, Fnv, Cnv);
	    if (r == NULL) return(NULL);
	}
	return(r);
    }
    cuddRef(t);

    if (!Cudd_IsConstant(Cnv)) {
	e = cuddAddRestrictRecur(dd, Fnv, Cnv);
	if (e == NULL) {
	    Cudd_RecursiveDeref(dd, t);
	    return(NULL);
	}
    } else if (Cnv == one) {
	e = Fnv;
    } else {		/* Cnv == zero: return (Fv @ Cv) previously computed */
	cuddDeref(t);
	return(t);
    }
    cuddRef(e);

    r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd, e);
	Cudd_RecursiveDeref(dd, t);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
    return(r);

} /* end of cuddAddRestrictRecur */



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

  Synopsis    [Performs safe minimization of a BDD.]

  Description [Performs safe minimization of a BDD. Given the BDD
  <code>f</code> of a function to be minimized and a BDD
  <code>c</code> representing the care set, Cudd_bddLICompaction
  produces the BDD of a function that agrees with <code>f</code>
  wherever <code>c</code> is 1.  Safe minimization means that the size
  of the result is guaranteed not to exceed the size of
  <code>f</code>. This function is based on the DAC97 paper by Hong et
  al..  Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction]

******************************************************************************/
DdNode *
cuddBddLICompaction(
  DdManager * dd /* manager */,
  DdNode * f /* function to be minimized */,
  DdNode * c /* constraint (care set) */)
{
    st_table *marktable, *markcache, *buildcache;
    DdNode *res, *zero;

    zero = Cudd_Not(DD_ONE(dd));
    if (c == zero) return(zero);

    /* We need to use local caches for both steps of this operation.
    ** The results of the edge marking step are only valid as long as the
    ** edge markings themselves are available. However, the edge markings
    ** are lost at the end of one invocation of Cudd_bddLICompaction.
    ** Hence, the cache entries for the edge marking step must be
    ** invalidated at the end of this function.
    ** For the result of the building step we argue as follows. The result
    ** for a node and a given constrain depends on the BDD in which the node
    ** appears. Hence, the same node and constrain may give different results
    ** in successive invocations.
    */
    marktable = st_init_table(st_ptrcmp,st_ptrhash);
    if (marktable == NULL) {
	return(NULL);
    }
    markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
    if (markcache == NULL) {
	st_free_table(marktable);
	return(NULL);
    }
    if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
	st_foreach(markcache, MarkCacheCleanUp, NULL);
	st_free_table(marktable);
	st_free_table(markcache);
	return(NULL);
    }
    st_foreach(markcache, MarkCacheCleanUp, NULL);
    st_free_table(markcache);
    buildcache = st_init_table(st_ptrcmp,st_ptrhash);
    if (buildcache == NULL) {
	st_free_table(marktable);
	return(NULL);
    }
    res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
    st_free_table(buildcache);
    st_free_table(marktable);
    return(res);

} /* end of cuddBddLICompaction */


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


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

  Synopsis    [Performs the recursive step of Cudd_bddConstrainDecomp.]

  Description [Performs the recursive step of Cudd_bddConstrainDecomp.
  Returns f super (i) if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_bddConstrainDecomp]

******************************************************************************/
static int
cuddBddConstrainDecomp(
  DdManager * dd,
  DdNode * f,
  DdNode ** decomp)
{
    DdNode *F, *fv, *fvn;
    DdNode *fAbs;
    DdNode *result;
    int ok;

    if (Cudd_IsConstant(f)) return(1);
    /* Compute complements of cofactors. */
    F = Cudd_Regular(f);
    fv = cuddT(F);
    fvn = cuddE(F);
    if (F == f) {
	fv = Cudd_Not(fv);
	fvn = Cudd_Not(fvn);
    }
    /* Compute abstraction of top variable. */
    fAbs = cuddBddAndRecur(dd, fv, fvn);
    if (fAbs == NULL) {
	return(0);
    }
    cuddRef(fAbs);
    fAbs = Cudd_Not(fAbs);
    /* Recursively find the next abstraction and the components of the
    ** decomposition. */
    ok = cuddBddConstrainDecomp(dd, fAbs, decomp);
    if (ok == 0) {
	Cudd_IterDerefBdd(dd,fAbs);
	return(0);
    }
    /* Compute the component of the decomposition corresponding to the
    ** top variable and store it in the decomposition array. */
    result = cuddBddConstrainRecur(dd, f, fAbs);
    if (result == NULL) {
	Cudd_IterDerefBdd(dd,fAbs);
	return(0);
    }
    cuddRef(result);
    decomp[F->index] = result;
    Cudd_IterDerefBdd(dd, fAbs);
    return(1);

} /* end of cuddBddConstrainDecomp */


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

  Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]

  Description [Performs the recursive step of Cudd_bddCharToVect.
  This function maintains the invariant that f is non-zero.
  Returns the i-th component of the vector if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_bddCharToVect]

******************************************************************************/
static DdNode *
cuddBddCharToVect(
  DdManager * dd,
  DdNode * f,
  DdNode * x)
{
    unsigned int topf;
    unsigned int level;
    int comple;

    DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;

    statLine(dd);
    /* Check the cache. */
    res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
    if (res != NULL) {
	return(res);
    }

    F = Cudd_Regular(f);

    topf = cuddI(dd,F->index);
    level = dd->perm[x->index];

    if (topf > level) return(x);

    one = DD_ONE(dd);
    zero = Cudd_Not(one);

    comple = F != f;
    fT = Cudd_NotCond(cuddT(F),comple);
    fE = Cudd_NotCond(cuddE(F),comple);

    if (topf == level) {
	if (fT == zero) return(zero);
	if (fE == zero) return(one);
	return(x);
    }

    /* Here topf < level. */
    if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
    if (fE == zero) return(cuddBddCharToVect(dd, fT, x));

    T = cuddBddCharToVect(dd, fT, x);
    if (T == NULL) {
	return(NULL);
    }
    cuddRef(T);
    E = cuddBddCharToVect(dd, fE, x);
    if (E == NULL) {
	Cudd_IterDerefBdd(dd,T);
	return(NULL);
    }
    cuddRef(E);
    res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
    if (res == NULL) {
	Cudd_IterDerefBdd(dd,T);
	Cudd_IterDerefBdd(dd,E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);
    cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
    return(res);

} /* end of cuddBddCharToVect */


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

  Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]

  Description [Performs the edge marking step of Cudd_bddLICompaction.
  Returns the LUB of the markings of the two outgoing edges of <code>f</code>
  if successful; otherwise CUDD_OUT_OF_MEM.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction cuddBddLICBuildResult]

******************************************************************************/
static int
cuddBddLICMarkEdges(
  DdManager * dd,
  DdNode * f,
  DdNode * c,
  st_table * table,
  st_table * cache)
{
    DdNode *Fv, *Fnv, *Cv, *Cnv;
    DdNode *one, *zero;
    unsigned int topf, topc;
    int	index;
    int comple;
    int resT, resE, res, retval;
    char **slot;
    MarkCacheKey *key;

    one = DD_ONE(dd);
    zero = Cudd_Not(one);

    /* Terminal cases. */
    if (c == zero) return(DD_LIC_DC);
    if (f == one)  return(DD_LIC_1);
    if (f == zero) return(DD_LIC_0);

    /* Make canonical to increase the utilization of the cache. */
    comple = Cudd_IsComplement(f);
    f = Cudd_Regular(f);
    /* Now f is a regular pointer to a non-constant node; c may be
    ** constant, or it may be complemented.
    */

    /* Check the cache. */
    key = ALLOC(MarkCacheKey, 1);
    if (key == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(CUDD_OUT_OF_MEM);
    }
    key->f = f; key->c = c;
    if (st_lookup(cache, (char *)key, (char **)&res)) {
	FREE(key);
	if (comple) {
	    if (res == DD_LIC_0) res = DD_LIC_1;
	    else if (res == DD_LIC_1) res = DD_LIC_0;
	}
	return(res);
    }

    /* Recursive step. */
    topf = dd->perm[f->index];