Version abc70930

1 files changed, 508 insertions, 0 deletions

diff --git a/abc70930/src/bdd/cas/casDec.c b/abc70930/src/bdd/cas/casDec.c
new file mode 100644
index 00000000..a1eb5f36
--- /dev/null
+++ b/abc70930/src/bdd/cas/casDec.c
@@ -0,0 +1,508 @@
+/**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                            ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+