| /**CFile**************************************************************** |
| |
| FileName [kitIsop.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Computation kit.] |
| |
| Synopsis [ISOP computation based on Morreale's algorithm.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - Dec 6, 2006.] |
| |
| Revision [$Id: kitIsop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "kit.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // ISOP computation fails if intermediate memory usage exceed this limit |
| #define KIT_ISOP_MEM_LIMIT (1<<20) |
| |
| // static procedures to compute ISOP |
| static unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore ); |
| static unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes ISOP from TT.] |
| |
| Description [Returns the cover in vMemory. Uses the rest of array in vMemory |
| as an intermediate memory storage. Returns the cover with -1 cubes, if the |
| the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of |
| intermediate data).] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ) |
| { |
| Kit_Sop_t cRes, * pcRes = &cRes; |
| Kit_Sop_t cRes2, * pcRes2 = &cRes2; |
| unsigned * pResult; |
| int RetValue = 0; |
| assert( nVars >= 0 && nVars <= 16 ); |
| // if nVars < 5, make sure it does not depend on those vars |
| // for ( i = nVars; i < 5; i++ ) |
| // assert( !Kit_TruthVarInSupport(puTruth, 5, i) ); |
| // prepare memory manager |
| Vec_IntClear( vMemory ); |
| Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT ); |
| // compute ISOP for the direct polarity |
| pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory ); |
| if ( pcRes->nCubes == -1 ) |
| { |
| vMemory->nSize = -1; |
| return -1; |
| } |
| assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) ); |
| if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) ) |
| { |
| vMemory->pArray[0] = 0; |
| Vec_IntShrink( vMemory, pcRes->nCubes ); |
| return 0; |
| } |
| if ( fTryBoth ) |
| { |
| // compute ISOP for the complemented polarity |
| Kit_TruthNot( puTruth, puTruth, nVars ); |
| pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory ); |
| if ( pcRes2->nCubes >= 0 ) |
| { |
| assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) ); |
| if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) ) |
| { |
| RetValue = 1; |
| pcRes = pcRes2; |
| } |
| } |
| Kit_TruthNot( puTruth, puTruth, nVars ); |
| } |
| // printf( "%d ", vMemory->nSize ); |
| // move the cover representation to the beginning of the memory buffer |
| memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) ); |
| Vec_IntShrink( vMemory, pcRes->nCubes ); |
| return RetValue; |
| } |
| void Kit_TruthIsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl ) |
| { |
| int i, k, Entry, Literal; |
| if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) ) |
| { |
| printf( "Constant %d\n", Vec_IntSize(vCover) ); |
| return; |
| } |
| Vec_IntForEachEntry( vCover, Entry, i ) |
| { |
| for ( k = 0; k < nVars; k++ ) |
| { |
| Literal = 3 & (Entry >> (k << 1)); |
| if ( Literal == 1 ) // neg literal |
| printf( "0" ); |
| else if ( Literal == 2 ) // pos literal |
| printf( "1" ); |
| else if ( Literal == 0 ) |
| printf( "-" ); |
| else assert( 0 ); |
| } |
| printf( " %d\n", !fCompl ); |
| } |
| } |
| void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ) |
| { |
| int fCompl = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth ); |
| Kit_TruthIsopPrintCover( vCover, nVars, fCompl ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes ISOP 6 variables or more.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore ) |
| { |
| Kit_Sop_t cRes0, cRes1, cRes2; |
| Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; |
| unsigned * puRes0, * puRes1, * puRes2; |
| unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1; |
| int i, k, Var, nWords, nWordsAll; |
| // assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) ); |
| // allocate room for the resulting truth table |
| nWordsAll = Kit_TruthWordNum( nVars ); |
| pTemp = Vec_IntFetch( vStore, nWordsAll ); |
| if ( pTemp == NULL ) |
| { |
| pcRes->nCubes = -1; |
| return NULL; |
| } |
| // check for constants |
| if ( Kit_TruthIsConst0( puOn, nVars ) ) |
| { |
| pcRes->nLits = 0; |
| pcRes->nCubes = 0; |
| pcRes->pCubes = NULL; |
| Kit_TruthClear( pTemp, nVars ); |
| return pTemp; |
| } |
| if ( Kit_TruthIsConst1( puOnDc, nVars ) ) |
| { |
| pcRes->nLits = 0; |
| pcRes->nCubes = 1; |
| pcRes->pCubes = Vec_IntFetch( vStore, 1 ); |
| if ( pcRes->pCubes == NULL ) |
| { |
| pcRes->nCubes = -1; |
| return NULL; |
| } |
| pcRes->pCubes[0] = 0; |
| Kit_TruthFill( pTemp, nVars ); |
| return pTemp; |
| } |
| assert( nVars > 0 ); |
| // find the topmost var |
| for ( Var = nVars-1; Var >= 0; Var-- ) |
| if ( Kit_TruthVarInSupport( puOn, nVars, Var ) || |
| Kit_TruthVarInSupport( puOnDc, nVars, Var ) ) |
| break; |
| assert( Var >= 0 ); |
| // consider a simple case when one-word computation can be used |
| if ( Var < 5 ) |
| { |
| unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore ); |
| for ( i = 0; i < nWordsAll; i++ ) |
| pTemp[i] = uRes; |
| return pTemp; |
| } |
| assert( Var >= 5 ); |
| nWords = Kit_TruthWordNum( Var ); |
| // cofactor |
| puOn0 = puOn; puOn1 = puOn + nWords; |
| puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords; |
| pTemp0 = pTemp; pTemp1 = pTemp + nWords; |
| // solve for cofactors |
| Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var ); |
| puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore ); |
| if ( pcRes0->nCubes == -1 ) |
| { |
| pcRes->nCubes = -1; |
| return NULL; |
| } |
| Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var ); |
| puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore ); |
| if ( pcRes1->nCubes == -1 ) |
| { |
| pcRes->nCubes = -1; |
| return NULL; |
| } |
| Kit_TruthSharp( pTemp0, puOn0, puRes0, Var ); |
| Kit_TruthSharp( pTemp1, puOn1, puRes1, Var ); |
| Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var ); |
| Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var ); |
| puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore ); |
| if ( pcRes2->nCubes == -1 ) |
| { |
| pcRes->nCubes = -1; |
| return NULL; |
| } |
| // create the resulting cover |
| pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes; |
| pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; |
| pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes ); |
| if ( pcRes->pCubes == NULL ) |
| { |
| pcRes->nCubes = -1; |
| return NULL; |
| } |
| k = 0; |
| for ( i = 0; i < pcRes0->nCubes; i++ ) |
| pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0)); |
| for ( i = 0; i < pcRes1->nCubes; i++ ) |
| pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1)); |
| for ( i = 0; i < pcRes2->nCubes; i++ ) |
| pcRes->pCubes[k++] = pcRes2->pCubes[i]; |
| assert( k == pcRes->nCubes ); |
| // create the resulting truth table |
| Kit_TruthOr( pTemp0, puRes0, puRes2, Var ); |
| Kit_TruthOr( pTemp1, puRes1, puRes2, Var ); |
| // copy the table if needed |
| nWords <<= 1; |
| for ( i = 1; i < nWordsAll/nWords; i++ ) |
| for ( k = 0; k < nWords; k++ ) |
| pTemp[i*nWords + k] = pTemp[k]; |
| // verify in the end |
| // assert( Kit_TruthIsImply( puOn, pTemp, nVars ) ); |
| // assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) ); |
| return pTemp; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes ISOP for 5 variables or less.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore ) |
| { |
| unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; |
| Kit_Sop_t cRes0, cRes1, cRes2; |
| Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; |
| unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2; |
| int i, k, Var; |
| assert( nVars <= 5 ); |
| assert( (uOn & ~uOnDc) == 0 ); |
| if ( uOn == 0 ) |
| { |
| pcRes->nLits = 0; |
| pcRes->nCubes = 0; |
| pcRes->pCubes = NULL; |
| return 0; |
| } |
| if ( uOnDc == 0xFFFFFFFF ) |
| { |
| pcRes->nLits = 0; |
| pcRes->nCubes = 1; |
| pcRes->pCubes = Vec_IntFetch( vStore, 1 ); |
| if ( pcRes->pCubes == NULL ) |
| { |
| pcRes->nCubes = -1; |
| return 0; |
| } |
| pcRes->pCubes[0] = 0; |
| return 0xFFFFFFFF; |
| } |
| assert( nVars > 0 ); |
| // find the topmost var |
| for ( Var = nVars-1; Var >= 0; Var-- ) |
| if ( Kit_TruthVarInSupport( &uOn, 5, Var ) || |
| Kit_TruthVarInSupport( &uOnDc, 5, Var ) ) |
| break; |
| assert( Var >= 0 ); |
| // cofactor |
| uOn0 = uOn1 = uOn; |
| uOnDc0 = uOnDc1 = uOnDc; |
| Kit_TruthCofactor0( &uOn0, Var + 1, Var ); |
| Kit_TruthCofactor1( &uOn1, Var + 1, Var ); |
| Kit_TruthCofactor0( &uOnDc0, Var + 1, Var ); |
| Kit_TruthCofactor1( &uOnDc1, Var + 1, Var ); |
| // solve for cofactors |
| uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore ); |
| if ( pcRes0->nCubes == -1 ) |
| { |
| pcRes->nCubes = -1; |
| return 0; |
| } |
| uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore ); |
| if ( pcRes1->nCubes == -1 ) |
| { |
| pcRes->nCubes = -1; |
| return 0; |
| } |
| uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore ); |
| if ( pcRes2->nCubes == -1 ) |
| { |
| pcRes->nCubes = -1; |
| return 0; |
| } |
| // create the resulting cover |
| pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes; |
| pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; |
| pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes ); |
| if ( pcRes->pCubes == NULL ) |
| { |
| pcRes->nCubes = -1; |
| return 0; |
| } |
| k = 0; |
| for ( i = 0; i < pcRes0->nCubes; i++ ) |
| pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0)); |
| for ( i = 0; i < pcRes1->nCubes; i++ ) |
| pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1)); |
| for ( i = 0; i < pcRes2->nCubes; i++ ) |
| pcRes->pCubes[k++] = pcRes2->pCubes[i]; |
| assert( k == pcRes->nCubes ); |
| // derive the final truth table |
| uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]); |
| // assert( (uOn & ~uRes2) == 0 ); |
| // assert( (uRes2 & ~uOnDc) == 0 ); |
| return uRes2; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
