extrabddkmap.c

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

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

  FileName    [extraBddKmap.c]

  PackageName [extra]

  Synopsis    [Visualizing the K-map.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: extraBddKmap.c,v 1.2 2003/05/27 23:14:38 alanmi Exp $]

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

///            K-map visualization using pseudo graphics             ///
///             Version 1.0. Started - August 20, 2000               ///
///          Version 2.0. Added to EXTRA - July 17, 2001             ///

#include "extra.h"

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

// the maximum number of variables in the Karnaugh Map
#define MAXVARS 20

/*
// single line
#define SINGLE_VERTICAL     (char)179
#define SINGLE_HORIZONTAL   (char)196
#define SINGLE_TOP_LEFT     (char)218
#define SINGLE_TOP_RIGHT    (char)191
#define SINGLE_BOT_LEFT     (char)192
#define SINGLE_BOT_RIGHT    (char)217

// double line
#define DOUBLE_VERTICAL     (char)186
#define DOUBLE_HORIZONTAL   (char)205
#define DOUBLE_TOP_LEFT     (char)201
#define DOUBLE_TOP_RIGHT    (char)187
#define DOUBLE_BOT_LEFT     (char)200
#define DOUBLE_BOT_RIGHT    (char)188

// line intersections
#define SINGLES_CROSS       (char)197
#define DOUBLES_CROSS       (char)206
#define S_HOR_CROSS_D_VER   (char)215
#define S_VER_CROSS_D_HOR   (char)216

// single line joining
#define S_JOINS_S_VER_LEFT  (char)180
#define S_JOINS_S_VER_RIGHT (char)195
#define S_JOINS_S_HOR_TOP   (char)193
#define S_JOINS_S_HOR_BOT   (char)194

// double line joining
#define D_JOINS_D_VER_LEFT  (char)185
#define D_JOINS_D_VER_RIGHT (char)204
#define D_JOINS_D_HOR_TOP   (char)202
#define D_JOINS_D_HOR_BOT   (char)203

// single line joining double line
#define S_JOINS_D_VER_LEFT  (char)182
#define S_JOINS_D_VER_RIGHT (char)199
#define S_JOINS_D_HOR_TOP   (char)207
#define S_JOINS_D_HOR_BOT   (char)209
*/

// single line
#define SINGLE_VERTICAL     (char)'|'
#define SINGLE_HORIZONTAL   (char)'-'
#define SINGLE_TOP_LEFT     (char)'+'
#define SINGLE_TOP_RIGHT    (char)'+'
#define SINGLE_BOT_LEFT     (char)'+'
#define SINGLE_BOT_RIGHT    (char)'+'

// double line
#define DOUBLE_VERTICAL     (char)'|'
#define DOUBLE_HORIZONTAL   (char)'-'
#define DOUBLE_TOP_LEFT     (char)'+'
#define DOUBLE_TOP_RIGHT    (char)'+'
#define DOUBLE_BOT_LEFT     (char)'+'
#define DOUBLE_BOT_RIGHT    (char)'+'

// line intersections
#define SINGLES_CROSS       (char)'+'
#define DOUBLES_CROSS       (char)'+'
#define S_HOR_CROSS_D_VER   (char)'+'
#define S_VER_CROSS_D_HOR   (char)'+'

// single line joining
#define S_JOINS_S_VER_LEFT  (char)'+'
#define S_JOINS_S_VER_RIGHT (char)'+'
#define S_JOINS_S_HOR_TOP   (char)'+'
#define S_JOINS_S_HOR_BOT   (char)'+'

// double line joining
#define D_JOINS_D_VER_LEFT  (char)'+'
#define D_JOINS_D_VER_RIGHT (char)'+'
#define D_JOINS_D_HOR_TOP   (char)'+'
#define D_JOINS_D_HOR_BOT   (char)'+'

// single line joining double line
#define S_JOINS_D_VER_LEFT  (char)'+'
#define S_JOINS_D_VER_RIGHT (char)'+'
#define S_JOINS_D_HOR_TOP   (char)'+'
#define S_JOINS_D_HOR_BOT   (char)'+'


// other symbols
#define UNDERSCORE          (char)95
//#define SYMBOL_ZERO       (char)248   // degree sign
//#define SYMBOL_ZERO         (char)'o'
#define SYMBOL_ZERO         (char)' '
#define SYMBOL_ONE          (char)'1'
#define SYMBOL_DC           (char)'-'
#define SYMBOL_OVERLAP      (char)'?'

// full cells and half cells
#define CELL_FREE           (char)32
#define CELL_FULL           (char)219
#define HALF_UPPER          (char)223
#define HALF_LOWER          (char)220
#define HALF_LEFT           (char)221
#define HALF_RIGHT          (char)222


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

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

// the array of BDD variables used internally
static DdNode * s_XVars[MAXVARS];

// flag which determines where the horizontal variable names are printed
static int fHorizontalVarNamesPrintedAbove = 1;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


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

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

// Oleg's way of generating the gray code
static int GrayCode( int BinCode );
static int BinCode ( int GrayCode );

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


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Prints the K-map of the function.]

  Description [If the pointer to the array of variables XVars is NULL,
               fSuppType determines how the support will be determined.
               fSuppType == 0 -- takes the first nVars of the manager
               fSuppType == 1 -- takes the topmost nVars of the manager
               fSuppType == 2 -- determines support from the on-set and the offset
			   ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void Extra_PrintKMap( 
  FILE * Output,  /* the output stream */
  DdManager * dd, 
  DdNode * OnSet, 
  DdNode * OffSet, 
  int nVars, 
  DdNode ** XVars, 
  int fSuppType, /* the flag which determines how support is computed */
  char ** pVarNames )
{
	int d, p, n, s, v, h, w;
	int nVarsVer;
	int nVarsHor;
	int nCellsVer;
	int nCellsHor;
	int nSkipSpaces;

	// make sure that on-set and off-set do not overlap
	if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
	{
		fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
		return;
	}

	if ( OnSet == b1 )
	{
		fprintf( Output, "PrintKMap(): Constant 1\n" );
		return;
	}
	if ( OffSet == b1 )
	{
		fprintf( Output, "PrintKMap(): Constant 0\n" );
		return;
	}

	if ( nVars < 0 || nVars > MAXVARS )
	{
		fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
		return;
	}

	// determine the support if it is not given
	if ( XVars == NULL )
	{
		if ( fSuppType == 0 )
		{ 	// assume that the support includes the first nVars of the manager
			assert( nVars );
			for ( v = 0; v < nVars; v++ )
				s_XVars[v] = Cudd_bddIthVar( dd, v );
		}
		else if ( fSuppType == 1 )
		{ 	// assume that the support includes the topmost nVars of the manager
			assert( nVars );
			for ( v = 0; v < nVars; v++ )
				s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] );
		}
		else // determine the support
		{
			DdNode * SuppOn, * SuppOff, * Supp;
			int cVars = 0;
			DdNode * TempSupp;

			// determine support
			SuppOn = Cudd_Support( dd, OnSet );		    Cudd_Ref( SuppOn );
			SuppOff = Cudd_Support( dd, OffSet );       Cudd_Ref( SuppOff );
			Supp = Cudd_bddAnd( dd, SuppOn, SuppOff );	Cudd_Ref( Supp );
			Cudd_RecursiveDeref( dd, SuppOn );
			Cudd_RecursiveDeref( dd, SuppOff );

			nVars = Cudd_SupportSize( dd, Supp );
			if ( nVars > MAXVARS )
			{
				fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS );
				Cudd_RecursiveDeref( dd, Supp );
				return;
			}

			// assign variables
			for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ )
				s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index );

			Cudd_RecursiveDeref( dd, TempSupp );
		}
	}
	else
	{
		// copy variables
		assert( XVars );
		for ( v = 0; v < nVars; v++ )
			s_XVars[v] = XVars[v];
	}

	////////////////////////////////////////////////////////////////////
	// determine the Karnaugh map parameters
	nVarsVer = nVars/2;
	nVarsHor = nVars - nVarsVer;
	nCellsVer = (1<<nVarsVer);
	nCellsHor = (1<<nVarsHor);
	nSkipSpaces = nVarsVer + 1;

	////////////////////////////////////////////////////////////////////
	// print variable names
	fprintf( Output, "\n" );
	for ( w = 0; w < nVarsVer; w++ )
        if ( pVarNames == NULL )
		    fprintf( Output, "%c", 'a'+nVarsHor+w );
        else
            fprintf( Output, " %s", pVarNames[nVarsHor+w] );

	if ( fHorizontalVarNamesPrintedAbove )
	{
		fprintf( Output, " \\ " );
		for ( w = 0; w < nVarsHor; w++ )
            if ( pVarNames == NULL )
		        fprintf( Output, "%c", 'a'+w );
            else
                fprintf( Output, "%s ", pVarNames[w] );
	}
	fprintf( Output, "\n" );

	if ( fHorizontalVarNamesPrintedAbove )
	{
		////////////////////////////////////////////////////////////////////
		// print horizontal digits
		for ( d = 0; d < nVarsHor; d++ )
		{
			for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
			for ( n = 0; n < nCellsHor; n++ )
				if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
					fprintf( Output, "1   " );
				else
					fprintf( Output, "0   " );
			fprintf( Output, "\n" );
		}
	}

	////////////////////////////////////////////////////////////////////
	// print the upper line
	for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
	fprintf( Output, "%c", DOUBLE_TOP_LEFT );
	for ( s = 0; s < nCellsHor; s++ )
	{
		fprintf( Output, "%c", DOUBLE_HORIZONTAL );
		fprintf( Output, "%c", DOUBLE_HORIZONTAL );
		fprintf( Output, "%c", DOUBLE_HORIZONTAL );
		if ( s != nCellsHor-1 )
			if ( s&1 )
				fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
			else
				fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
	}
	fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
	fprintf( Output, "\n" );

	////////////////////////////////////////////////////////////////////
	// print the map
	for ( v = 0; v < nCellsVer; v++ )
	{
		DdNode * CubeVerBDD;

		// print horizontal digits
//		for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
		for ( n = 0; n < nVarsVer; n++ )
			if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
				fprintf( Output, "1" );
			else
				fprintf( Output, "0" );
		fprintf( Output, " " );

		// find vertical cube
		CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor );	Cudd_Ref( CubeVerBDD );

		// print text line
		fprintf( Output, "%c", DOUBLE_VERTICAL );
		for ( h = 0; h < nCellsHor; h++ )
		{
			DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;

			fprintf( Output, " " );
//			fprintf( Output, "x" );
			///////////////////////////////////////////////////////////////
			// determine what should be printed
			CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars );	Cudd_Ref( CubeHorBDD );
			Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); 			        Cudd_Ref( Prod );
			Cudd_RecursiveDeref( dd, CubeHorBDD );

			ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );         			Cudd_Ref( ValueOnSet );
			ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );            		Cudd_Ref( ValueOffSet );
			Cudd_RecursiveDeref( dd, Prod );

			if ( ValueOnSet == b1 && ValueOffSet == b0 )
				fprintf( Output, "%c", SYMBOL_ONE );
			else if ( ValueOnSet == b0 && ValueOffSet == b1 )
				fprintf( Output, "%c", SYMBOL_ZERO );
			else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
				fprintf( Output, "%c", SYMBOL_DC );
			else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
				fprintf( Output, "%c", SYMBOL_OVERLAP );
			else
				assert(0);

			Cudd_RecursiveDeref( dd, ValueOnSet );
			Cudd_RecursiveDeref( dd, ValueOffSet );