casCore.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#include "bdd/extrab/extraBdd.h"
#include "cas.h"

Include dependency graph for casCore.c:

Go to the source code of this file.

Macros
#define	PRD(p)
	static varibles ///
#define	PRB_(f)
#define	PRK(f, n)
#define	PRK2(f, g, n)

Functions
ABC_NAMESPACE_IMPL_START DdNode *	GetSingleOutputFunction (DdManager *dd, DdNode **pbOuts, int nOuts, DdNode **pbVarsEnc, int nVarsEnc, int fVerbose)
	static functions ///
DdNode *	GetSingleOutputFunctionRemapped (DdManager *dd, DdNode **pOutputs, int nOuts, DdNode **pbVarsEnc, int nVarsEnc)
	INPUT REMAPPING ///.
DdNode *	GetSingleOutputFunctionRemappedNewDD (DdManager *dd, DdNode **pOutputs, int nOuts, DdManager **DdNew)
int	CreateDecomposedNetwork (DdManager *dd, DdNode *aFunc, char **pNames, int nNames, char *FileName, int nLutSize, int fCheck, int fVerbose)
	EXTERNAL FUNCTIONS ///.
void	WriteSingleOutputFunctionBlif (DdManager *dd, DdNode *aFunc, char **pNames, int nNames, char *FileName)
DdNode *	Cudd_bddTransferPermute (DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
int	Abc_CascadeExperiment (char *pFileGeneric, DdManager *dd, DdNode **pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose)
	EXTERNAL FUNCTIONS ///.
int	CompareSupports (int *ptrX, int *ptrY)
int	CompareMinterms (int *ptrX, int *ptrY)
int	GrayCode (int BinCode)
void	WriteDDintoBLIFfile (FILE *pFile, DdNode *Func, char *OutputName, char *Prefix, char **InputNames)
	BLIF WRITING FUNCTIONS ///.
void	WriteDDintoBLIFfileReorder (DdManager *dd, FILE *pFile, DdNode *Func, char *OutputName, char *Prefix, char **InputNames)
DdNode *	cuddBddTransferPermute (DdManager *ddS, DdManager *ddD, DdNode *f, int *Permute)

Macro Definition Documentation

PRB_

#define PRB_

(

f

)

Value:

printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )

Definition at line 59 of file casCore.c.

PRD

#define PRD

(

p

)

Value:

printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 )

static varibles ///

debugging macros ///

Definition at line 58 of file casCore.c.

PRK

#define PRK	(		f,
			n )

Value:

Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )

Definition at line 60 of file casCore.c.

PRK2

#define PRK2	(		f,
			g,
			n )

Value:

Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )

Definition at line 61 of file casCore.c.

Function Documentation

Abc_CascadeExperiment()

int Abc_CascadeExperiment	(	char *	pFileGeneric,
		DdManager *	dd,
		DdNode **	pOutputs,
		int	nInputs,
		int	nOutputs,
		int	nLutSize,
		int	fCheck,
		int	fVerbose )

EXTERNAL FUNCTIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file casCore.c.

{
    int i;
    int nVars = nInputs;
    int nOuts = nOutputs;
    abctime clk1;
 
    int      nVarsEnc;              // the number of additional variables to encode outputs
    DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
 
    int      nNames;               // the total number of all inputs
    char *   pNames[MAXINPUTS];     // the temporary storage for the input (and output encoding) names
 
    DdNode * aFunc;                 // the encoded 0-1 BDD containing all the outputs
 
    char FileNameIni[100];
    char FileNameFin[100];
    char Buffer[100];
 
    
//pTable = fopen( "stats.txt", "a+" );
//fprintf( pTable, "%s ", pFileGeneric );
//fprintf( pTable, "%d ", nVars );
//fprintf( pTable, "%d ", nOuts );
 
 
    // assign the file names
    strcpy( FileNameIni, pFileGeneric );
    strcat( FileNameIni, "_ENC.blif" );
 
    strcpy( FileNameFin, pFileGeneric );
    strcat( FileNameFin, "_LUT.blif" );
 
 
    // create the variables to encode the outputs
    nVarsEnc = Abc_Base2Log( nOuts );
    for ( i = 0; i < nVarsEnc; i++ )
        pbVarsEnc[i] = Cudd_bddNewVarAtLevel( dd, i );
 
 
    // store the input names
    nNames  = nVars + nVarsEnc;
    for ( i = 0; i < nVars; i++ )
    {
//      pNames[i] = Extra_UtilStrsav( pFunc->pInputNames[i] );
        sprintf( Buffer, "pi%03d", i );
        pNames[i] = Extra_UtilStrsav( Buffer );
    }
    // set the encoding variable name
    for ( ; i < nNames; i++ )
    {       
        sprintf( Buffer, "OutEnc_%02d", i-nVars );
        pNames[i] = Extra_UtilStrsav( Buffer );
    }
 
 
    // print the variable order
//  printf( "\n" );
//  printf( "Variable order is: " );
//  for ( i = 0; i < dd->size; i++ )
//      printf( " %d", dd->invperm[i] );
//  printf( "\n" );
 
    // derive the single-output function
    clk1 = Abc_Clock();
    aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose );  Cudd_Ref( aFunc );
//  aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
//  if ( fVerbose )
//  printf( "Single-output function computation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
 
//fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) );
 
    // dispose of the multiple-output function
//  Extra_Dissolve( pFunc );
 
    // reorder the single output function
//    if ( fVerbose )
//  printf( "Reordering variables...\n");
    clk1 = Abc_Clock();
//  if ( fVerbose )
//  printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) );
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1);
    Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
    Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
    if ( fVerbose )
    printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) );
    if ( fVerbose )
    printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
//  printf( "\n" );
//  printf( "Variable order is: " );
//  for ( i = 0; i < dd->size; i++ )
//      printf( " %d", dd->invperm[i] );
//  printf( "\n" );
//fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) );
 
    // write the single-output function into BLIF for verification
    clk1 = Abc_Clock();
    if ( fCheck )
    WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
//    if ( fVerbose )
//  printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
 
/*
    // verification of single output function
    clk1 = Abc_Clock();
    {
        BFunc g_Func;
        DdNode * aRes;
 
        g_Func.dd = dd;
        g_Func.FileInput = Extra_UtilStrsav(FileNameIni);
 
        if ( Extra_ReadFile( &g_Func ) == 0 )
        {
            printf( "\nSomething did not work out while reading the input file for verification\n");
            Extra_Dissolve( &g_Func );
            return;
        } 
 
        aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] );  Cudd_Ref( aRes );
 
        if ( aRes != aFunc )
            printf( "\nVerification FAILED!\n");
        else
            printf( "\nVerification okay!\n");
        
        Cudd_RecursiveDeref( dd, aRes );
 
        // delocate
        Extra_Dissolve( &g_Func );
    }
    printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
*/
 
    if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) )
        return 0;
 
/*
    // verification of the decomposed LUT network
    clk1 = Abc_Clock();
    {
        BFunc g_Func;
        DdNode * aRes;
 
        g_Func.dd = dd;
        g_Func.FileInput = Extra_UtilStrsav(FileNameFin);
 
        if ( Extra_ReadFile( &g_Func ) == 0 )
        {
            printf( "\nSomething did not work out while reading the input file for verification\n");
            Extra_Dissolve( &g_Func );
            return;
        } 
 
        aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] );  Cudd_Ref( aRes );
 
        if ( aRes != aFunc )
            printf( "\nFinal verification FAILED!\n");
        else
            printf( "\nFinal verification okay!\n");
        
        Cudd_RecursiveDeref( dd, aRes );
 
        // delocate 
        Extra_Dissolve( &g_Func );
    }
    printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
*/
 
    // verify the results
    if ( fCheck )
    {
        char Command[300];
        sprintf( Command, "cec %s %s", FileNameIni, FileNameFin );
        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
    }
 
    Cudd_RecursiveDeref( dd, aFunc );
 
    // release the names
    for ( i = 0; i < nNames; i++ )
        ABC_FREE( pNames[i] );
 
 
//fprintf( pTable, "\n" );
//fclose( pTable );
 
    return 1;
}

Here is the call graph for this function:

CompareMinterms()

int CompareMinterms	(	int *	ptrX,
		int *	ptrY )

Definition at line 474 of file casCore.c.

{
    return ( s_MintOnes[*ptrY] - s_MintOnes[*ptrX] );
}

CompareSupports()

int CompareSupports	(	int *	ptrX,
		int *	ptrY )

Definition at line 465 of file casCore.c.

{
    return ( s_SuppSize[*ptrY] - s_SuppSize[*ptrX] );
}

Here is the caller graph for this function:

CreateDecomposedNetwork()

int CreateDecomposedNetwork ( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose )

extern

EXTERNAL FUNCTIONS ///.

Definition at line 108 of file casDec.c.

{
    static LUT * pLuts[MAXINPUTS];   // the LUT cascade
    static int Profile[MAXINPUTS];   // the profile filled in with the info about the BDD width
    static int Permute[MAXINPUTS];   // the array to store a temporary permutation of variables
 
    LUT * p;               // the current LUT
    int i, v;
 
    DdNode * bCVars[32];   // these are variables for the codes
 
    int nVarsRem;          // the number of remaining variables
    int PrevMulti;         // column multiplicity on the previous level
    int fLastLut;          // flag to signal the last LUT
    int nLuts;
    int nLutsTotal = 0;
    int nLutOutputs = 0;
    int nLutOutputsOrig = 0;
 
    abctime clk1;
 
    s_LutSize = nLutSize;
 
    s_nFuncVars = nNames;
 
    // get the profile
    clk1 = Abc_Clock();
    Extra_ProfileWidth( dd, aFunc, Profile, -1 );
 
 
//  for ( v = 0; v < nNames; v++ )
//      printf( "Level = %2d, Width = %2d\n", v+1, Profile[v] );
 
 
//printf( "\n" );
 
    // mark-up the LUTs
    // assuming that the manager has exactly nNames vars (new vars have not been introduced yet)
    nVarsRem  = nNames;     // the number of remaining variables
    PrevMulti = 0;          // column multiplicity on the previous level
    fLastLut  = 0;
    nLuts     = 0;
    do
    {
        p = (LUT*) ABC_ALLOC( char, sizeof(LUT) );
        memset( p, 0, sizeof(LUT) );
 
        if ( nVarsRem + PrevMulti <= s_LutSize ) // this is the last LUT
        {
            p->nIns   = nVarsRem + PrevMulti;
            p->nInsP  = PrevMulti;
            p->nCols  = 2;
            p->nMulti = 1;
            p->Level  = nNames-nVarsRem;
 
            nVarsRem  = 0;
            PrevMulti = 1;
 
            fLastLut  = 1;
        }
        else // this is not the last LUT
        {
            p->nIns   = s_LutSize;
            p->nInsP  = PrevMulti;
            p->nCols  = Profile[nNames-(nVarsRem-(s_LutSize-PrevMulti))];
            p->nMulti = Abc_Base2Log(p->nCols);
            p->Level  = nNames-nVarsRem;
 
            nVarsRem  = nVarsRem-(s_LutSize-PrevMulti);
            PrevMulti = p->nMulti;
        }
        
        if ( p->nMulti >= s_LutSize )
        {
            printf( "The LUT size is too small\n" );
            return 0;
        }
 
        nLutOutputsOrig += p->nMulti;
 
 
//if ( fVerbose )
//printf( "Stage %2d: In = %3d, InP = %3d, Cols = %5d, Multi = %2d, Level = %2d\n", 
//       nLuts+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->Level );
 
 
        // there should be as many columns, codes, and nodes, as there are columns on this level
        p->pbCols  = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
        p->pbCodes = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
        p->paNodes = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
 
        pLuts[nLuts] = p;
        nLuts++;
    }
    while ( !fLastLut );
 
 
//if ( fVerbose )
//printf( "The number of cascades = %d\n", nLuts );
 
 
//fprintf( pTable, "%d ", nLuts );
 
 
    // add the new variables at the bottom
    for ( i = 0; i < s_LutSize; i++ )
        bCVars[i] = Cudd_bddNewVar(dd);
 
    // for each LUT - assign the LUT and encode the columns
    s_EncodingTime = 0;
    for ( i = 0; i < nLuts; i++ )
    {
        int RetValue;
        DdNode * bVars[32];    
        int nVars;
        DdNode * bVarsInCube;
        DdNode * bVarsCCube;
        DdNode * bVarsCube;
        int CutLevel;
 
        p = pLuts[i];
 
        // compute the columns of this LUT starting from the given set of nodes with the given codes
        // (these codes have been remapped to depend on the topmost variables in the manager)
        // for the first LUT, start with the constant 1 BDD
        CutLevel = p->Level + p->nIns - p->nInsP;
        if ( i == 0 )
            RetValue = Extra_bddNodePathsUnderCutArray( 
                            dd, &aFunc, &(b1), 1, 
                            p->paNodes, p->pbCols, CutLevel );
        else
            RetValue = Extra_bddNodePathsUnderCutArray( 
                            dd, pLuts[i-1]->paNodes, pLuts[i-1]->pbCodes, pLuts[i-1]->nCols, 
                            p->paNodes, p->pbCols, CutLevel );
        assert( RetValue == p->nCols );
        // at this point, we have filled out p->paNodes[] and p->pbCols[] of this LUT
        // pLuts[i-1]->paNodes depended on normal vars
        // pLuts[i-1]->pbCodes depended on the topmost variables 
        // the resulting p->paNodes depend on normal ADD nodes
        // the resulting p->pbCols depend on normal vars and topmost variables in the manager
 
        // perform the encoding
 
        // create the cube of these variables
        // collect the topmost variables of the manager
        nVars = p->nInsP;
        for ( v = 0; v < nVars; v++ )
            bVars[v] = dd->vars[ dd->invperm[v] ];
        bVarsCCube  = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 );    Cudd_Ref( bVarsCCube );
 
        // collect the primary input variables involved in this LUT
        nVars = p->nIns - p->nInsP;
        for ( v = 0; v < nVars; v++ )
            bVars[v] = dd->vars[ dd->invperm[p->Level+v] ];
        bVarsInCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 );    Cudd_Ref( bVarsInCube );
 
        // get the cube
        bVarsCube   = Cudd_bddAnd( dd, bVarsInCube, bVarsCCube );              Cudd_Ref( bVarsCube );
        Cudd_RecursiveDeref( dd, bVarsInCube );
        Cudd_RecursiveDeref( dd, bVarsCCube );
 
        // get the encoding relation
        if ( i == nLuts -1 )
        {
            DdNode * bVar;
            assert( p->nMulti == 1 );
            assert( p->nCols == 2 );
            assert( Cudd_IsConstant( p->paNodes[0] ) );
            assert( Cudd_IsConstant( p->paNodes[1] ) );
 
            bVar = ( p->paNodes[0] == a1 )? bCVars[0]: Cudd_Not( bCVars[0] );
            p->bRelation = Cudd_bddIte( dd, bVar, p->pbCols[0], p->pbCols[1] );  Cudd_Ref( p->bRelation );
        }
        else
        {
            abctime clk2 = Abc_Clock();
//          p->bRelation = PerformTheEncoding( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple );  Cudd_Ref( p->bRelation );
            p->bRelation = Extra_bddEncodingNonStrict( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple );  Cudd_Ref( p->bRelation );
            s_EncodingTime += Abc_Clock() - clk2;
        }
 
        // update the number of LUT outputs
        nLutOutputs += (p->nMulti - p->nSimple);
        nLutsTotal += p->nMulti;
 
//if ( fVerbose )
//printf( "Stage %2d: Simple = %d\n", i+1, p->nSimple );
 
if ( fVerbose )
printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d  Level = %3d\n", 
       i+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->nSimple, p->Level );
 
        // get the codes from the relation (these are not necessarily cubes)
        {
            int c;
            for ( c = 0; c < p->nCols; c++ )
            {
                p->pbCodes[c] = Cudd_bddAndAbstract( dd, p->bRelation, p->pbCols[c], bVarsCube ); Cudd_Ref( p->pbCodes[c] );
            }
        }
 
        Cudd_RecursiveDeref( dd, bVarsCube );
 
        // remap the codes to depend on the topmost varibles of the manager
        // useful as a preparation for the next step
        {
            DdNode ** pbTemp;
            int k, v;
 
            pbTemp = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
 
            // create the identical permutation
            for ( v = 0; v < dd->size; v++ )
                Permute[v] = v;
 
            // use the topmost variables of the manager 
            // to represent the previous level codes
            for ( v = 0; v < p->nMulti; v++ )
                Permute[bCVars[v]->index] = dd->invperm[v];
 
            Extra_bddPermuteArray( dd, p->pbCodes, pbTemp, p->nCols, Permute );
            // the array pbTemp comes already referenced
 
            // deref the old codes and assign the new ones
            for ( k = 0; k < p->nCols; k++ )
            {
                Cudd_RecursiveDeref( dd, p->pbCodes[k] );
                p->pbCodes[k] = pbTemp[k];
            }
            ABC_FREE( pbTemp );
        }
    } 
    if ( fVerbose )
    printf( "LUTs: Total = %5d. Final = %5d. Simple = %5d. (%6.2f %%)  ", 
        nLutsTotal, nLutOutputs, nLutsTotal-nLutOutputs, 100.0*(nLutsTotal-nLutOutputs)/nLutsTotal );
    if ( fVerbose )
    printf( "Memory = %6.2f MB\n", 1.0*nLutOutputs*(1<<nLutSize)/(1<<20) );
//  printf( "\n" );
 
//fprintf( pTable, "%d ", nLutOutputsOrig );
//fprintf( pTable, "%d ", nLutOutputs );
 
    if ( fVerbose )
    {
    printf( "Pure decomposition time   = %.2f sec\n", (float)(Abc_Clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
    printf( "Encoding time             = %.2f sec\n", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
//  printf( "Encoding search time      = %.2f sec\n", (float)(s_EncSearchTime)/(float)(CLOCKS_PER_SEC) );
//  printf( "Encoding compute time     = %.2f sec\n", (float)(s_EncComputeTime)/(float)(CLOCKS_PER_SEC) );
    }
 
 
//fprintf( pTable, "%.2f ", (float)(s_ReadingTime)/(float)(CLOCKS_PER_SEC) );
//fprintf( pTable, "%.2f ", (float)(Abc_Clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
//fprintf( pTable, "%.2f ", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
//fprintf( pTable, "%.2f ", (float)(s_RemappingTime)/(float)(CLOCKS_PER_SEC) );
 
 
    // write LUTs into the BLIF file
    clk1 = Abc_Clock();
    if ( fCheck )
    {
        FILE * pFile;
        // start the file
        pFile = fopen( FileName, "w" );
        fprintf( pFile, ".model %s\n", FileName );
 
        fprintf( pFile, ".inputs" );
        for ( i = 0; i < nNames; i++ )
            fprintf( pFile, " %s", pNames[i] );
        fprintf( pFile, "\n" );
        fprintf( pFile, ".outputs F" );
        fprintf( pFile, "\n" );
 
        // write the DD into the file
        WriteLUTSintoBLIFfile( pFile, dd, pLuts, nLuts, bCVars, pNames, nNames, FileName );
 
        fprintf( pFile, ".end\n" );
        fclose( pFile );
        if ( fVerbose )
        printf( "Output file writing time  = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
    }
 
 
    // updo the LUT cascade
    for ( i = 0; i < nLuts; i++ )
    {
        p = pLuts[i];
        for ( v = 0; v < p->nCols; v++ )
        {
            Cudd_RecursiveDeref( dd, p->pbCols[v] );
            Cudd_RecursiveDeref( dd, p->pbCodes[v] );
            Cudd_RecursiveDeref( dd, p->paNodes[v] );
        }
        Cudd_RecursiveDeref( dd, p->bRelation );
 
        ABC_FREE( p->pbCols );
        ABC_FREE( p->pbCodes );
        ABC_FREE( p->paNodes );
        ABC_FREE( p );
    }
 
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cudd_bddTransferPermute()

DdNode * Cudd_bddTransferPermute	(	DdManager *	ddSource,
		DdManager *	ddDestination,
		DdNode *	f,
		int *	Permute )

Function********************************************************************

Synopsis [Convert a BDD from a manager to another one.]

Description [Convert a BDD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise. The i-th entry in the array Permute tells what is the index of the i-th variable from the old manager in the new manager.]

SideEffects [None]

SeeAlso []

Definition at line 1082 of file casCore.c.

{
    DdNode *res;
    do
    {
        ddDestination->reordered = 0;
        res = cuddBddTransferPermute( ddSource, ddDestination, f, Permute );
    }
    while ( ddDestination->reordered == 1 );
    return ( res );
 
}                               /* end of Cudd_bddTransferPermute */

Here is the call graph for this function:

Here is the caller graph for this function:

cuddBddTransferPermute()

DdNode * cuddBddTransferPermute	(	DdManager *	ddS,
		DdManager *	ddD,
		DdNode *	f,
		int *	Permute )

Function********************************************************************

Synopsis [Convert a BDD from a manager to another one.]

Description [Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddTransferPermute]

Definition at line 1116 of file casCore.c.

{
    DdNode *res;
    st__table *table = NULL;
    st__generator *gen = NULL;
    DdNode *key, *value;
 
    table = st__init_table( st__ptrcmp, st__ptrhash );
    if ( table == NULL )
        goto failure;
    res = cuddBddTransferPermuteRecur( ddS, ddD, f, table, Permute );
    if ( res != NULL )
        cuddRef( res );
 
    /* Dereference all elements in the table and dispose of the table.
       ** This must be done also if res is NULL to avoid leaks in case of
       ** reordering. */
    gen = st__init_gen( table );
    if ( gen == NULL )
        goto failure;
    while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
    {
        Cudd_RecursiveDeref( ddD, value );
    }
    st__free_gen( gen );
    gen = NULL;
    st__free_table( table );
    table = NULL;
 
    if ( res != NULL )
        cuddDeref( res );
    return ( res );
 
  failure:
    if ( table != NULL )
        st__free_table( table );
    if ( gen != NULL )
        st__free_gen( gen );
    return ( NULL );
 
}                               /* end of cuddBddTransferPermute */

Here is the call graph for this function:

Here is the caller graph for this function:

GetSingleOutputFunction()

DdNode * GetSingleOutputFunction	(	DdManager *	dd,
		DdNode **	pbOuts,
		int	nOuts,
		DdNode **	pbVarsEnc,
		int	nVarsEnc,
		int	fVerbose )

static functions ///

CFile****************************************************************

FileName [casCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]

Synopsis [Entrance into the implementation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Spring 2002.]

Revision [

Id

casCore.c,v 1.0 2002/01/01 00:00:00 alanmi Exp

]

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 496 of file casCore.c.

{
    int i;
    DdNode * bResult, * aResult;
    DdNode * bCube, * bTemp, * bProd;
 
    int Order[MAXOUTPUTS];
//  int OrderMint[MAXOUTPUTS];
 
    // sort the output according to their support size
    for ( i = 0; i < nOuts; i++ )
    {
        s_SuppSize[i] = Cudd_SupportSize( dd, pbOuts[i] );
//      s_MintOnes[i] = BitCount8[i];
        Order[i]      = i;
//      OrderMint[i]  = i;
    }
    
    // order the outputs
    qsort( (void*)Order,     (size_t)nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareSupports );
    // order the outputs
//  qsort( (void*)OrderMint, (size_t)nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareMinterms );
 
 
    bResult = b0;   Cudd_Ref( bResult );
    for ( i = 0; i < nOuts; i++ )
    {
//      bCube   = Cudd_bddBitsToCube( dd, OrderMint[i], nVarsEnc, pbVarsEnc );   Cudd_Ref( bCube );
//      bProd   = Cudd_bddAnd( dd, bCube, pbOuts[Order[nOuts-1-i]] );         Cudd_Ref( bProd );
        bCube   = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc, 1 );   Cudd_Ref( bCube );
        bProd   = Cudd_bddAnd( dd, bCube, pbOuts[Order[i]] );         Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bCube );
 
        bResult = Cudd_bddOr( dd, bProd, bTemp = bResult );           Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }
 
    // convert to the ADD
if ( fVerbose )
printf( "Single BDD size = %6d nodes\n", Cudd_DagSize(bResult) );
    aResult = Cudd_BddToAdd( dd, bResult );  Cudd_Ref( aResult );
    Cudd_RecursiveDeref( dd, bResult );
if ( fVerbose )
printf( "MTBDD           = %6d nodes\n", Cudd_DagSize(aResult) );
    Cudd_Deref( aResult );
    return aResult;
}

Here is the call graph for this function:

Here is the caller graph for this function:

GetSingleOutputFunctionRemapped()

DdNode * GetSingleOutputFunctionRemapped	(	DdManager *	dd,
		DdNode **	pOutputs,
		int	nOuts,
		DdNode **	pbVarsEnc,
		int	nVarsEnc )

INPUT REMAPPING ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 590 of file casCore.c.

{
    static int Permute[MAXINPUTS];
    static DdNode * pRemapped[MAXOUTPUTS];
 
    DdNode * bSupp, * bTemp;
    int i, Counter;
    DdNode * bFunc;
    DdNode * aFunc;
 
    Cudd_AutodynDisable(dd);
 
    // perform the remapping
    for ( i = 0; i < nOuts; i++ )
    {
        // get support
        bSupp = Cudd_Support( dd, pOutputs[i] );    Cudd_Ref( bSupp );
 
        // create the variable map
        Counter = 0;
        for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
            Permute[bTemp->index] = Counter++;
 
        // transfer the BDD and remap it
        pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute );  Cudd_Ref( pRemapped[i] );
 
        // remove support
        Cudd_RecursiveDeref( dd, bSupp );
    }
    
    // perform the encoding
    bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc );   Cudd_Ref( bFunc );
 
    // convert to ADD
    aFunc = Cudd_BddToAdd( dd, bFunc );  Cudd_Ref( aFunc );
    Cudd_RecursiveDeref( dd, bFunc );
 
    // deref the intermediate results
    for ( i = 0; i < nOuts; i++ )
        Cudd_RecursiveDeref( dd, pRemapped[i] );
 
    Cudd_Deref( aFunc );
    return aFunc;
}

Here is the call graph for this function:

GetSingleOutputFunctionRemappedNewDD()

DdNode * GetSingleOutputFunctionRemappedNewDD	(	DdManager *	dd,
		DdNode **	pOutputs,
		int	nOuts,
		DdManager **	DdNew )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 648 of file casCore.c.

{
    static int Permute[MAXINPUTS];
    static DdNode * pRemapped[MAXOUTPUTS];
 
    static DdNode * pbVarsEnc[MAXINPUTS];
    int nVarsEnc;
 
    DdManager * ddnew;
 
    DdNode * bSupp, * bTemp;
    int i, v, Counter;
    DdNode * bFunc;
 
    // these are in the new manager
    DdNode * bFuncNew;
    DdNode * aFuncNew;
 
    int nVarsMax = 0;
 
    // perform the remapping and write the DDs into the new manager
    for ( i = 0; i < nOuts; i++ )
    {
        // get support
        bSupp = Cudd_Support( dd, pOutputs[i] );    Cudd_Ref( bSupp );
 
        // create the variable map
        // to remap the DD into the upper part of the manager
        Counter = 0;
        for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
            Permute[bTemp->index] = dd->invperm[Counter++];
 
        // transfer the BDD and remap it
        pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute );  Cudd_Ref( pRemapped[i] );
 
        // remove support
        Cudd_RecursiveDeref( dd, bSupp );
 
 
        // determine the largest support size
        if ( nVarsMax < Counter )
            nVarsMax = Counter;
    }
    
    // select the encoding variables to follow immediately after the original variables
    nVarsEnc = Abc_Base2Log(nOuts);
/*
    for ( v = 0; v < nVarsEnc; v++ )
        if ( nVarsMax + v < dd->size )
            pbVarsEnc[v] = dd->var[ dd->invperm[nVarsMax+v] ];
        else
            pbVarsEnc[v] = Cudd_bddNewVar( dd );
*/
    // create the new variables on top of the manager
    for ( v = 0; v < nVarsEnc; v++ )
        pbVarsEnc[v] = Cudd_bddNewVarAtLevel( dd, v );
 
//fprintf( pTable, "%d ", Cudd_SharingSize( pRemapped, nOuts ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pRemapped, nOuts) );
 
 
    // perform the encoding
    bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc );   Cudd_Ref( bFunc );
 
 
    // find the cross-manager permutation
    // the variable from the level v in the old manager 
    // should become a variable number v in the new manager
    for ( v = 0; v < nVarsMax + nVarsEnc; v++ )
        Permute[dd->invperm[v]] = v;
 

    // start the new manager
    ddnew = Cudd_Init( nVarsMax + nVarsEnc, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
//  Cudd_AutodynDisable(ddnew);
    Cudd_AutodynEnable(dd, CUDD_REORDER_SYMM_SIFT);
 
    // transfer it to the new manager
    bFuncNew = Cudd_bddTransferPermute( dd, ddnew, bFunc, Permute );      Cudd_Ref( bFuncNew );
 
 
    // deref the intermediate results in the old manager
    Cudd_RecursiveDeref( dd, bFunc );
    for ( i = 0; i < nOuts; i++ )
        Cudd_RecursiveDeref( dd, pRemapped[i] );
 

    // convert to ADD in the new manager
    aFuncNew = Cudd_BddToAdd( ddnew, bFuncNew );  Cudd_Ref( aFuncNew );
    Cudd_RecursiveDeref( ddnew, bFuncNew );
 
    // return the manager
    *DdNew = ddnew;
 
    Cudd_Deref( aFuncNew );
    return aFuncNew;
}

Here is the call graph for this function:

GrayCode()

int GrayCode

(

int

BinCode

)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file casCore.c.

{ 
  return BinCode ^ ( BinCode >> 1 );
}

Here is the caller graph for this function:

WriteDDintoBLIFfile()

void WriteDDintoBLIFfile	(	FILE *	pFile,
		DdNode *	Func,
		char *	OutputName,
		char *	Prefix,
		char **	InputNames )

BLIF WRITING FUNCTIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 803 of file casCore.c.

{
    int i;
    st__table * visited;
    st__generator * gen = NULL;
    long refAddr, diff, mask;
    DdNode * Node, * Else, * ElseR, * Then;
 
    /* Initialize symbol table for visited nodes. */
    visited = st__init_table( st__ptrcmp, st__ptrhash );
 
    /* Collect all the nodes of this DD in the symbol table. */
    cuddCollectNodes( Cudd_Regular(Func), visited );
 
    /* Find how many most significant hex digits are identical
       ** in the addresses of all the nodes. Build a mask based
       ** on this knowledge, so that digits that carry no information
       ** will not be printed. This is done in two steps.
       **  1. We scan the symbol table to find the bits that differ
       **     in at least 2 addresses.
       **  2. We choose one of the possible masks. There are 8 possible
       **     masks for 32-bit integer, and 16 possible masks for 64-bit
       **     integers.
     */
 
    /* Find the bits that are different. */
    refAddr = ( long )Cudd_Regular(Func);
    diff = 0;
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
    {
        diff |= refAddr ^ ( long ) Node;
    }
    st__free_gen( gen );
    gen = NULL;
 
    /* Choose the mask. */
    for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 )
    {
        mask = ( 1 << i ) - 1;
        if ( diff <= mask )
            break;
    }
 
 
    // write the buffer for the output
    fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(Func) ) / sizeof(DdNode), OutputName ); 
    fprintf( pFile, "%s 1\n", (Cudd_IsComplement(Func))? "0": "1" );
 
 
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
    {
        if ( Node->index == CUDD_MAXINDEX )
        {
            // write the terminal node
            fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
            fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" );
            continue;
        }
 
        Else  = cuddE(Node);
        ElseR = Cudd_Regular(Else);
        Then  = cuddT(Node);
 
        assert( InputNames[Node->index] );
        if ( Else == ElseR )
        { // no inverter
            fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index],                           
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );
        }
        else
        { // inverter
            int * pSlot;
            fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index],                         
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );
 
            // if the inverter is written, skip
            if ( ! st__find( visited, (char *)ElseR, (char ***)&pSlot ) )
                assert( 0 );
            if ( *pSlot )
                continue;
            *pSlot = 1;
 
            fprintf( pFile, ".names %s%lx %s%lx_i\n",  
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode)   );
            fprintf( pFile, "0 1\n" );
        }
    }
    st__free_gen( gen );
    gen = NULL;
    st__free_table( visited );
}

Here is the call graph for this function:

Here is the caller graph for this function:

WriteDDintoBLIFfileReorder()

void WriteDDintoBLIFfileReorder	(	DdManager *	dd,
		FILE *	pFile,
		DdNode *	Func,
		char *	OutputName,
		char *	Prefix,
		char **	InputNames )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 928 of file casCore.c.

{
    int i;
    st__table * visited;
    st__generator * gen = NULL;
    long refAddr, diff, mask;
    DdNode * Node, * Else, * ElseR, * Then;
 

    DdNode * bFmin;
    abctime clk1;
 
    if ( s_ddmin == NULL )
        s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
 
    clk1 = Abc_Clock();
    bFmin = Cudd_bddTransfer( dd, s_ddmin, Func );  Cudd_Ref( bFmin );
 
    // reorder
    printf( "Nodes before = %d.   ", Cudd_DagSize(bFmin) ); 
    Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT_CONV,1);
    printf( "Nodes after  = %d.  \n", Cudd_DagSize(bFmin) ); 
 
 
 
    /* Initialize symbol table for visited nodes. */
    visited = st__init_table( st__ptrcmp, st__ptrhash );
 
    /* Collect all the nodes of this DD in the symbol table. */
    cuddCollectNodes( Cudd_Regular(bFmin), visited );
 
    /* Find how many most significant hex digits are identical
       ** in the addresses of all the nodes. Build a mask based
       ** on this knowledge, so that digits that carry no information
       ** will not be printed. This is done in two steps.
       **  1. We scan the symbol table to find the bits that differ
       **     in at least 2 addresses.
       **  2. We choose one of the possible masks. There are 8 possible
       **     masks for 32-bit integer, and 16 possible masks for 64-bit
       **     integers.
     */
 
    /* Find the bits that are different. */
    refAddr = ( long )Cudd_Regular(bFmin);
    diff = 0;
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
    {
        diff |= refAddr ^ ( long ) Node;
    }
    st__free_gen( gen );
    gen = NULL;
 
    /* Choose the mask. */
    for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 )
    {
        mask = ( 1 << i ) - 1;
        if ( diff <= mask )
            break;
    }
 
 
    // write the buffer for the output
    fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(bFmin) ) / sizeof(DdNode), OutputName ); 
    fprintf( pFile, "%s 1\n", (Cudd_IsComplement(bFmin))? "0": "1" );
 
 
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
    {
        if ( Node->index == CUDD_MAXINDEX )
        {
            // write the terminal node
            fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
            fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" );
            continue;
        }
 
        Else  = cuddE(Node);
        ElseR = Cudd_Regular(Else);
        Then  = cuddT(Node);
 
        assert( InputNames[Node->index] );
        if ( Else == ElseR )
        { // no inverter
            fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index],                           
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );
        }
        else
        { // inverter
            fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index],                         
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );
 
            fprintf( pFile, ".names %s%lx %s%lx_i\n",  
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode)   );
            fprintf( pFile, "0 1\n" );
        }
    }
    st__free_gen( gen );
    gen = NULL;
    st__free_table( visited );
 

    Cudd_RecursiveDeref( s_ddmin, bFmin );
}

Here is the call graph for this function:

WriteSingleOutputFunctionBlif()

void WriteSingleOutputFunctionBlif	(	DdManager *	dd,
		DdNode *	aFunc,
		char **	pNames,
		int	nNames,
		char *	FileName )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 769 of file casCore.c.

{
    int i;
    FILE * pFile;
 
    // start the file
    pFile = fopen( FileName, "w" );
    fprintf( pFile, ".model %s\n", FileName );
 
    fprintf( pFile, ".inputs" );
    for ( i = 0; i < nNames; i++ )
        fprintf( pFile, " %s", pNames[i] );
    fprintf( pFile, "\n" );
    fprintf( pFile, ".outputs F" );
    fprintf( pFile, "\n" );
 
    // write the DD into the file
    WriteDDintoBLIFfile( pFile, aFunc, "F", "", pNames );
 
    fprintf( pFile, ".end\n" );
    fclose( pFile );
}

Here is the call graph for this function:

Here is the caller graph for this function: