Version abc80130_2

4 files changed, 1836 insertions, 0 deletions

diff --git a/src/bdd/cas/cas.h b/src/bdd/cas/cas.h
new file mode 100644
index 00000000..fcc9f890
--- /dev/null
+++ b/src/bdd/cas/cas.h
@@ -0,0 +1,62 @@
+/**CFile****************************************************************
+
+  FileName    [cas.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cas.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CAS_H__
+#define __CAS_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAXINPUTS   1024
+#define MAXOUTPUTS  1024
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== zzz.c ==========================================================*/
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
new file mode 100644
index 00000000..579235b1
--- /dev/null
+++ b/src/bdd/cas/casCore.c
@@ -0,0 +1,1263 @@
+/**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 $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+
+#include "extra.h"
+#include "cas.h"
+
+////////////////////////////////////////////////////////////////////////
+///                      static functions                            ///
+////////////////////////////////////////////////////////////////////////
+
+DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose );
+DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc );
+DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew );
+
+extern int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose );
+
+void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName );
+
+DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
+
+////////////////////////////////////////////////////////////////////////
+///                      static varibles                             ///
+////////////////////////////////////////////////////////////////////////
+
+//static FILE * pTable = NULL;
+//static long s_RemappingTime = 0;
+
+////////////////////////////////////////////////////////////////////////
+///                      debugging macros                            ///
+////////////////////////////////////////////////////////////////////////
+
+#define PRD(p)       printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 ) 
+#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                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose )
+{
+    int i;
+    int nVars = nInputs;
+    int nOuts = nOutputs;
+    long 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 = Extra_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 = 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)(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 = 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)(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 = clock();
+    if ( fCheck )
+    WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
+//    if ( fVerbose )
+//  printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+
+/*
+    ///////////////////////////////////////////////////////////////////
+    // verification of single output function
+    clk1 = 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)(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 = 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)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    ///////////////////////////////////////////////////////////////////
+*/
+ 
+    // verify the results
+    if ( fCheck )
+    {
+        extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+        extern void * Abc_FrameGetGlobalFrame();
+        char Command[200];
+        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++ )
+        free( pNames[i] );
+
+
+//fprintf( pTable, "\n" );
+//fclose( pTable );
+
+    return 1;
+}
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Experiment2( BFunc * pFunc )
+{
+    int i, x, RetValue;
+    int nVars = pFunc->nInputs;
+    int nOuts = pFunc->nOutputs;
+    DdManager * dd = pFunc->dd;
+    long 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];
+
+    DdManager * DdNew;
+
+//pTable = fopen( "stats.txt", "a+" );
+//fprintf( pTable, "%s ", pFunc->FileGeneric );
+//fprintf( pTable, "%d ", nVars );
+//fprintf( pTable, "%d ", nOuts );
+
+
+    // assign the file names
+    strcpy( FileNameIni, pFunc->FileGeneric );
+    strcat( FileNameIni, "_ENC.blif" );
+
+    strcpy( FileNameFin, pFunc->FileGeneric );
+    strcat( FileNameFin, "_LUT.blif" );
+
+    // derive the single-output function IN THE NEW MANAGER
+    clk1 = clock();
+//  aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
+    aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew );  Cudd_Ref( aFunc );
+    printf( "Single-output function derivation time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+//  s_RemappingTime = clock() - clk1;
+
+    // dispose of the multiple-output function
+    Extra_Dissolve( pFunc );
+
+    // reorder the single output function
+    printf( "\nReordering variables in the new manager...\n");
+    clk1 = clock();
+    printf( "Node count before = %d\n", Cudd_DagSize( aFunc ) );
+//  Cudd_ReduceHeap(DdNew, CUDD_REORDER_SIFT,1);
+    Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
+//  Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
+    printf( "Node count after  = %d\n", Cudd_DagSize( aFunc ) );
+    printf( "Variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    printf( "\n" );
+
+//fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
+//fprintf( pTable, "%d ", Extra_ProfileWidthMax(DdNew, aFunc) );
+
+
+    // create the names to be used with the new manager
+    nNames = DdNew->size;
+    for ( x = 0; x < nNames; x++ )
+    {
+        sprintf( Buffer, "v%02d", x );
+        pNames[x] = Extra_UtilStrsav( Buffer );
+    }
+
+
+
+    // write the single-output function into BLIF for verification
+    clk1 = clock();
+    WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni );
+    printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+
+
+    ///////////////////////////////////////////////////////////////////
+    // verification of single output function
+    clk1 = clock();
+    {
+        BFunc g_Func;
+        DdNode * aRes;
+
+        g_Func.dd = DdNew;
+        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( DdNew, g_Func.pOutputs[0] );  Cudd_Ref( aRes );
+
+        if ( aRes != aFunc )
+            printf( "\nVerification FAILED!\n");
+        else
+            printf( "\nVerification okay!\n");
+        
+        Cudd_RecursiveDeref( DdNew, aRes );
+
+        // delocate
+        Extra_Dissolve( &g_Func );
+    }
+    printf( "Preliminary verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    ///////////////////////////////////////////////////////////////////
+
+
+    CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 );
+
+/*
+    ///////////////////////////////////////////////////////////////////
+    // verification of the decomposed LUT network
+    clk1 = clock();
+    {
+        BFunc g_Func;
+        DdNode * aRes;
+
+        g_Func.dd = DdNew;
+        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( DdNew, g_Func.pOutputs[0] );  Cudd_Ref( aRes );
+
+        if ( aRes != aFunc )
+            printf( "\nFinal verification FAILED!\n");
+        else
+            printf( "\nFinal verification okay!\n");
+        
+        Cudd_RecursiveDeref( DdNew, aRes );
+
+        // delocate
+        Extra_Dissolve( &g_Func );
+    }
+    printf( "Final verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
+    ///////////////////////////////////////////////////////////////////
+*/
+
+
+    Cudd_RecursiveDeref( DdNew, aFunc );
+
+    // release the names
+    for ( i = 0; i < nNames; i++ )
+        free( pNames[i] );
+
+
+    
+    /////////////////////////////////////////////////////////////////////
+    // check for remaining references in the package
+    RetValue = Cudd_CheckZeroRef( DdNew );
+    printf( "\nThe number of referenced nodes in the new manager = %d\n", RetValue );
+    Cudd_Quit( DdNew );
+
+//fprintf( pTable, "\n" );
+//fclose( pTable );
+
+} 
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       SINGLE OUTPUT FUNCTION                     ///
+////////////////////////////////////////////////////////////////////////
+
+// the bit count for the first 256 integer numbers
+static unsigned char BitCount8[256] = {
+    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+
+/////////////////////////////////////////////////////////////
+static int s_SuppSize[MAXOUTPUTS];
+int CompareSupports( int *ptrX, int *ptrY )
+{
+    return ( s_SuppSize[*ptrY] - s_SuppSize[*ptrX] );
+}
+/////////////////////////////////////////////////////////////
+
+ 
+/////////////////////////////////////////////////////////////
+static int s_MintOnes[MAXOUTPUTS];
+int CompareMinterms( int *ptrX, int *ptrY )
+{
+    return ( s_MintOnes[*ptrY] - s_MintOnes[*ptrX] );
+}
+/////////////////////////////////////////////////////////////
+
+int GrayCode ( int BinCode )
+{ 
+  return BinCode ^ ( BinCode >> 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose )
+{
+    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,     nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareSupports );
+    // order the outputs
+//  qsort( (void*)OrderMint, 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;
+}
+/*
+DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc )
+{
+    int i;
+    DdNode * bResult, * aResult;
+    DdNode * bCube, * bTemp, * bProd;
+
+    bResult = b0;   Cudd_Ref( bResult );
+    for ( i = 0; i < nOuts; i++ )
+    {
+//      bCube   = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc );   Cudd_Ref( bCube );
+        bCube   = Extra_bddBitsToCube( dd, nOuts-1-i, nVarsEnc, pbVarsEnc );   Cudd_Ref( bCube );
+        bProd   = Cudd_bddAnd( dd, bCube, pbOuts[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 );
+    }
+
+    // conver to the ADD
+    aResult = Cudd_BddToAdd( dd, bResult );  Cudd_Ref( aResult );
+    Cudd_RecursiveDeref( dd, bResult );
+
+    Cudd_Deref( aResult );
+    return aResult;
+}
+*/
+
+
+////////////////////////////////////////////////////////////////////////
+///                        INPUT REMAPPING                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc )
+// returns the ADD of the remapped function
+{
+    static int Permute[MAXINPUTS];
+    static DdNode * pRemapped[MAXOUTPUTS];
+
+    DdNode * bSupp, * bTemp;
+    int i, Counter;
+    int nSuppPrev = -1;
+    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;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew )
+// returns the ADD of the remapped function
+{
+    static int Permute[MAXINPUTS];
+    static DdNode * pRemapped[MAXOUTPUTS];
+
+    static DdNode * pbVarsEnc[MAXINPUTS];
+    int nVarsEnc;
+
+    DdManager * ddnew;
+
+    DdNode * bSupp, * bTemp;
+    int i, v, Counter;
+    int nSuppPrev = -1;
+    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 = Extra_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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                        BLIF WRITING FUNCTIONS                    ///
+////////////////////////////////////////////////////////////////////////
+
+void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName )
+{
+    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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames )
+// writes the main part of the BLIF file 
+// Func is a BDD or a 0-1 ADD to be written
+// OutputName is the name of the output
+// Prefix is attached to each intermendiate signal to make it unique
+// InputNames are the names of the input signals
+// (some part of the code is borrowed from Cudd_DumpDot())
+{
+    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 );
+}
+
+
+
+
+static DdManager * s_ddmin;
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames )
+// writes the main part of the BLIF file 
+// Func is a BDD or a 0-1 ADD to be written
+// OutputName is the name of the output
+// Prefix is attached to each intermendiate signal to make it unique
+// InputNames are the names of the input signals
+// (some part of the code is borrowed from Cudd_DumpDot())
+{
+    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 );
+    //////////////////////////////////////////////////
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                    TRANSFER WITH MAPPING                         ///
+////////////////////////////////////////////////////////////////////////
+static DdNode * cuddBddTransferPermuteRecur
+ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute ));
+
+static DdNode * cuddBddTransferPermute
+ARGS((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. 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     []
+
+******************************************************************************/
+DdNode *
+Cudd_bddTransferPermute( DdManager * ddSource,
+                  DdManager * ddDestination, DdNode * f, int * Permute )
+{
+    DdNode *res;
+    do
+    {
+        ddDestination->reordered = 0;
+        res = cuddBddTransferPermute( ddSource, ddDestination, f, Permute );
+    }
+    while ( ddDestination->reordered == 1 );
+    return ( res );
+
+}                               /* end of Cudd_bddTransferPermute */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**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]
+
+******************************************************************************/
+DdNode *
+cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute )
+{
+    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, ( 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Cudd_bddTransferPermute.]
+
+  Description [Performs the recursive step of Cudd_bddTransferPermute.
+  Returns a pointer to the result if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [cuddBddTransferPermute]
+
+******************************************************************************/
+static DdNode *
+cuddBddTransferPermuteRecur( DdManager * ddS,
+                      DdManager * ddD, DdNode * f, st_table * table, int * Permute )
+{
+    DdNode *ft, *fe, *t, *e, *var, *res;
+    DdNode *one, *zero;
+    int index;
+    int comple = 0;
+
+    statLine( ddD );
+    one = DD_ONE( ddD );
+    comple = Cudd_IsComplement( f );
+
+    /* Trivial cases. */
+    if ( Cudd_IsConstant( f ) )
+        return ( Cudd_NotCond( one, comple ) );
+
+    /* Make canonical to increase the utilization of the cache. */
+    f = Cudd_NotCond( f, comple );
+    /* Now f is a regular pointer to a non-constant node. */
+
+    /* Check the cache. */
+    if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
+        return ( Cudd_NotCond( res, comple ) );
+
+    /* Recursive step. */
+    index = Permute[f->index];
+    ft = cuddT( f );
+    fe = cuddE( f );
+
+    t = cuddBddTransferPermuteRecur( ddS, ddD, ft, table, Permute );
+    if ( t == NULL )
+    {
+        return ( NULL );
+    }
+    cuddRef( t );
+
+    e = cuddBddTransferPermuteRecur( ddS, ddD, fe, table, Permute );
+    if ( e == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        return ( NULL );
+    }
+    cuddRef( e );
+
+    zero = Cudd_Not( one );
+    var = cuddUniqueInter( ddD, index, one, zero );
+    if ( var == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        Cudd_RecursiveDeref( ddD, e );
+        return ( NULL );
+    }
+    res = cuddBddIteRecur( ddD, var, t, e );
+    if ( res == NULL )
+    {
+        Cudd_RecursiveDeref( ddD, t );
+        Cudd_RecursiveDeref( ddD, e );
+        return ( NULL );
+    }
+    cuddRef( res );
+    Cudd_RecursiveDeref( ddD, t );
+    Cudd_RecursiveDeref( ddD, e );
+
+    if ( st_add_direct( table, ( char * ) f, ( char * ) res ) ==
+         ST_OUT_OF_MEM )
+    {
+        Cudd_RecursiveDeref( ddD, res );
+        return ( NULL );
+    }
+    return ( Cudd_NotCond( res, comple ) );
+
+}                               /* end of cuddBddTransferPermuteRecur */
+
+////////////////////////////////////////////////////////////////////////
+///                           END OF FILE                            ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
new file mode 100644
index 00000000..a1eb5f36
--- /dev/null
+++ b/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                            ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+
diff --git a/src/bdd/cas/module.make b/src/bdd/cas/module.make
new file mode 100644
index 00000000..7830e47f
--- /dev/null
+++ b/src/bdd/cas/module.make
@@ -0,0 +1,3 @@
+SRC +=    src/bdd/cas/casCore.c \
+    src/bdd/cas/casDec.c
+