From 0c6505a26a537dc911b6566f82d759521e527c08 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Jan 2008 20:01:00 -0800 Subject: Version abc80130_2 --- src/base/abci/abcMv.c | 369 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 369 insertions(+) create mode 100644 src/base/abci/abcMv.c (limited to 'src/base/abci/abcMv.c') diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c new file mode 100644 index 00000000..2858b8a7 --- /dev/null +++ b/src/base/abci/abcMv.c @@ -0,0 +1,369 @@ +/**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 $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Mv_Man_t_ Mv_Man_t; +struct Mv_Man_t_ +{ + int nInputs; // the number of 4-valued input variables + int nFuncs; // the number of 4-valued functions + DdManager * dd; // representation of functions + DdNode * bValues[15][4]; // representation of i-sets + DdNode * bValueDcs[15][4]; // representation of i-sets don't-cares + DdNode * bFuncs[15]; // representation of 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 ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MvExperiment() +{ + Mv_Man_t * p; + // get the functions + p = ALLOC( Mv_Man_t, 1 ); + memset( p, 0, sizeof(Mv_Man_t) ); + p->dd = Cudd_Init( 32, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + p->nFuncs = 15; + p->nInputs = 9; + Abc_MvRead( p ); + // process the functions + Abc_MvPrintStats( p ); +// Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 1 ); +// Abc_MvPrintStats( p ); + // try detecting support reducing bound set + Abc_MvDecompose( p ); + + // remove the manager + Abc_MvDeref( p ); + Extra_StopManager( p->dd ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MvPrintStats( Mv_Man_t * p ) +{ + int i, v; + for ( i = 0; i < 15; i++ ) + { + printf( "%2d : ", i ); + printf( "%3d (%2d) ", Cudd_DagSize(p->bFuncs[i])-1, Cudd_SupportSize(p->dd, p->bFuncs[i]) ); + for ( v = 0; v < 4; v++ ) + printf( "%d = %3d (%2d) ", v, Cudd_DagSize(p->bValues[i][v])-1, Cudd_SupportSize(p->dd, p->bValues[i][v]) ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars ) +{ + DdNode * bCube, * bVar, * bTemp; + int i; + bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); + for ( i = 0; i < nVars; i++ ) + { + if ( pLine[i] == '-' ) + continue; + else if ( pLine[i] == '0' ) // 0 + bVar = Cudd_Not( Cudd_bddIthVar(dd, 29-i) ); + else if ( pLine[i] == '1' ) // 1 + bVar = Cudd_bddIthVar(dd, 29-i); + else assert(0); + bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bCube ); + return bCube; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MvRead( Mv_Man_t * p ) +{ + FILE * pFile; + char Buffer[1000], * pLine; + DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum; + int i, v; + + // start the cube + bCubeSum = Cudd_ReadLogicZero(p->dd); Cudd_Ref( bCubeSum ); + + // start the values + for ( i = 0; i < 15; i++ ) + for ( v = 0; v < 4; v++ ) + { + p->bValues[i][v] = Cudd_ReadLogicZero(p->dd); Cudd_Ref( p->bValues[i][v] ); + p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd); Cudd_Ref( p->bValueDcs[i][v] ); + } + + // read the file + pFile = fopen( "input.pla", "r" ); + while ( fgets( Buffer, 1000, pFile ) ) + { + if ( Buffer[0] == '#' ) + continue; + if ( Buffer[0] == '.' ) + { + if ( Buffer[1] == 'e' ) + break; + continue; + } + + // get the cube + bCube = Abc_MvReadCube( p->dd, Buffer, 18 ); Cudd_Ref( bCube ); + + // add it to the values of the output functions + pLine = Buffer + 19; + for ( i = 0; i < 15; i++ ) + { + if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' ) + { + for ( v = 0; v < 4; v++ ) + { + p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube ); Cudd_Ref( p->bValueDcs[i][v] ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + continue; + } + else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0 + v = 0; + else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1 + v = 1; + else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2 + v = 2; + else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3 + v = 3; + else assert( 0 ); + // add the value + p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube ); Cudd_Ref( p->bValues[i][v] ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + + // add the cube + bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube ); Cudd_Ref( bCubeSum ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bCube ); + } + + // add the complement of the domain to all values + for ( i = 0; i < 15; i++ ) + for ( v = 0; v < 4; v++ ) + { + if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) ) + continue; + p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] ); Cudd_Ref( p->bValues[i][v] ); + Cudd_RecursiveDeref( p->dd, bTemp ); + p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) ); Cudd_Ref( p->bValues[i][v] ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + printf( "Domain = %5.2f %%.\n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) ); + Cudd_RecursiveDeref( p->dd, bCubeSum ); + + // create each output function + for ( i = 0; i < 15; i++ ) + { + p->bFuncs[i] = Cudd_ReadLogicZero(p->dd); Cudd_Ref( p->bFuncs[i] ); + for ( v = 0; v < 4; v++ ) + { + bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) ); + bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) ); + bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bCube ); + bProd = Cudd_bddAnd( p->dd, p->bValues[i][v], bCube ); Cudd_Ref( bProd ); + Cudd_RecursiveDeref( p->dd, bCube ); + // add the value + p->bFuncs[i] = Cudd_bddOr( p->dd, bTemp = p->bFuncs[i], bProd ); Cudd_Ref( p->bFuncs[i] ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bProd ); + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MvDeref( Mv_Man_t * p ) +{ + int i, v; + for ( i = 0; i < 15; i++ ) + for ( v = 0; v < 4; v++ ) + { + Cudd_RecursiveDeref( p->dd, p->bValues[i][v] ); + Cudd_RecursiveDeref( p->dd, p->bValueDcs[i][v] ); + } + for ( i = 0; i < 15; i++ ) + Cudd_RecursiveDeref( p->dd, p->bFuncs[i] ); +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_MvDecompose( Mv_Man_t * p ) +{ + DdNode * bCofs[16], * bVarCube1, * bVarCube2, * bVarCube, * bCube, * bVar0, * bVar1;//, * bRes; + int k, i1, i2, v1, v2;//, c1, c2, Counter; + + bVar0 = Cudd_bddIthVar(p->dd, 30); + bVar1 = Cudd_bddIthVar(p->dd, 31); + bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bCube ); + + for ( k = 0; k < p->nFuncs; k++ ) + { + printf( "FUNCTION %d\n", k ); + for ( i1 = 0; i1 < p->nFuncs; i1++ ) + for ( i2 = i1+1; i2 < p->nFuncs; i2++ ) + { + Vec_Ptr_t * vCofs; + + for ( v1 = 0; v1 < 4; v1++ ) + { + bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1 ), ((v1 & 1) == 0) ); + bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1-1), ((v1 & 2) == 0) ); + bVarCube1 = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bVarCube1 ); + for ( v2 = 0; v2 < 4; v2++ ) + { + bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2 ), ((v2 & 1) == 0) ); + bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2-1), ((v2 & 2) == 0) ); + bVarCube2 = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bVarCube2 ); + bVarCube = Cudd_bddAnd( p->dd, bVarCube1, bVarCube2 ); Cudd_Ref( bVarCube ); + bCofs[v1 * 4 + v2] = Cudd_Cofactor( p->dd, p->bFuncs[k], bVarCube ); Cudd_Ref( bCofs[v1 * 4 + v2] ); + Cudd_RecursiveDeref( p->dd, bVarCube ); + Cudd_RecursiveDeref( p->dd, bVarCube2 ); + } + Cudd_RecursiveDeref( p->dd, bVarCube1 ); + } +/* + // check the compatibility of cofactors + Counter = 0; + for ( c1 = 0; c1 < 16; c1++ ) + { + for ( c2 = 0; c2 <= c1; c2++ ) + printf( " " ); + for ( c2 = c1+1; c2 < 16; c2++ ) + { + bRes = Cudd_bddAndAbstract( p->dd, bCofs[c1], bCofs[c2], bCube ); Cudd_Ref( bRes ); + if ( bRes == Cudd_ReadOne(p->dd) ) + { + printf( "+" ); + Counter++; + } + else + { + printf( " " ); + } + Cudd_RecursiveDeref( p->dd, bRes ); + } + printf( "\n" ); + } +*/ + + vCofs = Vec_PtrAlloc( 16 ); + for ( v1 = 0; v1 < 4; v1++ ) + for ( v2 = 0; v2 < 4; v2++ ) + Vec_PtrPushUnique( vCofs, bCofs[v1 * 4 + v2] ); + printf( "%d ", Vec_PtrSize(vCofs) ); + Vec_PtrFree( vCofs ); + + // free the cofactors + for ( v1 = 0; v1 < 4; v1++ ) + for ( v2 = 0; v2 < 4; v2++ ) + Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] ); + + printf( "\n" ); +// printf( "%2d, %2d : %3d\n", i1, i2, Counter ); + } + } + + Cudd_RecursiveDeref( p->dd, bCube ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3