Version abc80130

1 files changed, 0 insertions, 508 deletions

diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
deleted file mode 100644
index a1eb5f36..00000000
--- a/src/bdd/cas/casDec.c
+++ /dev/null
@@ -1,508 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [casDec.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
-
-  Synopsis    [BDD-based decomposition with encoding.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - Spring 2002.]
-
-  Revision    [$Id: casDec.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <string.h>
-#include <stdlib.h>
-#include <time.h>
-
-#include "extra.h"
-#include "cas.h"
-
-////////////////////////////////////////////////////////////////////////
-///                      type definitions                            ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct
-{
-    int nIns;                // the number of LUT variables
-    int nInsP;               // the number of inputs coming from the previous LUT
-    int nCols;               // the number of columns in this LUT
-    int nMulti;              // the column multiplicity, [log2(nCols)]
-    int nSimple;             // the number of outputs implemented as direct connections to inputs of the previous block
-    int Level;               // the starting level in the ADD in this LUT
-
-//  DdNode ** pbVarsIn[32];  // the BDDs of the elementary input variables
-//  DdNode ** pbVarsOut[32]; // the BDDs of the elementary output variables 
-
-//  char * pNamesIn[32];     // the names of input variables
-//  char * pNamesOut[32];    // the names of output variables
-
-    DdNode ** pbCols;        // the array of columns represented by BDDs
-    DdNode ** pbCodes;       // the array of codes (in terms of pbVarsOut)
-    DdNode ** paNodes;       // the array of starting ADD nodes on the next level (also referenced)
-
-    DdNode * bRelation;      // the relation after encoding
-
-    // the relation depends on the three groups of variables:
-    // (1) variables on top represent the outputs of the previous cascade
-    // (2) variables in the middle represent the primary inputs
-    // (3) variables below (CVars) represent the codes
-    //
-    // the replacement is done after computing the relation
-} LUT;
-
-
-////////////////////////////////////////////////////////////////////////
-///                      static functions                            ///
-////////////////////////////////////////////////////////////////////////
-
-// the LUT-2-BLIF writing function
-void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName );
-
-// the function to write a DD (BDD or ADD) as a network of MUXES
-extern void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
-extern void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
-
-////////////////////////////////////////////////////////////////////////
-///                      static varibles                             ///
-////////////////////////////////////////////////////////////////////////
-
-static int s_LutSize = 15;
-static int s_nFuncVars; 
-
-long s_EncodingTime;
-
-long s_EncSearchTime;
-long s_EncComputeTime;
-
-////////////////////////////////////
-// temporary output variables
-//FILE * pTable;
-//long s_ReadingTime;
-//long s_RemappingTime;
-////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      debugging macros                            ///
-////////////////////////////////////////////////////////////////////////
-
-#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" ) 
-
-
-////////////////////////////////////////////////////////////////////////
-///                     EXTERNAL FUNCTIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose )
-// aFunc is a 0-1 ADD for the given function
-// pNames (nNames) are the input variable names
-// FileName is the name of the output file for the LUT network
-// dynamic variable reordering should be disabled when this function is running
-{
-    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 WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName )
-{
-    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] );
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                           END OF FILE                            ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-