extrautilprint.c

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

  Synopsis    []

  Description []
  
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Extra_WriteBlifStop( FILE * pFile )
{
	fprintf( pFile, ".end\n\n" );
	fclose( pFile );
}
/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Extra_WriteBlifGate( FILE * pFile, char * pInputNames[], int Polars[], int nInputs, char * pOutputName, int GateType )
{
	int v, i;

	// write the names line
	fprintf( pFile, ".names" );
	for ( v = 0; v < nInputs; v++ )
		fprintf( pFile, " %s", pInputNames[v] );
	fprintf( pFile, " %s\n", pOutputName );

	if ( GateType == EXTRA_GATE_TYPE_BUF )
		fprintf( pFile, "1 1\n" );
	else if ( GateType == EXTRA_GATE_TYPE_INV )
		fprintf( pFile, "0 1\n" );
	else if ( GateType == EXTRA_GATE_TYPE_AND || GateType == EXTRA_GATE_TYPE_NOR )
	{
		for ( v = 0; v < nInputs; v++ )
		{
			if ( GateType == EXTRA_GATE_TYPE_AND )
			{
				if ( Polars && Polars[v] == 0 )
					fprintf( pFile, "0" );
				else
					fprintf( pFile, "1" );
			}
			else
			{
				if ( Polars && Polars[v] == 0 )
					fprintf( pFile, "1" );
				else
					fprintf( pFile, "0" );
			}
		}
		fprintf( pFile, " 1\n" );
	}
	else if ( GateType == EXTRA_GATE_TYPE_OR || GateType == EXTRA_GATE_TYPE_NAND )
	{
		for ( v = 0; v < nInputs; v++ )
		{
			for ( i = 0; i < nInputs; i++ )
				if ( i == v )
				{
					if ( GateType == EXTRA_GATE_TYPE_OR )
					{
						if ( Polars && Polars[v] == 0 )
							fprintf( pFile, "0" );
						else
							fprintf( pFile, "1" );
					}
					else
					{
						if ( Polars && Polars[v] == 0 )
							fprintf( pFile, "1" );
						else
							fprintf( pFile, "0" );
					}
				}
				else
					fprintf( pFile, "-" );
			fprintf( pFile, " 1\n" );
		}
	}
	else if ( GateType == EXTRA_GATE_TYPE_EXOR || GateType == EXTRA_GATE_TYPE_NEXOR )
	{
		unsigned m, nMints;
		int nOnes;

		// write the cubes
		nMints = (1<<nInputs);
		for ( m = 0; m < nMints; m++ )
		{
			// count the number of ones
			nOnes = 0;
			for ( v = 0; v < nInputs; v++ )
				if ( m & (1<<v) )
					nOnes++;
			// if the number is ODD, write this minterm
			if (  (GateType == EXTRA_GATE_TYPE_EXOR  &&  (nOnes & 1)) || 
				  (GateType == EXTRA_GATE_TYPE_NEXOR && !(nOnes & 1)) ) 
			{
				Extra_PrintBinary( pFile, &m, nInputs );
				fprintf( pFile, " 1\n" );
			}
		}
	}
	else if ( GateType == EXTRA_GATE_TYPE_CROSS )
	{ // write the cross composed of 1's - to denote some strange gate
		for ( v = 0; v < nInputs; v++ )
		{
			for ( i = 0; i < nInputs; i++ )
				if ( i == v || i == nInputs-1-v )
					fprintf( pFile, "1" );
				else
					fprintf( pFile, "-" );
			fprintf( pFile, " 1\n" );
		}
	}
	else
	{
		assert( 0 );
	}
}


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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Extra_WriteBlifGateCascade( FILE * pFile, char * pInputNames[], int Polars[], int nInputs, char * pOutputName, int GateType )
{
	int SigNum;
	int fComp0;

	assert( nInputs > 0 );
	if ( nInputs == 1 )
	{
		fprintf( pFile, ".names %s %s\n", pInputNames[0], pOutputName );
		fComp0 = (Polars && Polars[0] == 0)? 1: 0;
		if ( GateType == EXTRA_GATE_TYPE_AND )
			fprintf( pFile, "%d 1\n", 1^fComp0 );
		else if ( GateType == EXTRA_GATE_TYPE_NOR )
			fprintf( pFile, "%d 1\n", 0^fComp0 );
		else if ( GateType == EXTRA_GATE_TYPE_OR )
			fprintf( pFile, "%d 1\n", 1^fComp0 );
		else if ( GateType == EXTRA_GATE_TYPE_NAND )
			fprintf( pFile, "%d 1\n", 0^fComp0 );
		else if ( GateType == EXTRA_GATE_TYPE_EXOR )
			fprintf( pFile, "1 1\n" );
		else if ( GateType == EXTRA_GATE_TYPE_NEXOR )
			fprintf( pFile, "0 1\n" );
		return;
	}
	SigNum = 1;
	extraWriteBlifGateCascade( pFile, pInputNames, Polars, nInputs, pOutputName, GateType, 0, &SigNum );
}

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

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


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

  Synopsis    [ZDD traversal function, which write ZDD into the BLIF file.]

  Description [Enumerates the cubes of zCover and writes them into s_pVerValues.
  Upon reaching the bottom level, writes the cube into the FILE.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void 
extraWriteBlifNode( 
  FILE * pFile,        // the output file
  DdManager * dd,      // the DD manager
  DdNode * zCover,     // the ZDD representing the cube cover
  int * pVarMap,       // the mapping of the variable number in the cube into the variable index in the manager
  int nVars,           // the number of variables in the cube
  int levPrev,         // the level from which this function is called
  int * pVarValues )   // the current array of levels
{
	int TopLevel;
	int lev, var;

	if ( zCover == z0 )
		return;
	if ( zCover == z1 )
	{
		// fill in the remaining variables 
		for ( lev = levPrev + 1; lev < dd->sizeZ; lev++ )
			pVarValues[ dd->invpermZ[ lev ] ] = 0;
		// write the cube 
	    for ( var = 0; var < nVars; var++ )
			if      (  pVarValues[ pVarMap[var]*2 ] && !pVarValues[ pVarMap[var]*2+1 ] ) // the value in ZDD is 1 
				fprintf( pFile, "1" );
			else if	( !pVarValues[ pVarMap[var]*2 ] &&  pVarValues[ pVarMap[var]*2+1 ] ) // the value in ZDD is 0
				fprintf( pFile, "0" );
			else if	(  pVarValues[ pVarMap[var]*2 ] &&  pVarValues[ pVarMap[var]*2+1 ] ) // the value in ZDD is wrong
				fprintf( pFile, "@" );
			else
				fprintf( pFile, "-" );
		// write the end of the line
		fprintf( pFile, " 1\n" );
		return;
	}
	else
	{
		// find the level of the top variable 
		TopLevel = dd->permZ[ zCover->index ];

		// fill in the remaining variables 
		for ( lev = levPrev + 1; lev < TopLevel; lev++ )
			pVarValues[ dd->invpermZ[ lev ] ] = 0;

		// fill in this variable 
		// the given var has negative polarity 
		pVarValues[ zCover->index ] = 0;
		// iterate through the else branch
		extraWriteBlifNode( pFile, dd, cuddE(zCover), pVarMap, nVars, TopLevel, pVarValues );
		
		// the given var has positive polarity
		pVarValues[ zCover->index ] = 1;
		// iterate through the then branch
		extraWriteBlifNode( pFile, dd, cuddT(zCover), pVarMap, nVars, TopLevel, pVarValues );
	}
} /* end of extraWriteBlifNode */


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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void extraWriteBlifNodeUsingGates( FILE * pFile, DdManager * dd, DdNode * zCover, char * pInputNames[], char * pOutputName, int fCascade )
{
	char Buffer[100];
	int * pPolars;
	char ** pNamesOr;
	char ** pNamesAnd;
	DdNode * zCoverCur;
	DdNode * zCube, * zTemp;
	int nCubes;
	int c, v;

	if ( cuddIsConstant(zCover) )
	{
		fprintf( pFile, ".names %s\n", pOutputName );
		if ( zCover == z1 )
			fprintf( pFile, " 1\n" );
		return;
	}

	nCubes   = Cudd_zddCount( dd, zCover );
	pNamesOr = ALLOC( char *, nCubes );
	// assign the cube names
	for ( c = 0; c < nCubes; c++ )
	{
		sprintf( Buffer, "%s_c%d", pOutputName, c );
		pNamesOr[c] = util_strsav( Buffer );
	}

	// write the OR gate
	if ( fCascade )
		Extra_WriteBlifGateCascade( pFile, pNamesOr, NULL, nCubes, pOutputName, EXTRA_GATE_TYPE_OR );
	else
		Extra_WriteBlifGate( pFile, pNamesOr, NULL, nCubes, pOutputName, EXTRA_GATE_TYPE_OR );


	// write the cubes
	pNamesAnd = ALLOC( char *, dd->size );
	pPolars   = ALLOC( int, dd->size );
	c = 0;
	zCoverCur = zCover;   Cudd_Ref( zCoverCur );
	while ( zCoverCur != z0 )
	{
		// get the cube
		zCube = Extra_zddSelectOneCube( dd, zCoverCur );  Cudd_Ref( zCube );
		// collect the input names and polarities present in this cube
		v = 0;
		for ( zTemp = zCube; zTemp != z1; zTemp = cuddT(zTemp) )
		{
			pNamesAnd[v] = pInputNames[zTemp->index/2];
			pPolars  [v] = (zTemp->index%2 == 0);
			v++;
		}
		if ( fCascade )
		{
/*
			fprintf( pFile, "\n\n\n" );
			fprintf( stdout, "\n\n\n" );
			Extra_WriteBlifGate( pFile, pNamesAnd, pPolars, v, pNamesOr[c], EXTRA_GATE_TYPE_AND );
			Extra_WriteBlifGate( stdout, pNamesAnd, pPolars, v, pNamesOr[c], EXTRA_GATE_TYPE_AND );
			fprintf( pFile, "\n" );
			fprintf( stdout, "\n" );
if ( strcmp( pNamesOr[c], "[5]_c0" ) == 0 )
{
	int i = 0;
}
			Extra_WriteBlifGateCascade( pFile, pNamesAnd, pPolars, v, pNamesOr[c], EXTRA_GATE_TYPE_AND );
			Extra_WriteBlifGateCascade( stdout, pNamesAnd, pPolars, v, pNamesOr[c], EXTRA_GATE_TYPE_AND );
			fprintf( pFile, "\n\n\n" );
			fprintf( stdout, "\n\n\n" );
*/
			Extra_WriteBlifGateCascade( pFile, pNamesAnd, pPolars, v, pNamesOr[c], EXTRA_GATE_TYPE_AND );
		}
		else
			Extra_WriteBlifGate( pFile, pNamesAnd, pPolars, v, pNamesOr[c], EXTRA_GATE_TYPE_AND );
		
		// substract this cube
		zCoverCur = Cudd_zddDiff( dd, zTemp = zCoverCur, zCube );  Cudd_Ref( zCoverCur );
		Cudd_RecursiveDerefZdd( dd, zTemp );
		Cudd_RecursiveDerefZdd( dd, zCube );
		c++;
	}
	Cudd_RecursiveDerefZdd( dd, zCoverCur );
	for ( c = 0; c < nCubes; c++ )
		free( pNamesOr[c] );
	free( pPolars );
	free( pNamesOr );
	free( pNamesAnd );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void extraWriteBlifGateCascade( FILE * pFile, char * pInputNames[], int Polars[], int nInputs, char * pOutputName, int GateType, int OutputSigNum, int * pSigNum )
{
	int nInputs1, nInputs2;
	int nSigNum1, nSigNum2;
	int fComp0, fComp1;

	assert( nInputs > 1 );
	if ( nInputs == 2 )
	{
		// write the names line
		fprintf( pFile, ".names" );
		// write the first input name
		fprintf( pFile, " %s", pInputNames[0] );
		// write the second input name
		fprintf( pFile, " %s", pInputNames[1] );
		// write the output name
		if ( OutputSigNum == 0 ) // this is the first call 
			fprintf( pFile, " %s\n", pOutputName );
		else
			fprintf( pFile, " %s_%d\n", pOutputName, OutputSigNum );
		// write the gate
		fComp0 = (Polars && Polars[0] == 0)? 1: 0;
		fComp1 = (Polars && Polars[1] == 0)? 1: 0;
		if ( GateType == EXTRA_GATE_TYPE_AND )
			fprintf( pFile, "%d%d 1\n", 1^fComp0, 1^fComp1 );
		else if ( GateType == EXTRA_GATE_TYPE_NOR )
			fprintf( pFile, "%d%d 1\n", 0^fComp0, 0^fComp1 );
		else if ( GateType == EXTRA_GATE_TYPE_OR )
			fprintf( pFile, "%d- 1\n-%d 1\n", 1^fComp0, 1^fComp1 );
		else if ( GateType == EXTRA_GATE_TYPE_NAND )
			fprintf( pFile, "%d- 1\n-%d 1\n", 0^fComp0, 0^fComp1 );
		else if ( GateType == EXTRA_GATE_TYPE_EXOR )
			fprintf( pFile, "01 1\n10 1\n" );
		else if ( GateType == EXTRA_GATE_TYPE_NEXOR )
			fprintf( pFile, "00 1\n11 1\n" );
		else
		{
			assert( 0 );
		}
		return;
	}
	// nInputs > 2

	nInputs1 = (1<<(Extra_Base2Log(nInputs)-1));
	nInputs2 = nInputs - nInputs1;
	assert( nInputs1 > 1 );
	assert( nInputs2 > 0 );
	nSigNum1 = (*pSigNum)++;
	nSigNum2 = (*pSigNum)++;

	// write the names line
	fprintf( pFile, ".names" );
	// write the first input name
	fprintf( pFile, " %s_%d", pOutputName, nSigNum1 );
	// write the second input name
	if ( nInputs2 == 1 )
		fprintf( pFile, " %s", pInputNames[nInputs1] );
	else
		fprintf( pFile, " %s_%d", pOutputName, nSigNum2 );
	// write the output name
	if ( OutputSigNum == 0 ) // this is the first call 
		fprintf( pFile, " %s\n", pOutputName );
	else
		fprintf( pFile, " %s_%d\n", pOutputName, OutputSigNum );
	// write the gate
	fComp0 = 0;
	fComp1 = (nInputs2 == 1 && Polars && Polars[nInputs1] == 0)? 1: 0;
	if ( GateType == EXTRA_GATE_TYPE_AND )
		fprintf( pFile, "%d%d 1\n", 1^fComp0, 1^fComp1 );
	else if ( GateType == EXTRA_GATE_TYPE_NOR )
		fprintf( pFile, "%d%d 1\n", 0^fComp0, 0^fComp1 );
	else if ( GateType == EXTRA_GATE_TYPE_OR )
		fprintf( pFile, "%d- 1\n-%d 1\n", 1^fComp0, 1^fComp1 );
	else if ( GateType == EXTRA_GATE_TYPE_NAND )
		fprintf( pFile, "%d- 1\n-%d 1\n", 0^fComp0, 0^fComp1 );
	else if ( GateType == EXTRA_GATE_TYPE_EXOR )
		fprintf( pFile, "01 1\n10 1\n" );
	else if ( GateType == EXTRA_GATE_TYPE_NEXOR )
		fprintf( pFile, "00 1\n11 1\n" );
	else
	{
		assert( 0 );
	}

	// call recursively for the first part
	extraWriteBlifGateCascade( pFile, pInputNames, Polars, nInputs1, pOutputName, GateType, nSigNum1, pSigNum );
	if ( nInputs2 > 1 )
		extraWriteBlifGateCascade( pFile, pInputNames + nInputs1, Polars? Polars + nInputs1: Polars, nInputs2, pOutputName, GateType, nSigNum2, pSigNum );
}