src/aig/cnf/cnfCut.c File Reference

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

Go to the source code of this file.

Functions

Cnf_Cut_t * Cnf_CutAlloc (Cnf_Man_t *p, int nLeaves)
void Cnf_CutFree (Cnf_Cut_t *pCut)
Cnf_Cut_t * Cnf_CutCreate (Cnf_Man_t *p, Aig_Obj_t *pObj)
void Cnf_CutPrint (Cnf_Cut_t *pCut)
void Cnf_CutDeref (Cnf_Man_t *p, Cnf_Cut_t *pCut)
void Cnf_CutRef (Cnf_Man_t *p, Cnf_Cut_t *pCut)
void Cnf_CutUpdateRefs (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
static int Cnf_CutMergeLeaves (Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int *pFanins)
static unsigned Cnf_TruthPhase (Cnf_Cut_t *pCut, Cnf_Cut_t *pCut1)
void Cnf_CutRemoveIthVar (Cnf_Cut_t *pCut, int iVar, int iFan)
void Cnf_CutInsertIthVar (Cnf_Cut_t *pCut, int iVar, int iFan)
Cnf_Cut_t * Cnf_CutCompose (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)

Function Documentation

Cnf_Cut_t* Cnf_CutAlloc ( Cnf_Man_t *  p,
int  nLeaves 
)

CFile****************************************************************

FileName [cnfCut.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG-to-CNF conversion.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file cnfCut.c.

00044 {
00045     Cnf_Cut_t * pCut;
00046     int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Aig_TruthWordNum(nLeaves);
00047     pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
00048     pCut->nFanins = nLeaves;
00049     pCut->nWords = Aig_TruthWordNum(nLeaves);
00050     pCut->vIsop[0] = pCut->vIsop[1] = NULL;
00051     return pCut;
00052 }

Cnf_Cut_t* Cnf_CutCompose ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
int  iFan 
)

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

Synopsis [Merges two cuts.]

Description [Returns NULL of the cuts cannot be merged.]

SideEffects []

SeeAlso []

Definition at line 291 of file cnfCut.c.

00292 {
00293     Cnf_Cut_t * pCutRes;
00294     static int pFanins[32];
00295     unsigned * pTruth, * pTruthFan, * pTruthRes;
00296     unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
00297     unsigned uPhase, uPhaseFan;
00298     int i, iVar, nFanins, RetValue;
00299 
00300     // make sure the second cut is the fanin of the first
00301     for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
00302         if ( pCut->pFanins[iVar] == iFan )
00303             break;
00304     assert( iVar < pCut->nFanins );
00305     // remove this variable
00306     Cnf_CutRemoveIthVar( pCut, iVar, iFan );
00307     // merge leaves of the cuts
00308     nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
00309     if ( nFanins+1 > p->nMergeLimit )
00310     {
00311         Cnf_CutInsertIthVar( pCut, iVar, iFan );
00312         return NULL;
00313     }
00314     // create new cut
00315     pCutRes = Cnf_CutAlloc( p, nFanins );
00316     memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
00317     assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
00318 
00319     // derive its truth table
00320     // get the truth tables in the composition space
00321     pTruth    = Cnf_CutTruth(pCut);
00322     pTruthFan = Cnf_CutTruth(pCutFan);
00323     pTruthRes = Cnf_CutTruth(pCutRes);
00324     for ( i = 0; i < 2*pCutRes->nWords; i++ )
00325         pTop[i] = pTruth[i % pCut->nWords];
00326     for ( i = 0; i < pCutRes->nWords; i++ )
00327         pFan[i] = pTruthFan[i % pCutFan->nWords];
00328     // move the variable to the end
00329     uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
00330     Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
00331     // compute the phases
00332     uPhase    = Cnf_TruthPhase( pCutRes, pCut    ) | (1 << pCutRes->nFanins);
00333     uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
00334     // permute truth-tables to the common support
00335     Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1,  pCutRes->nFanins+1, uPhase,    1 );
00336     Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins,   uPhaseFan, 1 );
00337     // perform Boolean operation
00338     Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
00339     // return the cut to its original condition
00340     Cnf_CutInsertIthVar( pCut, iVar, iFan );
00341     // consider the simple case
00342     if ( pCutRes->nFanins < 5 )
00343     {
00344         pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
00345         return pCutRes;
00346     }
00347 
00348     // derive ISOP for positive phase
00349     RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
00350     pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
00351     // derive ISOP for negative phase
00352     Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
00353     RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
00354     pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
00355     Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
00356 
00357     // compute the cut cost
00358     if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
00359         pCutRes->Cost = 127;
00360     else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
00361         pCutRes->Cost = 127;
00362     else
00363         pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
00364     return pCutRes;
00365 }

Cnf_Cut_t* Cnf_CutCreate ( Cnf_Man_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Creates cut for the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file cnfCut.c.

00085 {
00086     Dar_Cut_t * pCutBest;
00087     Cnf_Cut_t * pCut;
00088     unsigned * pTruth;
00089     assert( Aig_ObjIsNode(pObj) );
00090     pCutBest = Dar_ObjBestCut( pObj );
00091     assert( pCutBest != NULL );
00092     assert( pCutBest->nLeaves <= 4 );
00093     pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
00094     memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
00095     pTruth = Cnf_CutTruth(pCut);
00096     *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
00097     pCut->Cost = Cnf_CutSopCost( p, pCutBest );
00098     return pCut;
00099 }

void Cnf_CutDeref ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file cnfCut.c.

00133 {
00134     Aig_Obj_t * pObj;
00135     int i;
00136     Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
00137     {
00138         assert( pObj->nRefs > 0 );
00139         pObj->nRefs--;
00140     }
00141 }

void Cnf_CutFree ( Cnf_Cut_t *  pCut  ) 

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file cnfCut.c.

00066 {
00067     if ( pCut->vIsop[0] )
00068         Vec_IntFree( pCut->vIsop[0] );
00069     if ( pCut->vIsop[1] )
00070         Vec_IntFree( pCut->vIsop[1] );
00071 }

void Cnf_CutInsertIthVar ( Cnf_Cut_t *  pCut,
int  iVar,
int  iFan 
)

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

Synopsis [Inserts the fanin variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 271 of file cnfCut.c.

00272 {
00273     int i;
00274     for ( i = pCut->nFanins; i > iVar; i-- )
00275         pCut->pFanins[i] = pCut->pFanins[i-1];
00276     pCut->pFanins[iVar] = iFan;
00277     pCut->nFanins++;
00278 }

static int Cnf_CutMergeLeaves ( Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
int *  pFanins 
) [inline, static]

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

Synopsis [Merges two arrays of integers.]

Description [Returns the number of items.]

SideEffects []

SeeAlso []

Definition at line 193 of file cnfCut.c.

00194 {
00195     int i, k, nFanins = 0;
00196     for ( i = k = 0; i < pCut->nFanins && k < pCutFan->nFanins; )
00197     {
00198         if ( pCut->pFanins[i] == pCutFan->pFanins[k] )
00199             pFanins[nFanins++] = pCut->pFanins[i], i++, k++;
00200         else if ( pCut->pFanins[i] < pCutFan->pFanins[k] )
00201             pFanins[nFanins++] = pCut->pFanins[i], i++;
00202         else
00203             pFanins[nFanins++] = pCutFan->pFanins[k], k++;
00204     }
00205     for ( ; i < pCut->nFanins; i++ )
00206         pFanins[nFanins++] = pCut->pFanins[i];
00207     for ( ; k < pCutFan->nFanins; k++ )
00208         pFanins[nFanins++] = pCutFan->pFanins[k];
00209     return nFanins;
00210 }

void Cnf_CutPrint ( Cnf_Cut_t *  pCut  ) 

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file cnfCut.c.

00113 {
00114     int i;
00115     printf( "{" );
00116     for ( i = 0; i < pCut->nFanins; i++ )
00117         printf( "%d ", pCut->pFanins[i] );
00118     printf( " } " );
00119 }

void Cnf_CutRef ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file cnfCut.c.

00155 {
00156     Aig_Obj_t * pObj;
00157     int i;
00158     Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
00159     {
00160         pObj->nRefs++;
00161     }
00162 }

void Cnf_CutRemoveIthVar ( Cnf_Cut_t *  pCut,
int  iVar,
int  iFan 
)

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

Synopsis [Removes the fanin variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file cnfCut.c.

00252 {
00253     int i;
00254     assert( pCut->pFanins[iVar] == iFan );
00255     pCut->nFanins--;
00256     for ( i = iVar; i < pCut->nFanins; i++ )
00257         pCut->pFanins[i] = pCut->pFanins[i+1];
00258 }

void Cnf_CutUpdateRefs ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
Cnf_Cut_t *  pCutRes 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file cnfCut.c.

00176 {
00177     Cnf_CutDeref( p, pCut );
00178     Cnf_CutDeref( p, pCutFan );
00179     Cnf_CutRef( p, pCutRes );
00180 }

static unsigned Cnf_TruthPhase ( Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCut1 
) [inline, static]

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

Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file cnfCut.c.

00224 {
00225     unsigned uPhase = 0;
00226     int i, k;
00227     for ( i = k = 0; i < pCut->nFanins; i++ )
00228     {
00229         if ( k == pCut1->nFanins )
00230             break;
00231         if ( pCut->pFanins[i] < pCut1->pFanins[k] )
00232             continue;
00233         assert( pCut->pFanins[i] == pCut1->pFanins[k] );
00234         uPhase |= (1 << i);
00235         k++;
00236     }
00237     return uPhase;
00238 }

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