diff options
| -rw-r--r-- | src/base/abci/abcFx.c | 88 |
1 files changed, 71 insertions, 17 deletions
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 727bf263..6c770592 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [Interface with the fast_extract package.] + Synopsis [Implementation of traditional "fast_extract" algorithm.] Author [Alan Mishchenko] @@ -29,6 +29,59 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/* + The code in this file implements the traditional "fast_extract" algorithm, + which extracts two-cube divisors concurrently with single-cube two-literal divisors, + as proposed in the TCAD'92 paper by J. Rajski and J. Vasudevamurthi. + + Integration notes: + + It is assumed that each object (primary input or internal node) in the original network + is associated with a unique integer number, called object identifier (ObjId, for short). + + The user's input data given to 'fast_extract" is an array of cubes (pMan->vCubes). + Each cube is an array of integers, in which the first entry contains ObjId of the node, + to which this cube belongs in the original network. The following entries of a cube are + SOP literals of this cube. Each literal is represtned as 2*FaninId + ComplAttr, where FaninId + is ObjId of the fanin node and ComplAttr is 1 if literal is complemented, and 0 otherwise. + + The user's output data produced by 'fast_extract' is also an array of cubes (pMan->vCubes). + If no divisors have been extracted, the output array is the same as the input array. + If some divisors have been extracted, the output array contains updated old cubes and new cubes + representing the extracted divisors. The new divisors have their ObjId starting from the + largest ObjId used in the cubes. To give the user more flexibility, which may be needed when some + ObjIds are already used for primary output nodes, which do not participate in fast_extract, + the parameter ObjIdMax is passed to procedure Fx_FastExtract(). The new divisors will receive + their ObjId starting from ObjIdMax onward, as divisor extaction proceeds. + + The following two requirements are imposed on the input and output array of cubes: + (1) The array of cubes should be sorted by the first entry in each cube (that is, cubes belonging + to the same node should form a contiguous range). + (2) Literals in a cube should be sorted in the increasing order of the integer numbers. + + To integrate this code into a calling application, such as ABC, the input cube array should + be generated (below this is done by the procedure Abc_NtkFxRetrieve) and the output cube array + should be incorporated into the current network (below this is done by the procedure Abc_NtkFxInsert). + In essence, the latter procedure performs the following: + - removes the current fanins and SOPs of each node in the network + - adds new nodes for each new divisor introduced by "fast_extract" + - populates fanins and SOPs of each node, both old and new, as indicaded by the resulting cube array. + + Implementation notes: + + The implementation is optimized for simplicity and speed of computation. + (1) Main input/output data-structure (pMan->vCubes) is the array of cubes which is dynamically updated by the algorithm. + (2) Auxiliary data-structure (pMan->vLits) is the array of arrays. The i-th array contains IDs of cubes which have literal i. + It may be convenient to think about the first (second) array as rows (columns) of a sparse matrix, + although the sparse matrix data-structure is not used in the proposed implementation. + (3) Hash table (pMan->pHash) hashes the normalized divisors (represented as integer arrays) into integer numbers. + (4) Array of divisor weights (pMan->vWeights), that is, the number of SOP literals to be saved by extacting each divisor. + (5) Priority queue (pMan->vPrio), which sorts divisor (integer numbers) by their weight + (6) Integer array (pMan->vVarCube), which maps each ObjId into the first cube of this object, + or -1, if there is no cubes as in the case of a primary input. + +*/ + typedef struct Fx_Man_t_ Fx_Man_t; struct Fx_Man_t_ { @@ -36,22 +89,23 @@ struct Fx_Man_t_ Vec_Wec_t * vCubes; // cube -> lit // internal data Vec_Wec_t * vLits; // lit -> cube - Vec_Int_t * vCounts; // literal counts (currently unused) - Hsh_VecMan_t * pHash; // hash table of divisors + Vec_Int_t * vCounts; // literal counts (currently not used) + Hsh_VecMan_t * pHash; // hash table for normalized divisors Vec_Flt_t * vWeights; // divisor weights - Vec_Que_t * vPrio; // priority queue - Vec_Int_t * vVarCube; // mapping var into its first cube - // temporary arrays used for updating data-structure after one extraction + Vec_Que_t * vPrio; // priority queue for divisors by weight + Vec_Int_t * vVarCube; // mapping ObjId into its first cube + // temporary data to update the data-structure when a divisor is extracted Vec_Int_t * vCubesS; // single cubes for the given divisor Vec_Int_t * vCubesD; // cube pairs for the given divisor - Vec_Int_t * vCompls; // complements of cube pairs + Vec_Int_t * vCompls; // complemented attribute of each cube pair Vec_Int_t * vCubeFree; // cube-free divisor - Vec_Int_t * vDiv; // divisor + Vec_Int_t * vDiv; // selected divisor // statistics clock_t timeStart; // starting time int nVars; // original problem variables int nLits; // the number of SOP literals int nDivs; // the number of extracted divisors + int nCompls; // the number of complements int nPairsS; // number of lit pairs int nPairsD; // number of cube pairs int nDivsS; // single cube divisors @@ -63,8 +117,6 @@ static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { ret #define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ ) -static int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -248,6 +300,7 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk ) ***********************************************************************/ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose ) { + extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int fVerbose ); Vec_Wec_t * vCubes; assert( Abc_NtkIsSopLogic(pNtk) ); // check unique fanins @@ -372,8 +425,9 @@ static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv ) printf( "%4d : ", p->nDivs ); printf( "Div %7d : ", iDiv ); printf( "Weight %5d ", (int)Vec_FltEntry(p->vWeights, iDiv) ); +// printf( "Compl %4d ", p->nCompls ); Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) ); - for ( i = Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) + 3; i < 20; i++ ) + for ( i = Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) + 3; i < 16; i++ ) printf( " " ); printf( "Lits =%7d ", p->nLits ); printf( "Divs =%8d ", Hsh_VecSize(p->pHash) ); @@ -873,7 +927,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) Vec_Int_t * vCube, * vCube2, * vLitP, * vLitN; Vec_Int_t * vDiv = p->vDiv; int nLitsNew = p->nLits - (int)Vec_FltEntry(p->vWeights, iDiv); - int i, k, Lit0, Lit1, iVarNew, fComplAny, RetValue; + int i, k, Lit0, Lit1, iVarNew, RetValue; // get the divisor and select pivot variables p->nDivs++; @@ -952,13 +1006,13 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) } // create updated double-cube divisor cube pairs k = 0; - fComplAny = 0; + p->nCompls = 0; assert( Vec_IntSize(p->vCubesD) % 2 == 0 ); assert( Vec_IntSize(p->vCubesD) == 2 * Vec_IntSize(p->vCompls) ); for ( i = 0; i < Vec_IntSize(p->vCubesD); i += 2 ) { int fCompl = Vec_IntEntry(p->vCompls, i/2); - fComplAny |= fCompl; + p->nCompls += fCompl; vCube = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i) ); vCube2 = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i+1) ); RetValue = Fx_ManDivRemoveLits( vCube, vDiv, fCompl ); // cube 2*i @@ -1020,7 +1074,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) Vec_IntForEachEntry( vDiv, Lit0, i ) { Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_Lit2Var(Lit0)), p->vCubesD ); - if ( fComplAny && i > 1 ) // the last two lits are possibly complemented + if ( p->nCompls && i > 1 ) // the last two lits are possibly complemented Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_LitNot(Abc_Lit2Var(Lit0))), p->vCubesD ); } @@ -1041,14 +1095,14 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv ) SeeAlso [] ***********************************************************************/ -int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose ) +int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int fVerbose ) { int fVeryVerbose = 0; Fx_Man_t * p; clock_t clk = clock(); // initialize the data-structure p = Fx_ManStart( vCubes ); - Fx_ManCreateLiterals( p, nVars ); + Fx_ManCreateLiterals( p, ObjIdMax ); Fx_ManCreateDivisors( p ); if ( fVeryVerbose ) Fx_PrintMatrix( p ); |