/**CFile**************************************************************** FileName [kitSop.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Computation kit.] Synopsis [Procedures involving SOPs.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - Dec 6, 2006.] Revision [$Id: kitSop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $] ***********************************************************************/ #include "kit.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Creates SOP from the cube array.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory ) { unsigned uCube; int i; // start the cover cResult->nCubes = 0; cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) ); // add the cubes Vec_IntForEachEntry( vInput, uCube, i ) Kit_SopPushCube( cResult, uCube ); } /**Function************************************************************* Synopsis [Creates SOP from the cube array.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nLits, Vec_Int_t * vMemory ) { unsigned uCube, uMask = 0; int i, nCubes = Vec_IntSize(vInput); // start the cover cResult->nCubes = 0; cResult->pCubes = Vec_IntFetch( vMemory, nCubes ); // add the cubes // Vec_IntForEachEntry( vInput, uCube, i ) for ( i = 0; i < nCubes; i++ ) { uCube = Vec_IntEntry( vInput, i ); uMask = ((uCube | (uCube >> 1)) & 0x55555555); uMask |= (uMask << 1); Kit_SopPushCube( cResult, uCube ^ uMask ); } } /**Function************************************************************* Synopsis [Duplicates SOP.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory ) { unsigned uCube; int i; // start the cover cResult->nCubes = 0; cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) ); // add the cubes Kit_SopForEachCube( cSop, uCube, i ) Kit_SopPushCube( cResult, uCube ); } /**Function************************************************************* Synopsis [Derives the quotient of division by literal.] Description [Reduces the cover to be equal to the result of division of the given cover by the literal.] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit ) { unsigned uCube; int i, k = 0; Kit_SopForEachCube( cSop, uCube, i ) { if ( Kit_CubeHasLit(uCube, iLit) ) Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ ); } Kit_SopShrink( cSop, k ); } /**Function************************************************************* Synopsis [Divides cover by one cube.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory ) { unsigned uCube, uDiv; int i; // get the only cube assert( Kit_SopCubeNum(cDiv) == 1 ); uDiv = Kit_SopCube(cDiv, 0); // allocate covers vQuo->nCubes = 0; vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) ); vRem->nCubes = 0; vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) ); // sort the cubes Kit_SopForEachCube( cSop, uCube, i ) { if ( Kit_CubeContains( uCube, uDiv ) ) Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) ); else Kit_SopPushCube( vRem, uCube ); } } /**Function************************************************************* Synopsis [Divides cover by one cube.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory ) { unsigned uCube, uDiv; unsigned uCube2 = 0; // Suppress "might be used uninitialized" unsigned uDiv2, uQuo; int i, i2, k, k2, nCubesRem; assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) ); // consider special case if ( Kit_SopCubeNum(cDiv) == 1 ) { Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory ); return; } // allocate quotient vQuo->nCubes = 0; vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) ); // for each cube of the cover // it either belongs to the quotient or to the remainder Kit_SopForEachCube( cSop, uCube, i ) { // skip taken cubes if ( Kit_CubeIsMarked(uCube) ) continue; // find a matching cube in the divisor uDiv = ~0; Kit_SopForEachCube( cDiv, uDiv, k ) if ( Kit_CubeContains( uCube, uDiv ) ) break; // the cube is not found if ( k == Kit_SopCubeNum(cDiv) ) continue; // the quotient cube exists uQuo = Kit_CubeSharp( uCube, uDiv ); // find corresponding cubes for other cubes of the divisor uDiv2 = ~0; Kit_SopForEachCube( cDiv, uDiv2, k2 ) { if ( k2 == k ) continue; // find a matching cube Kit_SopForEachCube( cSop, uCube2, i2 ) { // skip taken cubes if ( Kit_CubeIsMarked(uCube2) ) continue; // check if the cube can be used if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) ) break; } // the case when the cube is not found if ( i2 == Kit_SopCubeNum(cSop) ) break; } // we did not find some cubes - continue looking at other cubes if ( k2 != Kit_SopCubeNum(cDiv) ) continue; // we found all cubes - add the quotient cube Kit_SopPushCube( vQuo, uQuo ); // mark the first cube Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i ); // mark other cubes that have this quotient Kit_SopForEachCube( cDiv, uDiv2, k2 ) { if ( k2 == k ) continue; // find a matching cube Kit_SopForEachCube( cSop, uCube2, i2 ) { // skip taken cubes if ( Kit_CubeIsMarked(uCube2) ) continue; // check if the cube can be used if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) ) break; } assert( i2 < Kit_SopCubeNum(cSop) ); // the cube is found, mark it // (later we will add all unmarked cubes to the remainder) Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 ); } } // determine the number of cubes in the remainder nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv); // allocate remainder vRem->nCubes = 0; vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem ); // finally add the remaining unmarked cubes to the remainder // and clean the marked cubes in the cover Kit_SopForEachCube( cSop, uCube, i ) { if ( !Kit_CubeIsMarked(uCube) ) { Kit_SopPushCube( vRem, uCube ); continue; } Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i ); } assert( nCubesRem == Kit_SopCubeNum(vRem) ); } /**Function************************************************************* Synopsis [Returns the common cube.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline unsigned Kit_SopCommonCube( Kit_Sop_t * cSop ) { unsigned uMask, uCube; int i; uMask = ~(unsigned)0; Kit_SopForEachCube( cSop, uCube, i ) uMask &= uCube; return uMask; } /**Function************************************************************* Synopsis [Makes the cover cube-free.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopMakeCubeFree( Kit_Sop_t * cSop ) { unsigned uMask, uCube; int i; uMask = Kit_SopCommonCube( cSop ); if ( uMask == 0 ) return; // remove the common cube Kit_SopForEachCube( cSop, uCube, i ) Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i ); } /**Function************************************************************* Synopsis [Checks if the cover is cube-free.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Kit_SopIsCubeFree( Kit_Sop_t * cSop ) { return Kit_SopCommonCube( cSop ) == 0; } /**Function************************************************************* Synopsis [Creates SOP composes of the common cube of the given SOP.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory ) { assert( Kit_SopCubeNum(cSop) > 0 ); cResult->nCubes = 0; cResult->pCubes = Vec_IntFetch( vMemory, 1 ); Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) ); } /**Function************************************************************* Synopsis [Find any literal that occurs more than once.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits ) { unsigned uCube; int i, k, nLitsCur; // go through each literal for ( i = 0; i < nLits; i++ ) { // go through all the cubes nLitsCur = 0; Kit_SopForEachCube( cSop, uCube, k ) if ( Kit_CubeHasLit(uCube, i) ) nLitsCur++; if ( nLitsCur > 1 ) return i; } return -1; } /**Function************************************************************* Synopsis [Find the least often occurring literal.] Description [Find the least often occurring literal among those that occur more than once.] SideEffects [] SeeAlso [] ***********************************************************************/ int Kit_SopWorstLiteral( Kit_Sop_t * cSop, int nLits ) { unsigned uCube; int i, k, iMin, nLitsMin, nLitsCur; int fUseFirst = 1; // go through each literal iMin = -1; nLitsMin = 1000000; for ( i = 0; i < nLits; i++ ) { // go through all the cubes nLitsCur = 0; Kit_SopForEachCube( cSop, uCube, k ) if ( Kit_CubeHasLit(uCube, i) ) nLitsCur++; // skip the literal that does not occur or occurs once if ( nLitsCur < 2 ) continue; // check if this is the best literal if ( fUseFirst ) { if ( nLitsMin > nLitsCur ) { nLitsMin = nLitsCur; iMin = i; } } else { if ( nLitsMin >= nLitsCur ) { nLitsMin = nLitsCur; iMin = i; } } } if ( nLitsMin < 1000000 ) return iMin; return -1; } /**Function************************************************************* Synopsis [Find the least often occurring literal.] Description [Find the least often occurring literal among those that occur more than once.] SideEffects [] SeeAlso [] ***********************************************************************/ int Kit_SopBestLiteral( Kit_Sop_t * cSop, int nLits, unsigned uMask ) { unsigned uCube; int i, k, iMax, nLitsMax, nLitsCur; int fUseFirst = 1; // go through each literal iMax = -1; nLitsMax = -1; for ( i = 0; i < nLits; i++ ) { if ( !Kit_CubeHasLit(uMask, i) ) continue; // go through all the cubes nLitsCur = 0; Kit_SopForEachCube( cSop, uCube, k ) if ( Kit_CubeHasLit(uCube, i) ) nLitsCur++; // skip the literal that does not occur or occurs once if ( nLitsCur < 2 ) continue; // check if this is the best literal if ( fUseFirst ) { if ( nLitsMax < nLitsCur ) { nLitsMax = nLitsCur; iMax = i; } } else { if ( nLitsMax <= nLitsCur ) { nLitsMax = nLitsCur; iMax = i; } } } if ( nLitsMax >= 0 ) return iMax; return -1; } /**Function************************************************************* Synopsis [Computes a level-zero kernel.] Description [Modifies the cover to contain one level-zero kernel.] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopDivisorZeroKernel_rec( Kit_Sop_t * cSop, int nLits ) { int iLit; // find any literal that occurs at least two times iLit = Kit_SopWorstLiteral( cSop, nLits ); if ( iLit == -1 ) return; // derive the cube-free quotient Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover Kit_SopMakeCubeFree( cSop ); // the same cover // call recursively Kit_SopDivisorZeroKernel_rec( cSop, nLits ); // the same cover } /**Function************************************************************* Synopsis [Computes the quick divisor of the cover.] Description [Returns 0, if there is no divisor other than trivial.] SideEffects [] SeeAlso [] ***********************************************************************/ int Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory ) { if ( Kit_SopCubeNum(cSop) <= 1 ) return 0; if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 ) return 0; // duplicate the cover Kit_SopDup( cResult, cSop, vMemory ); // perform the kerneling Kit_SopDivisorZeroKernel_rec( cResult, nLits ); assert( Kit_SopCubeNum(cResult) > 0 ); return 1; } /**Function************************************************************* Synopsis [Create the one-literal cover with the best literal from cSop.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory ) { int iLitBest; // get the best literal iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube ); // start the cover cResult->nCubes = 0; cResult->pCubes = Vec_IntFetch( vMemory, 1 ); // set the cube Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END