diff options
Diffstat (limited to 'src/bool/kit/kitIsop.c')
| -rw-r--r-- | src/bool/kit/kitIsop.c | 330 |
1 files changed, 330 insertions, 0 deletions
diff --git a/src/bool/kit/kitIsop.c b/src/bool/kit/kitIsop.c new file mode 100644 index 00000000..fc017c0e --- /dev/null +++ b/src/bool/kit/kitIsop.c @@ -0,0 +1,330 @@ +/**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 ) + { + 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; +} + +/**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->nCubes = 0; + pcRes->pCubes = NULL; + Kit_TruthClear( pTemp, nVars ); + return pTemp; + } + if ( Kit_TruthIsConst1( puOnDc, nVars ) ) + { + 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->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->nCubes = 0; + pcRes->pCubes = NULL; + return 0; + } + if ( uOnDc == 0xFFFFFFFF ) + { + 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->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 + |