src/bdd/cas/casDec.c File Reference

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <time.h>
#include "extra.h"
#include "cas.h"

Include dependency graph for casDec.c:

Go to the source code of this file.

Data Structures
struct	LUT
Defines
#define	PRB(f)   printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define	PRK(f, n)   Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
#define	PRK2(f, g, n)   Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
Functions
void	WriteLUTSintoBLIFfile (FILE *pFile, DdManager *dd, LUT **pLuts, int nLuts, DdNode **bCVars, char **pNames, int nNames, char *FileName)
void	WriteDDintoBLIFfile (FILE *pFile, DdNode *Func, char *OutputName, char *Prefix, char **InputNames)
void	WriteDDintoBLIFfileReorder (DdManager *dd, FILE *pFile, DdNode *Func, char *OutputName, char *Prefix, char **InputNames)
int	CreateDecomposedNetwork (DdManager *dd, DdNode *aFunc, char **pNames, int nNames, char *FileName, int nLutSize, int fCheck, int fVerbose)
Variables
static int	s_LutSize = 15
static int	s_nFuncVars
long	s_EncodingTime
long	s_EncSearchTime
long	s_EncComputeTime

---

Define Documentation

#define PRB

(

f

)

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

debugging macros ///

Definition at line 97 of file casDec.c.

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

Definition at line 98 of file casDec.c.

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

Definition at line 99 of file casDec.c.

---

Function Documentation

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

EXTERNAL FUNCTIONS ///

Definition at line 106 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;

    long clk1;

    s_LutSize = nLutSize;

    s_nFuncVars = nNames;

    // get the profile
    clk1 = 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*) malloc( 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 = Extra_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 **) malloc( p->nCols * sizeof(DdNode *) );
        p->pbCodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
        p->paNodes = (DdNode **) malloc( 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
        {
            long clk2 = 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 += 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 **) malloc( 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];
            }
            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)(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)(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 = 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)(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 );

        free( p->pbCols );
        free( p->pbCodes );
        free( p->paNodes );
        free( p );
    }

    return 1;
}

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

BLIF WRITING FUNCTIONS ///

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 815 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, ( 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, ( 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 );
}

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 940 of file casCore.c.

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


    DdNode * bFmin;
    int clk1;

    if ( s_ddmin == NULL )
        s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);

    clk1 = 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, ( 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, ( 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 );
}

void WriteLUTSintoBLIFfile	(	FILE *	pFile,
		DdManager *	dd,
		LUT **	pLuts,
		int	nLuts,
		DdNode **	bCVars,
		char **	pNames,
		int	nNames,
		char *	FileName
	)

static functions ///

Definition at line 414 of file casDec.c.

{
    int i, v, o;
    static char * pNamesLocalIn[MAXINPUTS];
    static char * pNamesLocalOut[MAXINPUTS];
    static char Buffer[100];
    DdNode * bCube, * bCof, * bFunc;
    LUT * p;

    // go through all the LUTs
    for ( i = 0; i < nLuts; i++ )
    {
        // get the pointer to the LUT
        p = pLuts[i];

        if ( i == nLuts -1 )
        {
            assert( p->nMulti == 1 );
        }


        fprintf( pFile, "#----------------- LUT #%d ----------------------\n", i );


        // fill in the names for the current LUT

        // write the outputs of the previous LUT
        if ( i != 0 )
        for ( v = 0; v < p->nInsP; v++ )
        {
            sprintf( Buffer, "LUT%02d_%02d", i-1, v );
            pNamesLocalIn[dd->invperm[v]] = Extra_UtilStrsav( Buffer );
        }
        // write the primary inputs of the current LUT
        for ( v = 0; v < p->nIns - p->nInsP; v++ )
            pNamesLocalIn[dd->invperm[p->Level+v]] = Extra_UtilStrsav( pNames[dd->invperm[p->Level+v]] );
        // write the outputs of the current LUT
        for ( v = 0; v < p->nMulti; v++ )
        {
            sprintf( Buffer, "LUT%02d_%02d", i, v );
            if ( i != nLuts - 1 )
                pNamesLocalOut[v] = Extra_UtilStrsav( Buffer );
            else 
                pNamesLocalOut[v] = Extra_UtilStrsav( "F" );
        }


        // write LUT outputs

        // get the prefix
        sprintf( Buffer, "L%02d_", i );

        // get the cube of encoding variables
        bCube = Extra_bddBitsToCube( dd, (1<<p->nMulti)-1, p->nMulti, bCVars, 1 );   Cudd_Ref( bCube );

        // write each output of the LUT
        for ( o = 0; o < p->nMulti; o++ )
        {
            // get the cofactor of this output
            bCof = Cudd_Cofactor( dd, p->bRelation, bCVars[o] );  Cudd_Ref( bCof );
            // quantify the remaining variables to get the function
            bFunc = Cudd_bddExistAbstract( dd, bCof, bCube );     Cudd_Ref( bFunc );
            Cudd_RecursiveDeref( dd, bCof );
            
            // write BLIF
            sprintf( Buffer, "L%02d_%02d_", i, o );

//          WriteDDintoBLIFfileReorder( dd, pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
            // does not work well; the advantage is marginal (30%), the run time is huge...

            WriteDDintoBLIFfile( pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
            Cudd_RecursiveDeref( dd, bFunc );
        }
        Cudd_RecursiveDeref( dd, bCube );

        // clean up the previous local names
        for ( v = 0; v < dd->size; v++ )
        {
            if ( pNamesLocalIn[v] )
                free( pNamesLocalIn[v] );
            pNamesLocalIn[v] = NULL;
        }
        for ( v = 0; v < p->nMulti; v++ )
            free( pNamesLocalOut[v] );
    }
}

---

Variable Documentation

long s_EncComputeTime

Definition at line 84 of file casDec.c.

long s_EncodingTime

Definition at line 81 of file casDec.c.

long s_EncSearchTime

Definition at line 83 of file casDec.c.

int s_LutSize = 15 [static]

static varibles ///

Definition at line 78 of file casDec.c.

int s_nFuncVars [static]

Definition at line 79 of file casDec.c.