From d0a0cf63951e24a6d979af65c58d564254caec70 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 9 Apr 2016 17:00:46 -0700 Subject: Command &esop to convert AIG into ESOP. --- src/aig/gia/giaEsop.c | 506 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 1 + 2 files changed, 507 insertions(+) create mode 100644 src/aig/gia/giaEsop.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c new file mode 100644 index 00000000..9d95ccf5 --- /dev/null +++ b/src/aig/gia/giaEsop.c @@ -0,0 +1,506 @@ +/**CFile**************************************************************** + + FileName [giaEsop.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [ESOP computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/extra/extra.h" +#include "misc/vec/vecHsh.h" +#include "misc/vec/vecWec.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Eso_Man_t_ Eso_Man_t; +struct Eso_Man_t_ +{ + Gia_Man_t * pGia; // user's AIG + int nVars; // number of variables + int Cube1; // ID of const1 cube + Vec_Wec_t * vEsops; // ESOP for each node + Hsh_VecMan_t * pHash; // hash table for cubes + Vec_Wec_t * vCubes; // cover during minimization + // internal + Vec_Int_t * vCube1; // first cube + Vec_Int_t * vCube2; // second cube + Vec_Int_t * vCube; // resulting cube +}; + +static inline Vec_Int_t * Eso_ManCube( Eso_Man_t * p, int iCube ) { assert( iCube >= 0 ); return Hsh_VecReadEntry(p->pHash, iCube); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Eso_Man_t * Eso_ManAlloc( Gia_Man_t * pGia ) +{ + int i, n, Id; + Eso_Man_t * p = ABC_CALLOC( Eso_Man_t, 1 ); + p->pGia = pGia; + p->nVars = Gia_ManCiNum(pGia); + p->Cube1 = ABC_INFINITY; + p->vEsops = Vec_WecStart( Gia_ManObjNum(pGia) ); + p->pHash = Hsh_VecManStart( 1000 ); + p->vCubes = Vec_WecStart(Gia_ManCiNum(pGia)+1); + p->vCube1 = Vec_IntAlloc(Gia_ManCiNum(pGia)); + p->vCube2 = Vec_IntAlloc(Gia_ManCiNum(pGia)); + p->vCube = Vec_IntAlloc(Gia_ManCiNum(pGia)); + Gia_ManForEachCiId( pGia, Id, i ) + { + for ( n = 0; n < 2; n++ ) + { + Vec_IntFill( p->vCube, 1, Abc_Var2Lit(i, n) ); + Hsh_VecManAdd( p->pHash, p->vCube ); + } + Vec_IntPush( Vec_WecEntry(p->vEsops, Id), Abc_Var2Lit(i, 0) ); + } + return p; +} +void Eso_ManStop( Eso_Man_t * p ) +{ + Vec_WecFree( p->vEsops ); + Hsh_VecManStop( p->pHash ); + Vec_WecFree( p->vCubes ); + Vec_IntFree( p->vCube1 ); + Vec_IntFree( p->vCube2 ); + Vec_IntFree( p->vCube ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Printing/transforming the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Eso_ManCoverPrint( Eso_Man_t * p, Vec_Int_t * vEsop ) +{ + Vec_Str_t * vStr; + Vec_Int_t * vCube; + int i, k, Lit, Cube; + if ( Vec_IntSize(vEsop) == 0 ) + { + printf( "Const 0\n" ); + return; + } + vStr = Vec_StrAlloc( p->nVars + 4 ); + Vec_StrFill( vStr, p->nVars, '-' ); + Vec_StrPush( vStr, ' ' ); + Vec_StrPush( vStr, '1' ); + Vec_StrPush( vStr, '\n' ); + Vec_StrPush( vStr, '\0' ); + assert( Vec_IntSize(vEsop) > 0 ); + Vec_IntForEachEntry( vEsop, Cube, i ) + { + if ( Cube == p->Cube1 ) + printf( "%s", Vec_StrArray(vStr) ); + else + { + vCube = Eso_ManCube( p, Cube ); + Vec_IntForEachEntry( vCube, Lit, k ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit)?'0':'1') ); + printf( "%s", Vec_StrArray(vStr) ); + Vec_IntForEachEntry( vCube, Lit, k ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), '-' ); + } + } + printf( "\n" ); + Vec_StrFree( vStr ); +} +Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover ) +{ + Vec_Int_t * vEsop; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; int i; + pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) ); + pNew->pName = Abc_UtilStrsav( p->pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p->pGia)->Value = 0; + Gia_ManForEachCi( p->pGia, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i ) + { + if ( Vec_IntSize(vEsop) > 0 ) + { + int c, Cube, iRoot = 0; + Vec_IntForEachEntry( vEsop, Cube, c ) + { + int k, Lit, iAnd = 1; + if ( Cube != p->Cube1 ) + { + Vec_Int_t * vCube = Eso_ManCube( p, Cube ); + Vec_IntForEachEntry( vCube, Lit, k ) + iAnd = Gia_ManHashAnd( pNew, iAnd, Lit + 2 ); + } + iRoot = Gia_ManHashXor( pNew, iRoot, iAnd ); + } + Gia_ManAppendCo( pNew, iRoot ); + } + else + Gia_ManAppendCo( pNew, 0 ); + } + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Minimization.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Eso_ManFindDistOneLitEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 and pCube2 both have nLits +{ + int i, iDiff = -1; + for ( i = 0; i < nLits; i++ ) + if ( pCube1[i] != pCube2[i] ) + { + if ( iDiff != -1 ) + return -1; + if ( Abc_Lit2Var(pCube1[i]) != Abc_Lit2Var(pCube2[i]) ) + return -1; + iDiff = i; + } + return iDiff; +} +int Eso_ManFindDistOneLitNotEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 has nLits; pCube2 has nLits + 1 +{ + int i, k, iDiff = -1; + for ( i = k = 0; i < nLits; i++, k++ ) + if ( pCube1[i] != pCube2[k] ) + { + if ( iDiff != -1 ) + return -1; + iDiff = i; + i--; + } + if ( iDiff == -1 ) + iDiff = nLits; + return iDiff; +} +void Eso_ManMinimizeAdd( Eso_Man_t * p, int Cube ) +{ + int fMimimize = 1; + Vec_Int_t * vCube = (Cube == p->Cube1) ? NULL : Eso_ManCube(p, Cube); + int * pCube2, * pCube = (Cube == p->Cube1) ? NULL : Vec_IntArray(vCube); + int Cube2, nLits = (Cube == p->Cube1) ? 0 : Vec_IntSize(vCube); + Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits ); + int c, k, iLit, iPlace = Vec_IntFind( vLevel, Cube ); + if ( iPlace >= 0 ) // identical found + { + Vec_IntDrop( vLevel, iPlace ); + return; + } + if ( Cube == p->Cube1 ) // simple case + { + assert( Vec_IntSize(vLevel) == 0 ); + Vec_IntPush( vLevel, Cube ); + return; + } + // look for distance-1 in next bin + if ( fMimimize && nLits < p->nVars - 1 ) + { + Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits+1 ); + Vec_IntForEachEntry( vLevel, Cube2, c ) + { + pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); + iLit = Eso_ManFindDistOneLitNotEqual( pCube, pCube2, nLits ); + if ( iLit == -1 ) + continue; + // remove this cube + Vec_IntDrop( vLevel, c ); + // create new cube + Vec_IntClear( p->vCube ); + for ( k = 0; k <= nLits; k++ ) + Vec_IntPush( p->vCube, Abc_LitNotCond(pCube2[k], k == iLit) ); + Cube = Hsh_VecManAdd( p->pHash, p->vCube ); + // try to add new cube + Eso_ManMinimizeAdd( p, Cube ); + return; + } + } + // look for distance-1 in the same bin + if ( fMimimize ) + { + Vec_IntForEachEntry( vLevel, Cube2, c ) + { + pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); + iLit = Eso_ManFindDistOneLitEqual( pCube2, pCube, nLits ); + if ( iLit == -1 ) + continue; + // remove this cube + Vec_IntDrop( vLevel, c ); + // create new cube + Vec_IntClear( p->vCube ); + for ( k = 0; k < nLits; k++ ) + if ( k != iLit ) + Vec_IntPush( p->vCube, pCube[k] ); + if ( Vec_IntSize(p->vCube) == 0 ) + Cube = p->Cube1; + else + Cube = Hsh_VecManAdd( p->pHash, p->vCube ); + // try to add new cube + Eso_ManMinimizeAdd( p, Cube ); + return; + } + } + assert( nLits > 0 ); + if ( fMimimize && nLits > 0 ) + { + // look for distance-1 in the previous bin + Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits-1 ); + // check for the case of one-literal cube + if ( nLits == 1 && Vec_IntSize(vLevel) == 1 ) + { + Vec_IntDrop( vLevel, 0 ); + Cube = Abc_LitNot( Cube ); + } + else + Vec_IntForEachEntry( vLevel, Cube2, c ) + { + pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); + iLit = Eso_ManFindDistOneLitNotEqual( pCube2, pCube, nLits-1 ); + if ( iLit == -1 ) + continue; + // remove this cube + Vec_IntDrop( vLevel, c ); + // create new cube + Vec_IntClear( p->vCube ); + for ( k = 0; k < nLits; k++ ) + Vec_IntPush( p->vCube, Abc_LitNotCond(pCube[k], k == iLit) ); + Cube = Hsh_VecManAdd( p->pHash, p->vCube ); + // try to add new cube + Eso_ManMinimizeAdd( p, Cube ); + return; + } + } + // could not find - simply add this cube + Vec_IntPush( vLevel, Cube ); +} + +void Eso_ManMinimizeCopy( Eso_Man_t * p, Vec_Int_t * vEsop ) +{ + Vec_Int_t * vLevel; + int i; + Vec_IntClear( vEsop ); + Vec_WecForEachLevel( p->vCubes, vLevel, i ) + { + Vec_IntAppend( vEsop, vLevel ); + if ( i > 0 ) + { + int k, Cube; + Vec_IntForEachEntry( vLevel, Cube, k ) + assert( Vec_IntSize(Eso_ManCube(p, Cube)) == i ); + } + Vec_IntClear( vLevel ); + } +} + +/**Function************************************************************* + + Synopsis [Compute the produce of two covers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Eso_ManComputeAnd( Eso_Man_t * p, Vec_Int_t * vCube1, Vec_Int_t * vCube2, Vec_Int_t * vCube ) +{ + int * pBeg = vCube->pArray; + int * pBeg1 = vCube1->pArray; + int * pBeg2 = vCube2->pArray; + int * pEnd1 = vCube1->pArray + vCube1->nSize; + int * pEnd2 = vCube2->pArray + vCube2->nSize; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + *pBeg++ = *pBeg1++, pBeg2++; + else if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) ) + return -1; + else if ( *pBeg1 < *pBeg2 ) + *pBeg++ = *pBeg1++; + else + *pBeg++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg++ = *pBeg2++; + vCube->nSize = pBeg - vCube->pArray; + assert( vCube->nSize <= vCube->nCap ); + assert( vCube->nSize >= vCube1->nSize ); + assert( vCube->nSize >= vCube2->nSize ); + return Hsh_VecManAdd( p->pHash, vCube ); +} +void Eso_ManComputeOne( Eso_Man_t * p, Vec_Int_t * vEsop1, Vec_Int_t * vEsop2, Vec_Int_t * vEsop ) +{ + Vec_Int_t vCube1, vCube2; + int i, k, Cube1, Cube2, Cube; + Vec_IntClear( vEsop ); + if ( Vec_IntSize(vEsop1) == 0 || Vec_IntSize(vEsop2) == 0 ) + return; + Cube1 = Vec_IntEntry(vEsop1, 0); + Cube2 = Vec_IntEntry(vEsop2, 0); + Vec_IntForEachEntry( vEsop1, Cube1, i ) + { + if ( Cube1 == p->Cube1 ) + { + Vec_IntForEachEntry( vEsop2, Cube2, k ) + Eso_ManMinimizeAdd( p, Cube2 ); + continue; + } + Vec_IntForEachEntry( vEsop2, Cube2, k ) + { + if ( Cube2 == p->Cube1 ) + { + Eso_ManMinimizeAdd( p, Cube1 ); + continue; + } + vCube1 = *Hsh_VecReadEntry( p->pHash, Cube1 ); + vCube2 = *Hsh_VecReadEntry( p->pHash, Cube2 ); + Cube = Eso_ManComputeAnd( p, &vCube1, &vCube2, p->vCube ); + if ( Cube >= 0 ) + Eso_ManMinimizeAdd( p, Cube ); + } + } + Eso_ManMinimizeCopy( p, vEsop ); +} + +/**Function************************************************************* + + Synopsis [Complements the cover if needed, or just copy it.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Eso_ManTransformOne( Eso_Man_t * p, Vec_Int_t * vEsop, int fCompl, Vec_Int_t * vRes ) +{ + int i, Cube, Start = 0; + Vec_IntClear( vRes ); + if ( fCompl ) + { + if ( Vec_IntSize(vEsop) == 0 ) + Vec_IntPush( vRes, p->Cube1 ); + else + { + Cube = Vec_IntEntry(vEsop, 0); + if ( Cube == p->Cube1 ) + Start = 1; + else if ( Cube < 2 * p->nVars ) + Vec_IntPush( vRes, Abc_LitNot(Cube) ), Start = 1; + else + Vec_IntPush( vRes, p->Cube1 ); + } + } + Vec_IntForEachEntryStart( vEsop, Cube, i, Start ) + Vec_IntPush( vRes, Cube ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Computes ESOP from AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Vec_Ptr_t * vCover; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; int i, nCubes = 0, nCubesUsed = 0; + Vec_Int_t * vEsop1, * vEsop2, * vEsop; + Eso_Man_t * p = Eso_ManAlloc( pGia ); + Gia_ManForEachAnd( pGia, pObj, i ) + { + vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0(pObj, i) ); + vEsop2 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId1(pObj, i) ); + vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 ); + vEsop2 = Eso_ManTransformOne( p, vEsop2, Gia_ObjFaninC1(pObj), p->vCube2 ); + vEsop = Vec_WecEntry( p->vEsops, i ); + Eso_ManComputeOne( p, vEsop1, vEsop2, vEsop ); + nCubes += Vec_IntSize(vEsop); + } + vCover = Vec_PtrAlloc( Gia_ManCoNum(pGia) ); + Gia_ManForEachCo( pGia, pObj, i ) + { + vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0p(pGia, pObj) ); + vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 ); + printf( "Output %3d: ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) ); + if ( fVerbose ) + Eso_ManCoverPrint( p, vEsop1 ); + Vec_PtrPush( vCover, Vec_IntDup(vEsop1) ); + nCubesUsed += Vec_IntSize(vEsop1); + } + printf( "Outs = %d. Cubes = %d. Used = %d. Hashed = %d. ", + Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + pNew = Eso_ManCoverConvert( p, vCover ); + Vec_VecFree( (Vec_Vec_t *)vCover ); + Eso_ManStop( p ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index cebb73eb..8c3d5a39 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -22,6 +22,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaEquiv.c \ src/aig/gia/giaEra.c \ src/aig/gia/giaEra2.c \ + src/aig/gia/giaEsop.c \ src/aig/gia/giaFadds.c \ src/aig/gia/giaFalse.c \ src/aig/gia/giaFanout.c \ -- cgit v1.2.3