diff options
Diffstat (limited to 'src/bool/kit/kitSop.c')
| -rw-r--r-- | src/bool/kit/kitSop.c | 579 |
1 files changed, 579 insertions, 0 deletions
diff --git a/src/bool/kit/kitSop.c b/src/bool/kit/kitSop.c new file mode 100644 index 00000000..21ea69b8 --- /dev/null +++ b/src/bool/kit/kitSop.c @@ -0,0 +1,579 @@ +/**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-ABC_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-ABC_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 + |