diff options
Diffstat (limited to 'src/opt')
| -rw-r--r-- | src/opt/rwr/rwr.h | 1 | ||||
| -rw-r--r-- | src/opt/rwr/rwrMan.c | 23 | ||||
| -rw-r--r-- | src/opt/xyz/module.make | 8 | ||||
| -rw-r--r-- | src/opt/xyz/xyz.h | 94 | ||||
| -rw-r--r-- | src/opt/xyz/xyzBuild.c | 379 | ||||
| -rw-r--r-- | src/opt/xyz/xyzCore.c | 697 | ||||
| -rw-r--r-- | src/opt/xyz/xyzInt.h | 631 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMan.c | 144 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinEsop.c | 277 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinMan.c | 112 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinSop.c | 341 | ||||
| -rw-r--r-- | src/opt/xyz/xyzMinUtil.c | 225 | ||||
| -rw-r--r-- | src/opt/xyz/xyzTest.c | 51 |
13 files changed, 2983 insertions, 0 deletions
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index 3856c04e..70e1070b 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -129,6 +129,7 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p ); extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute ); extern void Rwr_ManStop( Rwr_Man_t * p ); extern void Rwr_ManPrintStats( Rwr_Man_t * p ); +extern void Rwr_ManPrintStatsFile( Rwr_Man_t * p ); extern void * Rwr_ManReadDecs( Rwr_Man_t * p ); extern int Rwr_ManReadCompl( Rwr_Man_t * p ); extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time ); diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c index 1d306e7e..115065f5 100644 --- a/src/opt/rwr/rwrMan.c +++ b/src/opt/rwr/rwrMan.c @@ -179,6 +179,29 @@ void Rwr_ManPrintStats( Rwr_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Rwr_ManPrintStatsFile( Rwr_Man_t * p ) +{ + FILE * pTable; + pTable = fopen( "stats.txt", "a+" ); + fprintf( pTable, "%d ", p->nCutsGood ); + fprintf( pTable, "%d ", p->nSubgraphs ); + fprintf( pTable, "%d ", p->nNodesRewritten ); + fprintf( pTable, "%d", p->nNodesGained ); + fprintf( pTable, "\n" ); + fclose( pTable ); +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void * Rwr_ManReadDecs( Rwr_Man_t * p ) { return p->pGraph; diff --git a/src/opt/xyz/module.make b/src/opt/xyz/module.make new file mode 100644 index 00000000..ae7dab0f --- /dev/null +++ b/src/opt/xyz/module.make @@ -0,0 +1,8 @@ +SRC += src/opt/xyz/xyzBuild.c \ + src/opt/xyz/xyzCore.c \ + src/opt/xyz/xyzMan.c \ + src/opt/xyz/xyzMinEsop.c \ + src/opt/xyz/xyzMinMan.c \ + src/opt/xyz/xyzMinSop.c \ + src/opt/xyz/xyzMinUtil.c \ + src/opt/xyz/xyzTest.c diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h new file mode 100644 index 00000000..f18686ff --- /dev/null +++ b/src/opt/xyz/xyz.h @@ -0,0 +1,94 @@ +/**CFile**************************************************************** + + FileName [xyz.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Xyz_Man_t_ Xyz_Man_t; +typedef struct Xyz_Obj_t_ Xyz_Obj_t; + +// storage for node information +struct Xyz_Obj_t_ +{ + Min_Cube_t * pCover[3]; // pos/neg/esop + Vec_Int_t * vSupp; // computed support (all nodes except CIs) +}; + +// storage for additional information +struct Xyz_Man_t_ +{ + // general characteristics + int nFaninMax; // the number of vars + int nCubesMax; // the limit on the number of cubes in the intermediate covers + int nWords; // the number of words + Vec_Int_t * vFanCounts; // fanout counts + Vec_Ptr_t * vObjStrs; // object structures + void * pMemory; // memory for the internal data strctures + Min_Man_t * pManMin; // the cub manager + // arrays to map local variables + Vec_Int_t * vComTo0; // mapping of common variables into first fanin + Vec_Int_t * vComTo1; // mapping of common variables into second fanin + Vec_Int_t * vPairs0; // the first var in each pair of common vars + Vec_Int_t * vPairs1; // the second var in each pair of common vars + Vec_Int_t * vTriv0; // trival support of the first node + Vec_Int_t * vTriv1; // trival support of the second node + // statistics + int nSupps; // supports created + int nSuppsMax; // the maximum number of supports + int nBoundary; // the boundary size + int nNodes; // the number of nodes processed +}; + +static inline Xyz_Obj_t * Abc_ObjGetStr( Abc_Obj_t * pObj ) { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); } + +static inline void Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec ) { Abc_ObjGetStr(pObj)->vSupp = vVec; } +static inline Vec_Int_t * Abc_ObjGetSupp( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->vSupp; } + +static inline void Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; } +static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->pCover[2]; } + +static inline void Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; } +static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol ) { return Abc_ObjGetStr(pObj)->pCover[Pol]; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== xyzBuild.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk ); +/*=== xyzCore.c ===========================================================*/ +extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ); +/*=== xyzMan.c ============================================================*/ +extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax ); +extern void Xyz_ManFree( Xyz_Man_t * p ); +extern void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ); +/*=== xyzTest.c ===========================================================*/ +extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzBuild.c b/src/opt/xyz/xyzBuild.c new file mode 100644 index 00000000..e32721e7 --- /dev/null +++ b/src/opt/xyz/xyzBuild.c @@ -0,0 +1,379 @@ +/**CFile**************************************************************** + + FileName [xyzBuild.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Network construction procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp ) +{ + Vec_Int_t * vLits; + Abc_Obj_t * pNodeNew, * pFanin; + int i, iFanin, Lit; + // create empty cube + if ( pCube->nLits == 0 ) + return Abc_NodeCreateConst1(pNtkNew); + // get the literals of this cube + vLits = Vec_IntAlloc( 10 ); + Min_CubeGetLits( pCube, vLits ); + assert( pCube->nLits == (unsigned)vLits->nSize ); + // create special case when there is only one literal + if ( pCube->nLits == 1 ) + { + iFanin = Vec_IntEntry(vLits,0); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntFree( vLits ); + if ( Lit == 1 )// negative + return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy ); + return pFanin->pCopy; + } + assert( pCube->nLits > 1 ); + // create the AND cube + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + for ( i = 0; i < vLits->nSize; i++ ) + { + iFanin = Vec_IntEntry(vLits,i); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntWriteEntry( vLits, i, Lit==1 ); + Abc_ObjAddFanin( pNodeNew, pFanin->pCopy ); + } + pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray ); + Vec_IntFree( vLits ); + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level ) +{ + Min_Cube_t * pCover, * pCube; + Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin; + Vec_Int_t * vSupp; + int Entry, nCubes, i; + + if ( Abc_ObjIsCi(pObj) ) + return pObj->pCopy; + assert( Abc_ObjIsNode(pObj) ); + // skip if already computed + if ( pObj->pCopy ) + return pObj->pCopy; + + // get the support and the cover + vSupp = Abc_ObjGetSupp( pObj ); + pCover = Abc_ObjGetCover2( pObj ); + assert( vSupp ); +/* + if ( pCover && pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 ) + { + printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) ); + Min_CoverWrite( stdout, pCover ); + } +*/ +/* + // print the support of this node + printf( "{ " ); + Vec_IntForEachEntry( vSupp, Entry, i ) + printf( "%d ", Entry ); + printf( "} cubes = %d\n", Min_CoverCountCubes( pCover ) ); +*/ + // process the fanins + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFanin = Abc_NtkObj(pObj->pNtk, Entry); + Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 ); + } + + // for each cube, construct the node + nCubes = Min_CoverCountCubes( pCover ); + if ( nCubes == 0 ) + pNodeNew = Abc_NodeCreateConst0(pNtkNew); + else if ( nCubes == 1 ) + pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp ); + else + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Min_CoverForEachCube( pCover, pCube ) + { + pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp ); + Abc_ObjAddFanin( pNodeNew, pFaninNew ); + } + pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes ); + } +/* + printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level ); + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFanin = Abc_NtkObj(pObj->pNtk, Entry); + printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id ); + } + printf( "\n" ); + Min_CoverWrite( stdout, pCover ); +*/ + pObj->pCopy = pNodeNew; + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // reconstruct the network + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 ); +// printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id ); + } + // add the COs + Abc_NtkFinalize( pNtk, pNtkNew ); + Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkXyzDerive: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + + + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl ) +{ + assert( pObj->pCopy ); + if ( !fCompl ) + return pObj->pCopy; + if ( pObj->pCopy->pCopy == NULL ) + pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy ); + return pObj->pCopy->pCopy; + } + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp ) +{ + Vec_Int_t * vLits; + Abc_Obj_t * pNodeNew, * pFanin; + int i, iFanin, Lit; + // create empty cube + if ( pCube->nLits == 0 ) + return Abc_NodeCreateConst1(pNtkNew); + // get the literals of this cube + vLits = Vec_IntAlloc( 10 ); + Min_CubeGetLits( pCube, vLits ); + assert( pCube->nLits == (unsigned)vLits->nSize ); + // create special case when there is only one literal + if ( pCube->nLits == 1 ) + { + iFanin = Vec_IntEntry(vLits,0); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntFree( vLits ); +// if ( Lit == 1 )// negative +// return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy ); +// return pFanin->pCopy; + return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ); + } + assert( pCube->nLits > 1 ); + // create the AND cube + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + for ( i = 0; i < vLits->nSize; i++ ) + { + iFanin = Vec_IntEntry(vLits,i); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntWriteEntry( vLits, i, Lit==1 ); +// Abc_ObjAddFanin( pNodeNew, pFanin->pCopy ); + Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) ); + } +// pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray ); + pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL ); + Vec_IntFree( vLits ); + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl ) +{ + Min_Cube_t * pCover, * pCube; + Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin; + Vec_Int_t * vSupp; + int Entry, nCubes, i; + + // skip if already computed + if ( pObj->pCopy ) + return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl ); + assert( Abc_ObjIsNode(pObj) ); + + // get the support and the cover + vSupp = Abc_ObjGetSupp( pObj ); + pCover = Abc_ObjGetCover2( pObj ); + assert( vSupp ); + + // process the fanins + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFanin = Abc_NtkObj(pObj->pNtk, Entry); + Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 ); + } + + // for each cube, construct the node + nCubes = Min_CoverCountCubes( pCover ); + if ( nCubes == 0 ) + pNodeNew = Abc_NodeCreateConst0(pNtkNew); + else if ( nCubes == 1 ) + pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp ); + else + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Min_CoverForEachCube( pCover, pCube ) + { + pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp ); + Abc_ObjAddFanin( pNodeNew, pFaninNew ); + } + pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes ); + } + + pObj->pCopy = pNodeNew; + return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl ); +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [The resulting network contains only pure AND/OR/EXOR gates + and inverters. This procedure is usedful to generate Verilog.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pNodeNew; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // reconstruct the network + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pObj->pCopy, pNodeNew ); + } + // add the COs + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c new file mode 100644 index 00000000..a48f749e --- /dev/null +++ b/src/opt/xyz/xyzCore.c @@ -0,0 +1,697 @@ +/**CFile**************************************************************** + + FileName [xyzCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); +static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); +static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ); + +static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); +static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); +static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + Xyz_Man_t * p; + + assert( Abc_NtkIsStrash(pNtk) ); + + // create the manager + p = Xyz_ManAlloc( pNtk, nFaninMax ); + pNtk->pManCut = p; + + // perform mapping + Abc_NtkXyzCovers( p, pNtk, fVerbose ); + + // derive the final network + if ( fUseInvs ) + pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk ); + else + pNtkNew = Abc_NtkXyzDerive( p, pNtk ); + + Xyz_ManFree( p ); + pNtk->pManCut = NULL; + + // make sure that everything is okay + if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkXyz: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Compute the supports.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) +{ + Abc_Obj_t * pObj; + int i, clk = clock(); + + // start the manager + p->vFanCounts = Abc_NtkFanoutCounts(pNtk); + + // set trivial cuts for the constant and the CIs + pObj = Abc_NtkConst1(pNtk); + pObj->fMarkA = 1; + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->fMarkA = 1; + + // perform iterative decomposition + for ( i = 0; ; i++ ) + { + if ( fVerbose ) + printf( "Iter %d : ", i+1 ); + if ( Abc_NtkXyzCoversOne(p, pNtk, fVerbose) ) + break; + } + + // clean the cut-point markers + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->fMarkA = 0; + +if ( fVerbose ) +{ +PRT( "Total", clock() - clk ); +} +} + +/**Function************************************************************* + + Synopsis [Compute the supports.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pObj; + Vec_Ptr_t * vBoundary; + int i, clk = clock(); + int Counter = 0; + int fStop = 1; + + // array to collect the nodes in the new boundary + vBoundary = Vec_PtrAlloc( 100 ); + + // start from the COs and mark visited nodes using pObj->fMarkB + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // skip the solved nodes (including the CIs) + pObj = Abc_ObjFanin0(pObj); + if ( pObj->fMarkA ) + { + Counter++; + continue; + } + + // traverse the cone starting from this node + Abc_NtkXyzCovers_rec( p, pObj, vBoundary ); + if ( Abc_ObjGetSupp(pObj) == NULL ) + fStop = 0; + else + Counter++; + +/* + printf( "%-15s : ", Abc_ObjName(pObj) ); + printf( "lev = %5d ", pObj->Level ); + if ( Abc_ObjGetSupp(pObj) == NULL ) + { + printf( "\n" ); + continue; + } + printf( "supp = %3d ", Abc_ObjGetSupp(pObj)->nSize ); + printf( "esop = %3d ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) ); + printf( "\n" ); +*/ + } + Extra_ProgressBarStop( pProgress ); + + // clean visited nodes + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->fMarkB = 0; + + // create the new boundary + p->nBoundary = 0; + Vec_PtrForEachEntry( vBoundary, pObj, i ) + { + if ( !pObj->fMarkA ) + { + pObj->fMarkA = 1; + p->nBoundary++; + } + } + Vec_PtrFree( vBoundary ); + +if ( fVerbose ) +{ + printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d Bound = %4d ", + Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary ); +PRT( "T", clock() - clk ); +} + return fStop; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ) +{ + Abc_Obj_t * pObj0, * pObj1; + // return if the support is already computed + if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) ) + return; + // mark as visited + pObj->fMarkB = 1; + // get the fanins + pObj0 = Abc_ObjFanin0(pObj); + pObj1 = Abc_ObjFanin1(pObj); + // solve for the fanins + Abc_NtkXyzCovers_rec( p, pObj0, vBoundary ); + Abc_NtkXyzCovers_rec( p, pObj1, vBoundary ); + // skip the node that spaced out + if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready + !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready + !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) ) // node's support or covers cannot be computed + { + // save the nodes of the future boundary + if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) ) + Vec_PtrPush( vBoundary, pObj0 ); + if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) ) + Vec_PtrPush( vBoundary, pObj1 ); + return; + } + // consider dropping the fanin supports +// Abc_NodeXyzDropData( p, pObj0 ); +// Abc_NodeXyzDropData( p, pObj1 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 ) +{ + Vec_Int_t * vSupp; + int k0, k1; + + assert( vSupp0 && vSupp1 ); + Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 ); + Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 ); + Vec_IntClear( p->vPairs0 ); + Vec_IntClear( p->vPairs1 ); + + vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize ); + for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; ) + { + if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( p->vPairs0, k0 ); + Vec_IntPush( p->vPairs1, k1 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + k0++; k1++; + } + else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + k0++; + } + else + { + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( vSupp, vSupp1->pArray[k1] ); + k1++; + } + } + for ( ; k0 < vSupp0->nSize; k0++ ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + } + for ( ; k1 < vSupp1->nSize; k1++ ) + { + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( vSupp, vSupp1->pArray[k1] ); + } +/* + printf( "Zero : " ); + for ( k0 = 0; k0 < vSupp0->nSize; k0++ ) + printf( "%d ", vSupp0->pArray[k0] ); + printf( "\n" ); + + printf( "One : " ); + for ( k1 = 0; k1 < vSupp1->nSize; k1++ ) + printf( "%d ", vSupp1->pArray[k1] ); + printf( "\n" ); + + printf( "Sum : " ); + for ( k0 = 0; k0 < vSupp->nSize; k0++ ) + printf( "%d ", vSupp->pArray[k0] ); + printf( "\n" ); + printf( "\n" ); +*/ + return vSupp; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) +{ + Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1; + Vec_Int_t * vSupp, * vSupp0, * vSupp1; + + if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); + if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); + + // get the resulting support + vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); + vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); + vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 ); + + // quit if support if too large + if ( vSupp->nSize > p->nFaninMax ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // get the covers + pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); + pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); + + // complement the first if needed + if ( !Abc_ObjFaninC0(pObj) ) + pCover0 = pCov0; + else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube + pCover0 = pCov0->pNext; + else + pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; + + // complement the second if needed + if ( !Abc_ObjFaninC1(pObj) ) + pCover1 = pCov1; + else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube + pCover1 = pCov1->pNext; + else + pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; + + // derive and minimize the cover (quit if too large) + if ( !Abc_NodeXyzProductEsop( p, pCover0, pCover1, vSupp->nSize ) ) + { + pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); + Min_CoverRecycle( p->pManMin, pCover ); + Vec_IntFree( vSupp ); + return 0; + } + + // minimize the cover + Min_EsopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); + + // quit if the cover is too large + if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCover ); + Vec_IntFree( vSupp ); + return 0; + } + + // count statistics + p->nSupps++; + p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps ); + + // set the covers + assert( Abc_ObjGetSupp(pObj) == NULL ); + Abc_ObjSetSupp( pObj, vSupp ); + Abc_ObjSetCover2( pObj, pCover ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) +{ + Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1; + Vec_Int_t * vSupp, * vSupp0, * vSupp1; + int fCompl0, fCompl1; + + if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); + if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); + + // get the resulting support + vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); + vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); + vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 ); + + // quit if support if too large + if ( vSupp->nSize > p->nFaninMax ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // get the complemented attributes + fCompl0 = Abc_ObjFaninC0(pObj); + fCompl1 = Abc_ObjFaninC1(pObj); + + // prepare the positive cover + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); + + // derive and minimize the cover (quit if too large) + if ( !pCover0 || !pCover1 ) + pCoverP = NULL; + else if ( !Abc_NodeXyzProductSop( p, pCover0, pCover1, vSupp->nSize ) ) + { + pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); + Min_CoverRecycle( p->pManMin, pCoverP ); + pCoverP = NULL; + } + else + { + Min_SopMinimize( p->pManMin ); + pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); + // quit if the cover is too large + if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCoverP ); + pCoverP = NULL; + } + } + + // prepare the negative cover + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); + + // derive and minimize the cover (quit if too large) + if ( !pCover0 || !pCover1 ) + pCoverN = NULL; + else if ( !Abc_NodeXyzUnionSop( p, pCover0, pCover1, vSupp->nSize ) ) + { + pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); + Min_CoverRecycle( p->pManMin, pCoverN ); + pCoverN = NULL; + } + else + { + Min_SopMinimize( p->pManMin ); + pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); + // quit if the cover is too large + if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCoverN ); + pCoverN = NULL; + } + } + + if ( pCoverP == NULL && pCoverN == NULL ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // count statistics + p->nSupps++; + p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps ); + + // set the covers + assert( Abc_ObjGetSupp(pObj) == NULL ); + Abc_ObjSetSupp( pObj, vSupp ); + Abc_ObjSetCover( pObj, pCoverP, 0 ); + Abc_ObjSetCover( pObj, pCoverN, 1 ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + int i, Val0, Val1; + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + if ( pCover0 == NULL || pCover1 == NULL ) + return 1; + + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + // go through the support variables of the cubes + for ( i = 0; i < p->vPairs0->nSize; i++ ) + { + Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); + Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); + if ( (Val0 & Val1) == 0 ) + break; + } + // check disjointness + if ( i < p->vPairs0->nSize ) + continue; + + if ( p->pManMin->nCubes >= p->nCubesMax ) + return 0; + + // create the product cube + pCube = Min_CubeAlloc( p->pManMin ); + + // add the literals + pCube->nLits = 0; + for ( i = 0; i < nSupp; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + Val0 = 3; + else + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + + if ( p->vComTo1->pArray[i] == -1 ) + Val1 = 3; + else + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + + if ( (Val0 & Val1) == 3 ) + continue; + + Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); + pCube->nLits++; + } + // add the cube to storage + while ( Min_EsopAddCube( p->pManMin, pCube ) ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + return 1; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + int i, Val0, Val1; + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + if ( pCover0 ) + { + Min_CoverForEachCube( pCover0, pCube0 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo0->nSize; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + continue; + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + if ( Val0 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val0 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes >= p->nCubesMax ) + return 0; + // add the cube to storage + while ( Min_EsopAddCube( p->pManMin, pCube ) ); + } + } + if ( pCover1 ) + { + Min_CoverForEachCube( pCover1, pCube1 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo1->nSize; i++ ) + { + if ( p->vComTo1->pArray[i] == -1 ) + continue; + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + if ( Val1 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val1 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes >= p->nCubesMax ) + return 0; + // add the cube to storage + while ( Min_EsopAddCube( p->pManMin, pCube ) ); + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + return 1; +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h new file mode 100644 index 00000000..22950bfd --- /dev/null +++ b/src/opt/xyz/xyzInt.h @@ -0,0 +1,631 @@ +/**CFile**************************************************************** + + FileName [xyzInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Min_Man_t_ Min_Man_t; +typedef struct Min_Cube_t_ Min_Cube_t; + +struct Min_Man_t_ +{ + int nVars; // the number of vars + int nWords; // the number of words + Extra_MmFixed_t * pMemMan; // memory manager for cubes + // temporary cubes + Min_Cube_t * pOne0; // tautology cube + Min_Cube_t * pOne1; // tautology cube + Min_Cube_t * pTriv0[2]; // trivial cube + Min_Cube_t * pTriv1[2]; // trivial cube + Min_Cube_t * pTemp; // cube for computing the distance + Min_Cube_t * pBubble; // cube used as a separator + // temporary storage for the new cover + int nCubes; // the number of cubes + Min_Cube_t ** ppStore; // storage for cubes by number of literals +}; + +struct Min_Cube_t_ +{ + Min_Cube_t * pNext; // the pointer to the next cube in the cover + unsigned nVars : 10; // the number of variables + unsigned nWords : 12; // the number of machine words + unsigned nLits : 10; // the number of literals in the cube + unsigned uData[1]; // the bit-data for the cube +}; + + +// iterators through the entries in the linked lists of cubes +#define Min_CoverForEachCube( pCover, pCube ) \ + for ( pCube = pCover; \ + pCube; \ + pCube = pCube->pNext ) +#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \ + for ( pCube = pCover, \ + pCube2 = pCube? pCube->pNext: NULL; \ + pCube; \ + pCube = pCube2, \ + pCube2 = pCube? pCube->pNext: NULL ) +#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev ) \ + for ( pCube = pCover, \ + ppPrev = &(pCover); \ + pCube; \ + ppPrev = &pCube->pNext, \ + pCube = pCube->pNext ) + +// macros to get hold of bits and values in the cubes +static inline int Min_CubeHasBit( Min_Cube_t * p, int i ) { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Min_CubeSetBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] |= (1<<((i) & 31)); } +static inline void Min_CubeXorBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] ^= (1<<((i) & 31)); } +static inline int Min_CubeGetVar( Min_Cube_t * p, int Var ) { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); } +static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31)); } + +/*=== xyzMinEsop.c ==========================================================*/ +extern void Min_EsopMinimize( Min_Man_t * p ); +extern int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +/*=== xyzMinSop.c ==========================================================*/ +extern void Min_SopMinimize( Min_Man_t * p ); +extern int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +/*=== xyzMinMan.c ==========================================================*/ +extern Min_Man_t * Min_ManAlloc( int nVars ); +extern void Min_ManClean( Min_Man_t * p, int nSupp ); +extern void Min_ManFree( Min_Man_t * p ); +/*=== xyzMinUtil.c ==========================================================*/ +extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ); +extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ); +extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); +extern void Min_CoverCheck( Min_Man_t * p ); +extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ); +extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ); +extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p ) +{ + Min_Cube_t * pCube; + pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan ); + pCube->pNext = NULL; + pCube->nVars = p->nVars; + pCube->nWords = p->nWords; + pCube->nLits = 0; + memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Creates the cube representing elementary var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl ) +{ + Min_Cube_t * pCube; + pCube = Min_CubeAlloc( p ); + Min_CubeXorBit( pCube, iVar*2+fCompl ); + pCube->nLits = 1; + return pCube; +} + +/**Function************************************************************* + + Synopsis [Creates the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy ) +{ + Min_Cube_t * pCube; + pCube = Min_CubeAlloc( p ); + memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Recycles the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube ) +{ + Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); +} + +/**Function************************************************************* + + Synopsis [Recycles the cube cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube, * pCube2; + Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); +} + + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeCountLits( Min_Cube_t * pCube ) +{ + unsigned uData; + int Count = 0, i, w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Count++; + } + return Count; +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits ) +{ + unsigned uData; + int i, w; + Vec_IntClear( vLits ); + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Vec_IntPush( vLits, w*16 + i/2 ); + } +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CoverCountCubes( Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube; + int Count = 0; + Min_CoverForEachCube( pCover, pCube ) + Count++; + return Count; +} + + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + unsigned uData; + int i; + assert( pCube0->nVars == pCube1->nVars ); + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] & pCube1->uData[i]; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( uData != 0x55555555 ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Collects the disjoint variables of the two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars ) +{ + unsigned uData; + int i, w; + Vec_IntClear( vVars ); + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555; + uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1)); + if ( uData == 0 ) + continue; + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Vec_IntPush( vVars, w*16 + i/2 ); + } +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp ) +{ + unsigned uData; + int i, fFound = 0; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] ^ pCube1->uData[i]; + if ( uData == 0 ) + { + if ( pTemp ) pTemp->uData[i] = 0; + continue; + } + if ( fFound ) + return 0; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( (uData & (uData-1)) > 0 ) // more than one 1 + return 0; + if ( pTemp ) pTemp->uData[i] = uData | (uData << 1); + fFound = 1; + } + if ( fFound == 0 ) + { + printf( "\n" ); + Min_CubeWrite( stdout, pCube0 ); + Min_CubeWrite( stdout, pCube1 ); + printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 ) +{ + unsigned uData;//, uData2; + int i, k, Var0 = -1, Var1 = -1; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] ^ pCube1->uData[i]; + if ( uData == 0 ) + continue; + if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s + return 0; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 ) + return 0; + for ( k = 0; k < 32; k += 2 ) + if ( uData & (1 << k) ) + { + if ( Var0 == -1 ) + Var0 = 16 * i + k/2; + else if ( Var1 == -1 ) + Var1 = 16 * i + k/2; + else + return 0; + } + /* + if ( Var0 >= 0 ) + { + uData &= 0xFFFF; + uData2 = (uData >> 16); + if ( uData && uData2 ) + return 0; + if ( uData ) + { + } + uData }= uData2; + uData &= 0x + } + */ + } + if ( Var0 >= 0 && Var1 >= 0 ) + { + *pVar0 = Var0; + *pVar1 = Var1; + return 1; + } + if ( Var0 == -1 || Var1 == -1 ) + { + printf( "\n" ); + Min_CubeWrite( stdout, pCube0 ); + Min_CubeWrite( stdout, pCube1 ); + printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + Min_Cube_t * pCube; + int i; + assert( pCube0->nVars == pCube1->nVars ); + pCube = Min_CubeAlloc( p ); + for ( i = 0; i < p->nWords; i++ ) + pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i]; + pCube->nLits = Min_CubeCountLits( pCube ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + Min_Cube_t * pCube; + int i; + assert( pCube0->nVars == pCube1->nVars ); + pCube = Min_CubeAlloc( p ); + for ( i = 0; i < p->nWords; i++ ) + pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i]; + pCube->nLits = Min_CubeCountLits( pCube ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + int i; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + if ( pCube0->uData[i] != pCube1->uData[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + int i; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Transforms the cube into the result of merging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask ) +{ + int w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w]; + pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]); + } +} + + + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube, * pCube2, * pThis; + if ( pCover == NULL ) + { + Min_ManClean( p, p->nVars ); + return; + } + Min_ManClean( p, pCover->nVars ); + Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + { + // go through the linked list + Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + Min_CubeRecycle( p, pCube ); + break; + } + if ( pThis != NULL ) + continue; + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + } +} + +/**Function************************************************************* + + Synopsis [Check if the cube is equal or dist1 or contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew ) +{ + Min_Cube_t * pCube; + int i; + // check identity + Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) + if ( Min_CubesAreEqual( pCube, pNew ) ) + return 1; + // check containment + for ( i = 0; i < (int)pNew->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pCube ) + if ( Min_CubeIsContained( pCube, pNew ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Check if the cube is equal or dist1 or contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew ) +{ + Min_Cube_t * pCube; + Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) + if ( Min_CubesDistOne( pCube, pNew, NULL ) ) + return pCube; + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMan.c b/src/opt/xyz/xyzMan.c new file mode 100644 index 00000000..844e8c13 --- /dev/null +++ b/src/opt/xyz/xyzMan.c @@ -0,0 +1,144 @@ +/**CFile**************************************************************** + + FileName [xyzMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Decomposition manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax ) +{ + Xyz_Man_t * pMan; + Xyz_Obj_t * pMem; + Abc_Obj_t * pObj; + int i; + assert( pNtk->pManCut == NULL ); + + // start the manager + pMan = ALLOC( Xyz_Man_t, 1 ); + memset( pMan, 0, sizeof(Xyz_Man_t) ); + pMan->nFaninMax = nFaninMax; + pMan->nCubesMax = 2 * pMan->nFaninMax; + pMan->nWords = Abc_BitWordNum( nFaninMax * 2 ); + + // get the cubes + pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax ); + pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax ); + pMan->vPairs0 = Vec_IntAlloc( nFaninMax ); + pMan->vPairs1 = Vec_IntAlloc( nFaninMax ); + pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 ); + pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 ); + + // allocate memory for object structures + pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) ); + memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) ); + // allocate storage for the pointers to the memory + pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) ); + Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL ); + Abc_NtkForEachObj( pNtk, pObj, i ) + Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i ); + // create the cube manager + pMan->pManMin = Min_ManAlloc( nFaninMax ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Xyz_ManFree( Xyz_Man_t * p ) +{ + Vec_Int_t * vSupp; + int i; + for ( i = 0; i < p->vObjStrs->nSize; i++ ) + { + vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp; + if ( vSupp ) Vec_IntFree( vSupp ); + } + + Min_ManFree( p->pManMin ); + Vec_PtrFree( p->vObjStrs ); + Vec_IntFree( p->vFanCounts ); + Vec_IntFree( p->vTriv0 ); + Vec_IntFree( p->vTriv1 ); + Vec_IntFree( p->vComTo0 ); + Vec_IntFree( p->vComTo1 ); + Vec_IntFree( p->vPairs0 ); + Vec_IntFree( p->vPairs1 ); + free( p->pMemory ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Drop the covers at the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ) +{ + int nFanouts; + assert( p->vFanCounts ); + nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id ); + assert( nFanouts > 0 ); + if ( --nFanouts == 0 ) + { + Vec_IntFree( Abc_ObjGetSupp(pObj) ); + Abc_ObjSetSupp( pObj, NULL ); + Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) ); + Abc_ObjSetCover2( pObj, NULL ); + p->nSupps--; + } + Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c new file mode 100644 index 00000000..114e28a6 --- /dev/null +++ b/src/opt/xyz/xyzMinEsop.c @@ -0,0 +1,277 @@ +/**CFile**************************************************************** + + FileName [xyzMinEsop.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [ESOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Min_EsopRewrite( Min_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_EsopMinimize( Min_Man_t * p ) +{ + int nCubesInit, nCubesOld, nIter; + if ( p->nCubes < 3 ) + return; + nIter = 0; + nCubesInit = p->nCubes; + do { + nCubesOld = p->nCubes; + Min_EsopRewrite( p ); + nIter++; + } + while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); + +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of rewriting using distance 2 cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_EsopRewrite( Min_Man_t * p ) +{ + Min_Cube_t * pCube, ** ppPrev; + Min_Cube_t * pThis, ** ppPrevT; + int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld; + int nPairs = 0; + + // insert the bubble before the first cube + p->pBubble->pNext = p->ppStore[0]; + p->ppStore[0] = p->pBubble; + p->pBubble->nLits = 0; + + // go through the cubes + while ( 1 ) + { + // get the index of the bubble + Index = p->pBubble->nLits; + + // find the bubble + Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) + if ( pCube == p->pBubble ) + break; + assert( pCube == p->pBubble ); + + // remove the bubble, get the next cube after the bubble + *ppPrev = p->pBubble->pNext; + pCube = p->pBubble->pNext; + if ( pCube == NULL ) + for ( Index++; Index <= p->nVars; Index++ ) + if ( p->ppStore[Index] ) + { + ppPrev = &(p->ppStore[Index]); + pCube = p->ppStore[Index]; + break; + } + // stop if there is no more cubes + if ( pCube == NULL ) + break; + + // find the first dist2 cube + Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars ) + Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars - 1 ) + Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + // continue if there is no dist2 cube + if ( pThis == NULL ) + { + // insert the bubble after the cube + p->pBubble->pNext = pCube->pNext; + pCube->pNext = p->pBubble; + p->pBubble->nLits = pCube->nLits; + continue; + } + nPairs++; + + // remove the cubes, insert the bubble instead of pCube + *ppPrevT = pThis->pNext; + *ppPrev = p->pBubble; + p->pBubble->pNext = pCube->pNext; + p->pBubble->nLits = pCube->nLits; + p->nCubes -= 2; + + // Exorlink-2: + // A{v00} B{v01} + A{v10} B{v11} = + // A{v00+v10} B{v01} + A{v10} B{v01+v11} = + // A{v00} B{v01+v11} + A{v00+v10} B{v11} + + // save the dist2 parameters + v00 = Min_CubeGetVar( pCube, Var0 ); + v01 = Min_CubeGetVar( pCube, Var1 ); + v10 = Min_CubeGetVar( pThis, Var0 ); + v11 = Min_CubeGetVar( pThis, Var1 ); +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + + // derive the first pair of resulting cubes + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits -= (v00 != 3); + pCube->nLits += ((v00 ^ v10) != 3); + Min_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits -= (v11 != 3); + pThis->nLits += ((v01 ^ v11) != 3); + + // add the cubes + nCubesOld = p->nCubes; + while ( Min_EsopAddCube( p, pCube ) ); + while ( Min_EsopAddCube( p, pThis ) ); + // check if the cubes were absorbed + if ( p->nCubes < nCubesOld + 2 ) + continue; + + // pull out both cubes + assert( pThis == p->ppStore[pThis->nLits] ); + p->ppStore[pThis->nLits] = pThis->pNext; + assert( pCube == p->ppStore[pCube->nLits] ); + p->ppStore[pCube->nLits] = pCube->pNext; + p->nCubes -= 2; + + // derive the second pair of resulting cubes + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits -= ((v00 ^ v10) != 3); + pCube->nLits += (v00 != 3); + Min_CubeXorVar( pCube, Var1, v11 ); + pCube->nLits -= (v01 != 3); + pCube->nLits += ((v01 ^ v11) != 3); + + Min_CubeXorVar( pThis, Var0, v00 ); + pThis->nLits -= (v10 != 3); + pThis->nLits += ((v00 ^ v10) != 3); + Min_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits -= ((v01 ^ v11) != 3); + pThis->nLits += (v11 != 3); + + // add them anyhow + while ( Min_EsopAddCube( p, pCube ) ); + while ( Min_EsopAddCube( p, pThis ) ); + } +// printf( "Pairs = %d ", nPairs ); +} + +/**Function************************************************************* + + Synopsis [Adds the cube to storage.] + + Description [If the distance one cube is found, returns the transformed + cube. If there is no distance one, adds the given cube to storage. + Do not forget to clean the storage!] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +{ + Min_Cube_t * pThis, ** ppPrev; + // try to find the identical cube + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + *ppPrev = pThis->pNext; + Min_CubeRecycle( p, pCube ); + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 0; + } + } + // find a distance-1 cube if it exists + if ( pCube->nLits < pCube->nVars ) + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransform( pCube, pThis, p->pTemp ); + pCube->nLits++; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransform( pCube, pThis, p->pTemp ); + pCube->nLits--; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + if ( pCube->nLits > 0 ) + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransform( pCube, pThis, p->pTemp ); + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + // add the cube + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c new file mode 100644 index 00000000..423564c1 --- /dev/null +++ b/src/opt/xyz/xyzMinMan.c @@ -0,0 +1,112 @@ +/**CFile**************************************************************** + + FileName [xyzMinMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [SOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Man_t * Min_ManAlloc( int nVars ) +{ + Min_Man_t * pMan; + // start the manager + pMan = ALLOC( Min_Man_t, 1 ); + memset( pMan, 0, sizeof(Min_Man_t) ); + pMan->nVars = nVars; + pMan->nWords = Abc_BitWordNum( nVars * 2 ); + pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) ); + // allocate storage for the temporary cover + pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 ); + // create tautology cubes + Min_ManClean( pMan, nVars ); + pMan->pOne0 = Min_CubeAlloc( pMan ); + pMan->pOne1 = Min_CubeAlloc( pMan ); + pMan->pTemp = Min_CubeAlloc( pMan ); + pMan->pBubble = Min_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0; + // create trivial cubes + Min_ManClean( pMan, 1 ); + pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 ); + pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 ); + pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 ); + pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Cleans the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_ManClean( Min_Man_t * p, int nSupp ) +{ + // set the size of the cube manager + p->nVars = nSupp; + p->nWords = Abc_BitWordNum(2*nSupp); + // clean the storage + memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) ); + p->nCubes = 0; +} + +/**Function************************************************************* + + Synopsis [Stops the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_ManFree( Min_Man_t * p ) +{ + Extra_MmFixedStop ( p->pMemMan, 0 ); + free( p->ppStore ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c new file mode 100644 index 00000000..1c5951fe --- /dev/null +++ b/src/opt/xyz/xyzMinSop.c @@ -0,0 +1,341 @@ +/**CFile**************************************************************** + + FileName [xyzMinSop.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [SOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Min_SopRewrite( Min_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopMinimize( Min_Man_t * p ) +{ + int nCubesInit, nCubesOld, nIter; + if ( p->nCubes < 3 ) + return; + nIter = 0; + nCubesInit = p->nCubes; + do { + nCubesOld = p->nCubes; + Min_SopRewrite( p ); + nIter++; + } + while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); + +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopRewrite( Min_Man_t * p ) +{ + Min_Cube_t * pCube, ** ppPrev; + Min_Cube_t * pThis, ** ppPrevT; + Min_Cube_t * pTemp; + int v00, v01, v10, v11, Var0, Var1, Index; + int nPairs = 0; + + // insert the bubble before the first cube + p->pBubble->pNext = p->ppStore[0]; + p->ppStore[0] = p->pBubble; + p->pBubble->nLits = 0; + + // go through the cubes + while ( 1 ) + { + // get the index of the bubble + Index = p->pBubble->nLits; + + // find the bubble + Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) + if ( pCube == p->pBubble ) + break; + assert( pCube == p->pBubble ); + + // remove the bubble, get the next cube after the bubble + *ppPrev = p->pBubble->pNext; + pCube = p->pBubble->pNext; + if ( pCube == NULL ) + for ( Index++; Index <= p->nVars; Index++ ) + if ( p->ppStore[Index] ) + { + ppPrev = &(p->ppStore[Index]); + pCube = p->ppStore[Index]; + break; + } + // stop if there is no more cubes + if ( pCube == NULL ) + break; + + // find the first dist2 cube + Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars ) + Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + // continue if there is no dist2 cube + if ( pThis == NULL ) + { + // insert the bubble after the cube + p->pBubble->pNext = pCube->pNext; + pCube->pNext = p->pBubble; + p->pBubble->nLits = pCube->nLits; + continue; + } + nPairs++; + + // remove the cubes, insert the bubble instead of pCube + *ppPrevT = pThis->pNext; + *ppPrev = p->pBubble; + p->pBubble->pNext = pCube->pNext; + p->pBubble->nLits = pCube->nLits; + p->nCubes -= 2; + + + // save the dist2 parameters + v00 = Min_CubeGetVar( pCube, Var0 ); + v01 = Min_CubeGetVar( pCube, Var1 ); + v10 = Min_CubeGetVar( pThis, Var0 ); + v11 = Min_CubeGetVar( pThis, Var1 ); + assert( v00 != v10 && v01 != v11 ); + assert( v00 != 3 || v01 != 3 ); + assert( v10 != 3 || v11 != 3 ); + + // skip the case when rewriting is impossible + if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 ) + continue; + + // if one of them does not have DC lit, move it + if ( v00 != 3 && v01 != 3 ) + { + pTemp = pCube; pCube = pThis; pThis = pTemp; + Index = v00; v00 = v10; v10 = Index; + Index = v01; v01 = v11; v11 = Index; + } + +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + + // make sure the first cube has first var DC + if ( v00 != 3 ) + { + assert( v01 == 3 ); + Index = Var0; Var0 = Var1; Var1 = Index; + Index = v00; v00 = v01; v01 = Index; + Index = v10; v10 = v11; v11 = Index; + } + + // consider both cases: both have DC lit + if ( v00 == 3 && v11 == 3 ) + { + assert( v01 != 3 && v10 != 3 ); + // try two reduced cubes + + } + else // the first cube has DC lit + { + assert( v01 != 3 && v10 != 3 && v11 != 3 ); + // try reduced and expanded cube + } + } +// printf( "Pairs = %d ", nPairs ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +{ + return 1; +} + + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopDist1Merge( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pCube2, * pCubeNew; + int i; + for ( i = p->nVars; i >= 0; i-- ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + Min_CoverForEachCube( pCube->pNext, pCube2 ) + { + assert( pCube->nLits == pCube2->nLits ); + if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) + continue; + pCubeNew = Min_CubesXor( p, pCube, pCube2 ); + assert( pCubeNew->nLits == pCube->nLits - 1 ); + pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; + p->ppStore[pCubeNew->nLits] = pCubeNew; + p->nCubes++; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopContain( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pCube2, ** ppPrev; + int i, k; + for ( i = 0; i <= p->nVars; i++ ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev ) + { + if ( !Min_CubesAreEqual( pCube, pCube2 ) ) + continue; + *ppPrev = pCube2->pNext; + Min_CubeRecycle( p, pCube2 ); + p->nCubes--; + } + for ( k = i + 1; k <= p->nVars; k++ ) + Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev ) + { + if ( !Min_CubeIsContained( pCube, pCube2 ) ) + continue; + *ppPrev = pCube2->pNext; + Min_CubeRecycle( p, pCube2 ); + p->nCubes--; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) +{ + Vec_Int_t * vVars; + Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev; + int Num, Value, i; + + // get the variables + vVars = Vec_IntAlloc( 100 ); + // create the tautology cube + pCover = Min_CubeAlloc( p ); + // sharp it with all cubes + Min_CoverForEachCube( pSharp, pCube ) + Min_CoverForEachCubePrev( pCover, pThis, ppPrev ) + { + if ( Min_CubesDisjoint( pThis, pCube ) ) + continue; + // remember the next pointer + pNext = pThis->pNext; + // get the variables, in which pThis is '-' while pCube is fixed + Min_CoverGetDisjVars( pThis, pCube, vVars ); + // generate the disjoint cubes + pReady = pThis; + Vec_IntForEachEntryReverse( vVars, Num, i ) + { + // correct the literal + Min_CubeXorVar( pReady, vVars->pArray[i], 3 ); + if ( i == 0 ) + break; + // create the new cube and clean this value + Value = Min_CubeGetVar( pReady, vVars->pArray[i] ); + pReady = Min_CubeDup( p, pReady ); + Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value ); + // add to the cover + *ppPrev = pReady; + ppPrev = &pReady->pNext; + } + pThis = pReady; + pThis->pNext = pNext; + } + Vec_IntFree( vVars ); + + // perform dist-1 merge and contain + Min_CoverExpandRemoveEqual( p, pCover ); + Min_SopDist1Merge( p ); + Min_SopContain( p ); + return Min_CoverCollect( p, p->nVars ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c new file mode 100644 index 00000000..0aebb815 --- /dev/null +++ b/src/opt/xyz/xyzMinUtil.c @@ -0,0 +1,225 @@ +/**CFile**************************************************************** + + FileName [xyzMinUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ) +{ + int i; + assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); + for ( i = 0; i < (int)pCube->nVars; i++ ) + if ( Min_CubeHasBit(pCube, i*2) ) + { + if ( Min_CubeHasBit(pCube, i*2+1) ) + fprintf( pFile, "-" ); + else + fprintf( pFile, "0" ); + } + else + { + if ( Min_CubeHasBit(pCube, i*2+1) ) + fprintf( pFile, "1" ); + else + fprintf( pFile, "?" ); + } + fprintf( pFile, " 1\n" ); +// fprintf( pFile, " %d\n", pCube->nLits ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube; + Min_CoverForEachCube( pCover, pCube ) + Min_CubeWrite( pFile, pCube ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) +{ + char Buffer[1000]; + Min_Cube_t * pCube; + FILE * pFile; + int i; + sprintf( Buffer, "%s.esop", pName ); + for ( i = strlen(Buffer) - 1; i >= 0; i-- ) + if ( Buffer[i] == '<' || Buffer[i] == '>' ) + Buffer[i] = '_'; + pFile = fopen( Buffer, "w" ); + fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() ); + fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 ); + fprintf( pFile, ".o %d\n", 1 ); + fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) ); + if ( fEsop ) fprintf( pFile, ".type esop\n" ); + Min_CoverForEachCube( pCover, pCube ) + Min_CubeWrite( pFile, pCube ); + fprintf( pFile, ".e\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of rewriting using distance 2 cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverCheck( Min_Man_t * p ) +{ + Min_Cube_t * pCube; + int i; + for ( i = 0; i <= p->nVars; i++ ) + Min_CoverForEachCube( p->ppStore[i], pCube ) + assert( i == (int)pCube->nLits ); +} + + +/**Function************************************************************* + + Synopsis [Converts the cover from the sorted structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ) +{ + Min_Cube_t * pCov = NULL, ** ppTail = &pCov; + Min_Cube_t * pCube, * pCube2; + int i; + for ( i = 0; i <= nSuppSize; i++ ) + { + Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 ) + { + assert( i == (int)pCube->nLits ); + *ppTail = pCube; + ppTail = &pCube->pNext; + } + } + *ppTail = NULL; + return pCov; +} + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube, * pCube2; + Min_ManClean( p, p->nVars ); + Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + { + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + } +} + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube; + int i, Counter; + if ( pCover == NULL ) + return 0; + // clean the cube + for ( i = 0; i < (int)pCover->nWords; i++ ) + p->pTemp->uData[i] = ~((unsigned)0); + // add the bit data + Min_CoverForEachCube( pCover, pCube ) + for ( i = 0; i < (int)pCover->nWords; i++ ) + p->pTemp->uData[i] &= pCube->uData[i]; + // count the vars + Counter = 0; + for ( i = 0; i < (int)pCover->nVars; i++ ) + Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 ); + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c new file mode 100644 index 00000000..6c0a63f3 --- /dev/null +++ b/src/opt/xyz/xyzTest.c @@ -0,0 +1,51 @@ +/**CFile**************************************************************** + + FileName [xyzTest.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Testing procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ) +{ + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |