src/base/abci/abcMv.c File Reference

#include "abc.h"
Include dependency graph for abcMv.c:

Go to the source code of this file.

Data Structures

struct  Mv_Man_t_

Typedefs

typedef struct Mv_Man_t_ Mv_Man_t

Functions

static void Abc_MvDecompose (Mv_Man_t *p)
static void Abc_MvPrintStats (Mv_Man_t *p)
static void Abc_MvRead (Mv_Man_t *p)
static void Abc_MvDeref (Mv_Man_t *p)
static DdNode * Abc_MvReadCube (DdManager *dd, char *pLine, int nVars)
void Abc_MvExperiment ()

Typedef Documentation

typedef struct Mv_Man_t_ Mv_Man_t

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

FileName [abcMv.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Multi-valued decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
abcMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 27 of file abcMv.c.

Function Documentation

void Abc_MvDecompose ( Mv_Man_t *  p  )  [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file abcMv.c.

00287 {
00288     DdNode * bCofs[16], * bVarCube1, * bVarCube2, * bVarCube, * bCube, * bVar0, * bVar1;//, * bRes;
00289     int k, i1, i2, v1, v2;//, c1, c2, Counter;
00290 
00291     bVar0 = Cudd_bddIthVar(p->dd, 30);
00292     bVar1 = Cudd_bddIthVar(p->dd, 31);
00293     bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bCube );
00294 
00295     for ( k = 0; k < p->nFuncs; k++ )
00296     {
00297         printf( "FUNCTION %d\n", k );
00298         for ( i1 = 0; i1 < p->nFuncs; i1++ )
00299         for ( i2 = i1+1; i2 < p->nFuncs; i2++ )
00300         {
00301             Vec_Ptr_t * vCofs;
00302 
00303             for ( v1 = 0; v1 < 4; v1++ )
00304             {
00305                 bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1  ), ((v1 & 1) == 0) );
00306                 bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1-1), ((v1 & 2) == 0) );
00307                 bVarCube1 = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bVarCube1 );
00308                 for ( v2 = 0; v2 < 4; v2++ )
00309                 {
00310                     bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2  ), ((v2 & 1) == 0) );
00311                     bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2-1), ((v2 & 2) == 0) );
00312                     bVarCube2 = Cudd_bddAnd( p->dd, bVar0, bVar1 );         Cudd_Ref( bVarCube2 );
00313                     bVarCube = Cudd_bddAnd( p->dd, bVarCube1, bVarCube2 );  Cudd_Ref( bVarCube );
00314                     bCofs[v1 * 4 + v2] = Cudd_Cofactor( p->dd, p->bFuncs[k], bVarCube );  Cudd_Ref( bCofs[v1 * 4 + v2] );
00315                     Cudd_RecursiveDeref( p->dd, bVarCube );
00316                     Cudd_RecursiveDeref( p->dd, bVarCube2 );
00317                 }
00318                 Cudd_RecursiveDeref( p->dd, bVarCube1 );
00319             }
00320 /*
00321             // check the compatibility of cofactors
00322             Counter = 0;
00323             for ( c1 = 0; c1 < 16; c1++ )
00324             {
00325                 for ( c2 = 0; c2 <= c1; c2++ )
00326                     printf( " " );
00327                 for ( c2 = c1+1; c2 < 16; c2++ )
00328                 {
00329                     bRes = Cudd_bddAndAbstract( p->dd, bCofs[c1], bCofs[c2], bCube );  Cudd_Ref( bRes );
00330                     if ( bRes == Cudd_ReadOne(p->dd) )
00331                     {
00332                         printf( "+" );
00333                         Counter++;
00334                     }
00335                     else
00336                     {
00337                         printf( " " );
00338                     }
00339                     Cudd_RecursiveDeref( p->dd, bRes );
00340                 }
00341                 printf( "\n" );
00342             }
00343 */
00344 
00345             vCofs = Vec_PtrAlloc( 16 );
00346             for ( v1 = 0; v1 < 4; v1++ )
00347             for ( v2 = 0; v2 < 4; v2++ )
00348                 Vec_PtrPushUnique( vCofs, bCofs[v1 * 4 + v2] );
00349             printf( "%d ", Vec_PtrSize(vCofs) );
00350             Vec_PtrFree( vCofs );
00351 
00352             // free the cofactors
00353             for ( v1 = 0; v1 < 4; v1++ )
00354             for ( v2 = 0; v2 < 4; v2++ )
00355                 Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
00356 
00357             printf( "\n" );
00358 //            printf( "%2d, %2d : %3d\n", i1, i2, Counter );
00359         }
00360     }
00361 
00362     Cudd_RecursiveDeref( p->dd, bCube );
00363 }

void Abc_MvDeref ( Mv_Man_t *  p  )  [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 260 of file abcMv.c.

00261 {
00262     int i, v;
00263     for ( i = 0; i < 15; i++ )
00264     for ( v = 0; v < 4; v++ )
00265     {
00266         Cudd_RecursiveDeref( p->dd, p->bValues[i][v] );
00267         Cudd_RecursiveDeref( p->dd, p->bValueDcs[i][v] );
00268     }
00269     for ( i = 0; i < 15; i++ )
00270         Cudd_RecursiveDeref( p->dd, p->bFuncs[i] );
00271 }

void Abc_MvExperiment (  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 59 of file abcMv.c.

00060 {
00061     Mv_Man_t * p;
00062     // get the functions
00063     p = ALLOC( Mv_Man_t, 1 );
00064     memset( p, 0, sizeof(Mv_Man_t) );
00065     p->dd = Cudd_Init( 32, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00066     p->nFuncs  = 15;
00067     p->nInputs =  9;
00068     Abc_MvRead( p );
00069     // process the functions
00070     Abc_MvPrintStats( p );
00071 //    Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 1 );
00072 //    Abc_MvPrintStats( p );
00073     // try detecting support reducing bound set
00074     Abc_MvDecompose( p );
00075 
00076     // remove the manager
00077     Abc_MvDeref( p );
00078     Extra_StopManager( p->dd );
00079     free( p );
00080 }

void Abc_MvPrintStats ( Mv_Man_t *  p  )  [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file abcMv.c.

00094 {
00095     int i, v;
00096     for ( i = 0; i < 15; i++ )
00097     {
00098         printf( "%2d : ", i );
00099         printf( "%3d (%2d)    ", Cudd_DagSize(p->bFuncs[i])-1, Cudd_SupportSize(p->dd, p->bFuncs[i]) );
00100         for ( v = 0; v < 4; v++ )
00101             printf( "%d = %3d (%2d)  ", v, Cudd_DagSize(p->bValues[i][v])-1, Cudd_SupportSize(p->dd, p->bValues[i][v]) );
00102         printf( "\n" );
00103     }
00104 }

void Abc_MvRead ( Mv_Man_t *  p  )  [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file abcMv.c.

00150 {
00151     FILE * pFile;
00152     char Buffer[1000], * pLine;
00153     DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum;
00154     int i, v;
00155 
00156     // start the cube
00157     bCubeSum = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( bCubeSum );
00158 
00159     // start the values
00160     for ( i = 0; i < 15; i++ )
00161     for ( v = 0; v < 4; v++ )
00162     {
00163         p->bValues[i][v]   = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValues[i][v] );
00164         p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValueDcs[i][v] );
00165     }
00166 
00167     // read the file
00168     pFile = fopen( "input.pla", "r" );
00169     while ( fgets( Buffer, 1000, pFile ) )
00170     {
00171         if ( Buffer[0] == '#' )
00172             continue;
00173         if ( Buffer[0] == '.' )
00174         {
00175             if ( Buffer[1] == 'e' )
00176                 break;
00177             continue;
00178         }
00179 
00180         // get the cube 
00181         bCube = Abc_MvReadCube( p->dd, Buffer, 18 );  Cudd_Ref( bCube );
00182 
00183         // add it to the values of the output functions
00184         pLine = Buffer + 19;
00185         for ( i = 0; i < 15; i++ )
00186         {
00187             if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' )
00188             {
00189                 for ( v = 0; v < 4; v++ )
00190                 {
00191                     p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube );  Cudd_Ref( p->bValueDcs[i][v] );
00192                     Cudd_RecursiveDeref( p->dd, bTemp );
00193                 }
00194                 continue;
00195             }
00196             else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0
00197                 v = 0;
00198             else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1
00199                 v = 1;
00200             else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2
00201                 v = 2;
00202             else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3
00203                 v = 3;
00204             else assert( 0 );
00205             // add the value
00206             p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube );  Cudd_Ref( p->bValues[i][v] );
00207             Cudd_RecursiveDeref( p->dd, bTemp );
00208         }
00209 
00210         // add the cube
00211         bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube );  Cudd_Ref( bCubeSum );
00212         Cudd_RecursiveDeref( p->dd, bTemp );
00213         Cudd_RecursiveDeref( p->dd, bCube );
00214     }
00215 
00216     // add the complement of the domain to all values
00217     for ( i = 0; i < 15; i++ )
00218         for ( v = 0; v < 4; v++ )
00219         {
00220             if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) )
00221                 continue;
00222             p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] );  Cudd_Ref( p->bValues[i][v] );
00223             Cudd_RecursiveDeref( p->dd, bTemp );
00224             p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) );  Cudd_Ref( p->bValues[i][v] );
00225             Cudd_RecursiveDeref( p->dd, bTemp );
00226         }
00227     printf( "Domain = %5.2f %%.\n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) ); 
00228     Cudd_RecursiveDeref( p->dd, bCubeSum );
00229 
00230     // create each output function
00231     for ( i = 0; i < 15; i++ )
00232     {
00233         p->bFuncs[i] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bFuncs[i] );
00234         for ( v = 0; v < 4; v++ )
00235         {
00236             bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) );
00237             bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) );
00238             bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );             Cudd_Ref( bCube );
00239             bProd = Cudd_bddAnd( p->dd, p->bValues[i][v], bCube );  Cudd_Ref( bProd );
00240             Cudd_RecursiveDeref( p->dd, bCube );
00241             // add the value
00242             p->bFuncs[i] = Cudd_bddOr( p->dd, bTemp = p->bFuncs[i], bProd );  Cudd_Ref( p->bFuncs[i] );
00243             Cudd_RecursiveDeref( p->dd, bTemp );
00244             Cudd_RecursiveDeref( p->dd, bProd );
00245         }
00246     }
00247 }

DdNode * Abc_MvReadCube ( DdManager *  dd,
char *  pLine,
int  nVars 
) [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file abcMv.c.

00118 {
00119     DdNode * bCube, * bVar, * bTemp;
00120     int i;
00121     bCube = Cudd_ReadOne(dd);  Cudd_Ref( bCube );
00122     for ( i = 0; i < nVars; i++ )
00123     {
00124         if ( pLine[i] == '-' )
00125             continue;
00126         else if ( pLine[i] == '0' ) // 0
00127             bVar = Cudd_Not( Cudd_bddIthVar(dd, 29-i) );
00128         else if ( pLine[i] == '1' ) // 1
00129             bVar = Cudd_bddIthVar(dd, 29-i);
00130         else assert(0);
00131         bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
00132         Cudd_RecursiveDeref( dd, bTemp );
00133     }
00134     Cudd_Deref( bCube );
00135     return bCube;
00136 }

Generated on Tue Jan 5 12:18:38 2010 for abc70930 by  doxygen 1.6.1