src/aig/kit/kitIsop.c File Reference

#include "kit.h"
Include dependency graph for kitIsop.c:

Go to the source code of this file.

Defines

#define KIT_ISOP_MEM_LIMIT   (1<<16)

Functions

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)
int Kit_TruthIsop (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)

Define Documentation

#define KIT_ISOP_MEM_LIMIT   (1<<16)

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

] DECLARATIONS ///

Definition at line 28 of file kitIsop.c.

Function Documentation

int Kit_TruthIsop ( unsigned *  puTruth,
int  nVars,
Vec_Int_t *  vMemory,
int  fTryBoth 
)

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 []

Definition at line 52 of file kitIsop.c.

00053 {
00054     Kit_Sop_t cRes, * pcRes = &cRes;
00055     Kit_Sop_t cRes2, * pcRes2 = &cRes2;
00056     unsigned * pResult;
00057     int RetValue = 0;
00058     assert( nVars >= 0 && nVars < 16 );
00059     // if nVars < 5, make sure it does not depend on those vars
00060 //    for ( i = nVars; i < 5; i++ )
00061 //        assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
00062     // prepare memory manager
00063     Vec_IntClear( vMemory );
00064     Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
00065     // compute ISOP for the direct polarity
00066     pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
00067     if ( pcRes->nCubes == -1 )
00068     {
00069         vMemory->nSize = -1;
00070         return -1;
00071     }
00072     assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
00073     if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
00074     {
00075         vMemory->pArray[0] = 0;
00076         Vec_IntShrink( vMemory, pcRes->nCubes );
00077         return 0;
00078     }
00079     if ( fTryBoth )
00080     {
00081         // compute ISOP for the complemented polarity
00082         Kit_TruthNot( puTruth, puTruth, nVars );
00083         pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
00084         if ( pcRes2->nCubes >= 0 )
00085         {
00086             assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
00087             if ( pcRes->nCubes > pcRes2->nCubes )
00088             {
00089                 RetValue = 1;
00090                 pcRes = pcRes2;
00091             }
00092         }
00093         Kit_TruthNot( puTruth, puTruth, nVars );
00094     }
00095 //    printf( "%d ", vMemory->nSize );
00096     // move the cover representation to the beginning of the memory buffer
00097     memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
00098     Vec_IntShrink( vMemory, pcRes->nCubes );
00099     return RetValue;
00100 }

unsigned Kit_TruthIsop5_rec ( unsigned  uOn,
unsigned  uOnDc,
int  nVars,
Kit_Sop_t *  pcRes,
Vec_Int_t *  vStore 
) [static]

Function*************************************************************

Synopsis [Computes ISOP for 5 variables or less.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file kitIsop.c.

00238 {
00239     unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
00240     Kit_Sop_t cRes0, cRes1, cRes2;
00241     Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
00242     unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
00243     int i, k, Var;
00244     assert( nVars <= 5 );
00245     assert( (uOn & ~uOnDc) == 0 );
00246     if ( uOn == 0 )
00247     {
00248         pcRes->nCubes = 0;
00249         pcRes->pCubes = NULL;
00250         return 0;
00251     }
00252     if ( uOnDc == 0xFFFFFFFF )
00253     {
00254         pcRes->nCubes = 1;
00255         pcRes->pCubes = Vec_IntFetch( vStore, 1 );
00256         if ( pcRes->pCubes == NULL )
00257         {
00258             pcRes->nCubes = -1;
00259             return 0;
00260         }
00261         pcRes->pCubes[0] = 0;
00262         return 0xFFFFFFFF;
00263     }
00264     assert( nVars > 0 );
00265     // find the topmost var
00266     for ( Var = nVars-1; Var >= 0; Var-- )
00267         if ( Kit_TruthVarInSupport( &uOn, 5, Var ) || 
00268              Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
00269              break;
00270     assert( Var >= 0 );
00271     // cofactor
00272     uOn0   = uOn1   = uOn;
00273     uOnDc0 = uOnDc1 = uOnDc;
00274     Kit_TruthCofactor0( &uOn0, Var + 1, Var );
00275     Kit_TruthCofactor1( &uOn1, Var + 1, Var );
00276     Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
00277     Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
00278     // solve for cofactors
00279     uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
00280     if ( pcRes0->nCubes == -1 )
00281     {
00282         pcRes->nCubes = -1;
00283         return 0;
00284     }
00285     uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
00286     if ( pcRes1->nCubes == -1 )
00287     {
00288         pcRes->nCubes = -1;
00289         return 0;
00290     }
00291     uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
00292     if ( pcRes2->nCubes == -1 )
00293     {
00294         pcRes->nCubes = -1;
00295         return 0;
00296     }
00297     // create the resulting cover
00298     pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
00299     pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
00300     if ( pcRes->pCubes == NULL )
00301     {
00302         pcRes->nCubes = -1;
00303         return 0;
00304     }
00305     k = 0;
00306     for ( i = 0; i < pcRes0->nCubes; i++ )
00307         pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
00308     for ( i = 0; i < pcRes1->nCubes; i++ )
00309         pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
00310     for ( i = 0; i < pcRes2->nCubes; i++ )
00311         pcRes->pCubes[k++] = pcRes2->pCubes[i];
00312     assert( k == pcRes->nCubes );
00313     // derive the final truth table
00314     uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
00315 //    assert( (uOn & ~uRes2) == 0 );
00316 //    assert( (uRes2 & ~uOnDc) == 0 );
00317     return uRes2;
00318 }

unsigned * Kit_TruthIsop_rec ( unsigned *  puOn,
unsigned *  puOnDc,
int  nVars,
Kit_Sop_t *  pcRes,
Vec_Int_t *  vStore 
) [static]

Function*************************************************************

Synopsis [Computes ISOP 6 variables or more.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file kitIsop.c.

00114 {
00115     Kit_Sop_t cRes0, cRes1, cRes2;
00116     Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
00117     unsigned * puRes0, * puRes1, * puRes2;
00118     unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
00119     int i, k, Var, nWords, nWordsAll;
00120 //    assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
00121     // allocate room for the resulting truth table
00122     nWordsAll = Kit_TruthWordNum( nVars );
00123     pTemp = Vec_IntFetch( vStore, nWordsAll );
00124     if ( pTemp == NULL )
00125     {
00126         pcRes->nCubes = -1;
00127         return NULL;
00128     }
00129     // check for constants
00130     if ( Kit_TruthIsConst0( puOn, nVars ) )
00131     {
00132         pcRes->nCubes = 0;
00133         pcRes->pCubes = NULL;
00134         Kit_TruthClear( pTemp, nVars );
00135         return pTemp;
00136     }
00137     if ( Kit_TruthIsConst1( puOnDc, nVars ) )
00138     {
00139         pcRes->nCubes = 1;
00140         pcRes->pCubes = Vec_IntFetch( vStore, 1 );
00141         if ( pcRes->pCubes == NULL )
00142         {
00143             pcRes->nCubes = -1;
00144             return NULL;
00145         }
00146         pcRes->pCubes[0] = 0;
00147         Kit_TruthFill( pTemp, nVars );
00148         return pTemp;
00149     }
00150     assert( nVars > 0 );
00151     // find the topmost var
00152     for ( Var = nVars-1; Var >= 0; Var-- )
00153         if ( Kit_TruthVarInSupport( puOn, nVars, Var ) || 
00154              Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
00155              break;
00156     assert( Var >= 0 );
00157     // consider a simple case when one-word computation can be used
00158     if ( Var < 5 )
00159     {
00160         unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
00161         for ( i = 0; i < nWordsAll; i++ )
00162             pTemp[i] = uRes;
00163         return pTemp;
00164     }
00165     assert( Var >= 5 );
00166     nWords = Kit_TruthWordNum( Var );
00167     // cofactor
00168     puOn0   = puOn;    puOn1   = puOn + nWords;
00169     puOnDc0 = puOnDc;  puOnDc1 = puOnDc + nWords;
00170     pTemp0  = pTemp;   pTemp1  = pTemp + nWords;
00171     // solve for cofactors
00172     Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
00173     puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
00174     if ( pcRes0->nCubes == -1 )
00175     {
00176         pcRes->nCubes = -1;
00177         return NULL;
00178     }
00179     Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
00180     puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
00181     if ( pcRes1->nCubes == -1 )
00182     {
00183         pcRes->nCubes = -1;
00184         return NULL;
00185     }
00186     Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
00187     Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
00188     Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
00189     Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
00190     puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
00191     if ( pcRes2->nCubes == -1 )
00192     {
00193         pcRes->nCubes = -1;
00194         return NULL;
00195     }
00196     // create the resulting cover
00197     pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
00198     pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
00199     if ( pcRes->pCubes == NULL )
00200     {
00201         pcRes->nCubes = -1;
00202         return NULL;
00203     }
00204     k = 0;
00205     for ( i = 0; i < pcRes0->nCubes; i++ )
00206         pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
00207     for ( i = 0; i < pcRes1->nCubes; i++ )
00208         pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
00209     for ( i = 0; i < pcRes2->nCubes; i++ )
00210         pcRes->pCubes[k++] = pcRes2->pCubes[i];
00211     assert( k == pcRes->nCubes );
00212     // create the resulting truth table
00213     Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
00214     Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
00215     // copy the table if needed
00216     nWords <<= 1;
00217     for ( i = 1; i < nWordsAll/nWords; i++ )
00218         for ( k = 0; k < nWords; k++ )
00219             pTemp[i*nWords + k] = pTemp[k];
00220     // verify in the end
00221 //    assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
00222 //    assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
00223     return pTemp;
00224 }

Generated on Tue Jan 5 12:18:28 2010 for abc70930 by  doxygen 1.6.1