cuddexport.c

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

{
    int		retval;
    int		i;

    /* Call the function that really gets the job done. */
    for (i = 0; i < n; i++) {
	if (onames == NULL) {
	    retval = fprintf(fp, "f%d = ", i);
	} else {
	    retval = fprintf(fp, "%s = ", onames[i]);
	}
	if (retval == EOF) return(0);
	if (f[i] == DD_ONE(dd)) {
	    retval = fprintf(fp, "CONST1");
	    if (retval == EOF) return(0);
	} else if (f[i] == Cudd_Not(DD_ONE(dd)) || f[i] == DD_ZERO(dd)) {
	    retval = fprintf(fp, "CONST0");
	    if (retval == EOF) return(0);
	} else {
	    retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? "!(" : "");
	    if (retval == EOF) return(0);
	    retval = ddDoDumpFactoredForm(dd,Cudd_Regular(f[i]),fp,inames);
	    if (retval == 0) return(0);
	    retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? ")" : "");
	    if (retval == EOF) return(0);
	}
	retval = fprintf(fp, "%s", i == n-1 ? "" : "\n");
	if (retval == EOF) return(0);
    }

    return(1);

} /* end of Cudd_DumpFactoredForm */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


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


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

  Synopsis    [Performs the recursive step of Cudd_DumpBlif.]

  Description [Performs the recursive step of Cudd_DumpBlif. Traverses
  the BDD f and writes a multiplexer-network description to the file
  pointed by fp in blif format. f is assumed to be a regular pointer
  and ddDoDumpBlif guarantees this assumption in the recursive calls.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
ddDoDumpBlif(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  st_table * visited,
  char ** names)
{
    DdNode	*T, *E;
    int		retval;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    /* If already visited, nothing to do. */
    if (st_is_member(visited, (char *) f) == 1)
        return(1);

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Mark node as visited. */
    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
        return(0);

    /* Check for special case: If constant node, generate constant 1. */
    if (f == DD_ONE(dd)) {
#if SIZEOF_VOID_P == 8
        retval = fprintf(fp, ".names %lx\n1\n",(unsigned long) f / (unsigned long) sizeof(DdNode));
#else
        retval = fprintf(fp, ".names %x\n1\n",(unsigned) f / (unsigned) sizeof(DdNode));
#endif
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Check whether this is an ADD. We deal with 0-1 ADDs, but not
    ** with the general case.
    */
    if (f == DD_ZERO(dd)) {
#if SIZEOF_VOID_P == 8
        retval = fprintf(fp, ".names %lx\n",(unsigned long) f / (unsigned long) sizeof(DdNode));
#else
        retval = fprintf(fp, ".names %x\n",(unsigned) f / (unsigned) sizeof(DdNode));
#endif
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }
    if (cuddIsConstant(f))
	return(0);

    /* Recursive calls. */
    T = cuddT(f);
    retval = ddDoDumpBlif(dd,T,fp,visited,names);
    if (retval != 1) return(retval);
    E = Cudd_Regular(cuddE(f));
    retval = ddDoDumpBlif(dd,E,fp,visited,names);
    if (retval != 1) return(retval);

    /* Write multiplexer taking complement arc into account. */
    if (names != NULL) {
	retval = fprintf(fp,".names %s", names[f->index]);
    } else {
	retval = fprintf(fp,".names %d", f->index);
    }
    if (retval == EOF)
	return(0);

#if SIZEOF_VOID_P == 8
    if (Cudd_IsComplement(cuddE(f))) {
        retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-0 1\n",
	    (unsigned long) T / (unsigned long) sizeof(DdNode),
	    (unsigned long) E / (unsigned long) sizeof(DdNode),
	    (unsigned long) f / (unsigned long) sizeof(DdNode));
    } else {
        retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-1 1\n",
	    (unsigned long) T / (unsigned long) sizeof(DdNode),
	    (unsigned long) E / (unsigned long) sizeof(DdNode),
	    (unsigned long) f / (unsigned long) sizeof(DdNode));
    }
#else
    if (Cudd_IsComplement(cuddE(f))) {
        retval = fprintf(fp," %x %x %x\n11- 1\n0-0 1\n",
	    (unsigned) T / (unsigned) sizeof(DdNode),
	    (unsigned) E / (unsigned) sizeof(DdNode),
	    (unsigned) f / (unsigned) sizeof(DdNode));
    } else {
        retval = fprintf(fp," %x %x %x\n11- 1\n0-1 1\n",
	    (unsigned) T / (unsigned) sizeof(DdNode),
	    (unsigned) E / (unsigned) sizeof(DdNode),
	    (unsigned) f / (unsigned) sizeof(DdNode));
    }
#endif
    if (retval == EOF) {
        return(0);
    } else {
        return(1);
    }

} /* end of ddDoDumpBlif */


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

  Synopsis    [Performs the recursive step of Cudd_DumpDaVinci.]

  Description [Performs the recursive step of Cudd_DumpDaVinci. Traverses
  the BDD f and writes a term expression to the file
  pointed by fp in daVinci format. f is assumed to be a regular pointer
  and ddDoDumpDaVinci guarantees this assumption in the recursive calls.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
ddDoDumpDaVinci(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  st_table * visited,
  char ** names,
  long  mask)
{
    DdNode	*T, *E;
    int		retval;
    long	id;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    id = ((long) f & mask) / sizeof(DdNode);

    /* If already visited, insert a reference. */
    if (st_is_member(visited, (char *) f) == 1) {
	retval = fprintf(fp,"r(\"%lx\")", id);
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Mark node as visited. */
    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
        return(0);

    /* Check for special case: If constant node, generate constant 1. */
    if (Cudd_IsConstant(f)) {
        retval = fprintf(fp, "l(\"%lx\",n(\"constant\",[a(\"OBJECT\",\"%g\")],[]))", id, cuddV(f));
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Recursive calls. */
    if (names != NULL) {
	retval = fprintf(fp,
			 "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%s\"),",
			 id, names[f->index]);
    } else {
	retval = fprintf(fp,
			 "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%d\"),",
			 id, f->index);
    }
    retval = fprintf(fp, "a(\"_GO\",\"ellipse\")],[e(\"then\",[a(\"EDGECOLOR\",\"blue\"),a(\"_DIR\",\"none\")],");
    if (retval == EOF) return(0);
    T = cuddT(f);
    retval = ddDoDumpDaVinci(dd,T,fp,visited,names,mask);
    if (retval != 1) return(retval);
    retval = fprintf(fp, "),e(\"else\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
		     Cudd_IsComplement(cuddE(f)) ? "red" : "green");
    if (retval == EOF) return(0);
    E = Cudd_Regular(cuddE(f));
    retval = ddDoDumpDaVinci(dd,E,fp,visited,names,mask);
    if (retval != 1) return(retval);

    retval = fprintf(fp,")]))");
    if (retval == EOF) {
        return(0);
    } else {
        return(1);
    }

} /* end of ddDoDumpDaVinci */


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

  Synopsis    [Performs the recursive step of Cudd_DumpDDcal.]

  Description [Performs the recursive step of Cudd_DumpDDcal. Traverses
  the BDD f and writes a line for each node to the file
  pointed by fp in DDcal format. f is assumed to be a regular pointer
  and ddDoDumpDDcal guarantees this assumption in the recursive calls.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
ddDoDumpDDcal(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  st_table * visited,
  char ** names,
  long  mask)
{
    DdNode	*T, *E;
    int		retval;
    long	id, idT, idE;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    id = ((long) f & mask) / sizeof(DdNode);

    /* If already visited, do nothing. */
    if (st_is_member(visited, (char *) f) == 1) {
	return(1);
    }

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Mark node as visited. */
    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
        return(0);

    /* Check for special case: If constant node, assign constant. */
    if (Cudd_IsConstant(f)) {
	if (f != DD_ONE(dd) && f != DD_ZERO(dd))
	    return(0);
	retval = fprintf(fp, "n%lx = %g\n", id, cuddV(f));
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Recursive calls. */
    T = cuddT(f);
    retval = ddDoDumpDDcal(dd,T,fp,visited,names,mask);
    if (retval != 1) return(retval);
    E = Cudd_Regular(cuddE(f));
    retval = ddDoDumpDDcal(dd,E,fp,visited,names,mask);
    if (retval != 1) return(retval);
    idT = ((long) T & mask) / sizeof(DdNode);
    idE = ((long) E & mask) / sizeof(DdNode);
    if (names != NULL) {
	retval = fprintf(fp, "n%lx = %s * n%lx + %s' * n%lx%s\n",
			 id, names[f->index], idT, names[f->index],
			 idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
    } else {
	retval = fprintf(fp, "n%lx = v%d * n%lx + v%d' * n%lx%s\n",
			 id, f->index, idT, f->index,
			 idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
    }
    if (retval == EOF) {
        return(0);
    } else {
        return(1);
    }

} /* end of ddDoDumpDDcal */


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

  Synopsis    [Performs the recursive step of Cudd_DumpFactoredForm.]

  Description [Performs the recursive step of
  Cudd_DumpFactoredForm. Traverses the BDD f and writes a factored
  form for each node to the file pointed by fp in terms of the
  factored forms of the children. Constants are propagated, and
  absorption is applied.  f is assumed to be a regular pointer and
  ddDoDumpFActoredForm guarantees this assumption in the recursive
  calls.]

  SideEffects [None]

  SeeAlso     [Cudd_DumpFactoredForm]

******************************************************************************/
static int
ddDoDumpFactoredForm(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  char ** names)
{
    DdNode	*T, *E;
    int		retval;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
    assert(!Cudd_IsConstant(f));
#endif

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Recursive calls. */
    T = cuddT(f);
    E = cuddE(f);
    if (T != DD_ZERO(dd)) {
	if (E != DD_ONE(dd)) {
	    if (names != NULL) {
		retval = fprintf(fp, "%s", names[f->index]);
	    } else {
		retval = fprintf(fp, "x%d", f->index);
	    }
	    if (retval == EOF) return(0);
	}
	if (T != DD_ONE(dd)) {
	    retval = fprintf(fp, "%s(", E != DD_ONE(dd) ? " * " : "");
	    if (retval == EOF) return(0);
	    retval = ddDoDumpFactoredForm(dd,T,fp,names);
	    if (retval != 1) return(retval);
	    retval = fprintf(fp, ")");
	    if (retval == EOF) return(0);
	}
	if (E == Cudd_Not(DD_ONE(dd)) || E == DD_ZERO(dd)) return(1);
	retval = fprintf(fp, " + ");
	if (retval == EOF) return(0);
    }
    E = Cudd_Regular(E);
    if (T != DD_ONE(dd)) {
	if (names != NULL) {
	    retval = fprintf(fp, "!%s", names[f->index]);
	} else {
	    retval = fprintf(fp, "!x%d", f->index);
	}
	if (retval == EOF) return(0);
    }
    if (E != DD_ONE(dd)) {
	retval = fprintf(fp, "%s%s(", T != DD_ONE(dd) ? " * " : "",
			 E != cuddE(f) ? "!" : "");
	if (retval == EOF) return(0);
	retval = ddDoDumpFactoredForm(dd,E,fp,names);
	if (retval != 1) return(retval);
	retval = fprintf(fp, ")");
	if (retval == EOF) return(0);
    }
    return(1);

} /* end of ddDoDumpFactoredForm */